Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems

Christian Desrosiers (), Philippe Galinier (), Alain Hertz () and Sandrine Paroz ()
Additional contact information
Christian Desrosiers: Ecole Polytechnique and GERAD
Philippe Galinier: Ecole Polytechnique and CRT
Alain Hertz: Ecole Polytechnique and GERAD
Sandrine Paroz: Ecole Polytechnique and GERAD

Journal of Combinatorial Optimization, 2009, vol. 18, issue 2, No 2, 124-150

Abstract: Abstract In this paper, we propose efficient algorithms to extract minimal unsatisfiable subsets of clauses or variables in unsatisfiable propositional formulas. Such subsets yield unsatisfiable propositional subformulas that become satisfiable when any of their clauses or variables is removed. These subformulas have numerous applications, including proving unsatisfiability and post-infeasibility analysis. The algorithms we propose are based on heuristics, and thus, can be applied to large instances. Furthermore, we show that, in some cases, the minimality of the subformulas can be proven with these algorithms. We also present an original algorithm to find minimum cardinality unsatisfiable subformulas in smaller instances. Finally, we report computational experiments on unsatisfiable instances from various sources, that demonstrate the effectiveness of our algorithms.

Keywords: Satisfiability; Heuristics; Minimal unsatisfiable subformulas (MUS) (search for similar items in EconPapers)
Date: 2009
References: View references in EconPapers View complete reference list from CitEc
Citations: View citations in EconPapers (1)

Downloads: (external link)
http://link.springer.com/10.1007/s10878-008-9142-4 Abstract (text/html)
Access to the full text of the articles in this series is restricted.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:jcomop:v:18:y:2009:i:2:d:10.1007_s10878-008-9142-4

Ordering information: This journal article can be ordered from
https://www.springer.com/journal/10878

DOI: 10.1007/s10878-008-9142-4

Access Statistics for this article

Journal of Combinatorial Optimization is currently edited by Thai, My T.

More articles in Journal of Combinatorial Optimization from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().