loading...
Tracking MUSes and Strict Inconsistent Covers
San Jose, California, USA November 12-November 16
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/FMCAD.2006.34Formal Methods in Computer Aided Desi ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Eric Gregoire, Universite d?Artois, France
Bertrand Mazure, Universite d?Artois, France
Cedric Piette, Universite d?Artois, France
In this paper, a new heuristic-based approach is introduced to extract minimally unsatisfiable subformulas (in short, MUSes) of SAT instances. It is shown that it often outperforms current competing methods. Then, the focus is on inconsistent covers, which represent sets of MUSes that cover enough independent sources of infeasibility for the instance to regain satisfiability if they were repaired. As the number of MUSes can be exponential with respect to the size of the instance, it is shown that such a concept is often a viable trade-off since it does not require us to compute all MUSes but provides us with enough mutually independent infeasibility causes that need to be addressed in order to restore satisfiability.
Citation:
Eric Gregoire, Bertrand Mazure, Cedric Piette, "Tracking MUSes and Strict Inconsistent Covers," fmcad, pp.39-46, Formal Methods in Computer Aided Design (FMCAD'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.