Some notes on model rotation
Wieringa, Siert
Original · EN
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.
English translation
This paper has no Arabic translation yet. Be the first: it takes a few seconds, and the result is stored for every future reader.