Some notes on model rotation

TL;DR

This paper explores model rotation in MUS finding algorithms, introducing blocked edges concept, showing some clauses are unreachable, and proving a conjecture, thereby advancing understanding of the technique's limitations.

Contribution

It introduces blocked edges in model rotation graphs, demonstrates unreachable clauses in certain formulas, and proves a conjecture related to model rotation.

Findings

Blocked edges can prevent traversal in model rotation graphs.

Some clauses are unreachable in irredundant CNF formulas.

A conjecture by Belov, Lynce, and Marques-Silva is proven.

Abstract

Model rotation is an efficient technique for improving MUS finding algorithms. In previous work we have studied model rotation as an algorithm that traverses a graph which is induced by the input formula. This document introduces the notion of blocked edges, which are edges in this graph that can never be traversed. We show the existence of irredundant CNF formulas in which some clauses are unreachable by model rotation. Additionally, we proof a conjecture by Belov, Lynce and Marques-Silva.