Some notes on model rotation
Logic in Computer Science
2014-01-30 v4
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.
Cite
@article{arxiv.1308.2142,
title = {Some notes on model rotation},
author = {Siert Wieringa},
journal= {arXiv preprint arXiv:1308.2142},
year = {2014}
}
Comments
v1: Fixed a bug in the note after lemma 2.3 v2: Uploaded by accident (modified but incorrect definition of MES). v3: Fixed definition of MES