skip to main content
10.1145/1120725.1120907acmconferencesArticle/Chapter ViewAbstractPublication PagesaspdacConference Proceedingsconference-collections
Article

MUP: a minimal unsatisfiability prover

Published: 18 January 2005 Publication History

Abstract

After establishing the unsatisfiability of a SAT instance encoding a typical design task, there is a practical need to identify its minimal unsatisfiable subsets, which pinpoint the reasons for the infeasibility of the design. Due to the potentially expensive computation, existing tools for the extraction of unsatisfiable subformulas do not guarantee the minimality of the results. This paper describes a practical algorithm that decides the minimal unsatisfiability of any CNF formula through BDD manipulation. This algorithm has a worse-case complexity that is exponential only in the treewidth of the CNF formula. We provide an empirical evaluation of the algorithm, highlighting its efficiency on a set of hard problems as well as its ability to work with existing subformula extraction tools to achieve optimal results.

References

[1]
Ron Aharoni and Nathan Linial. Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas. Journal of Combinatorial Theory Series A, 43:196--204, 1986.]]
[2]
Fadi Aloul, Igor Markov, and Karem Sakallah. Faster SAT and smaller BDDs via common function structure. In International Conference on Computer Aided Design (ICCAD), University of Michigan, 2001. Tool available for download at http://www.eecs.umich.edu/~faloul/Tools/mince/.]]
[3]
SAT Benchmarks from Automotive Product Configuration, http://www-sr.informatik.uni-tuebingen.de/~sinz/DC/.]]
[4]
H. L. Bodlaender, J. R. Gilbert, H. Hafsteinsson, and T. Kloks. Approximating treewidth, pathwidth, and minimum elimination tree height. Journal of Algorithms, 18:238--255, 1995.]]
[5]
Renato Bruni. Approximating minimal unsatisfiable subformulae by means of adaptive core search. Discrete Applied Mathematics, 130(2):85--100, 2003.]]
[6]
Renato Bruni and Antonio Sassano. Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae. Electronic Notes in Discrete Mathematics, 9, 2001.]]
[7]
R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35:677--691, 1986.]]
[8]
Hans Kleine Büning. On subclasses of minimal unsatisfiable formulas. Discrete Applied Mathematics, 107(1--3):83--98, 2000.]]
[9]
J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checking with partitioned transition relations. In Proceedings of the International Conference on Very Large Scale Integration, 1991.]]
[10]
Adnan Darwiche and Mark Hopkins. Using recursive decomposition to construct elimination orders, jointrees and dtrees. In Trends in Artificial Intelligence, Lecture notes in AI, 2143, pages 180--191. Springer-Verlag, 2001.]]
[11]
Gennady Davydov, Inna Davydova, and Hans Kleine Büning. An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF. Annals of Mathematics and Artificial Intelligence, 23(3--4):229--245, 1998.]]
[12]
Rina Dechter. Bucket elimination: A unifying framework for probabilistic inference. In Proceedings of the 12th Conference on Uncertainty in Artificial Intelligence, pages 211--219, 1996.]]
[13]
Herbert Fleischner, Oliver Kullmann, and Stefan Szeider. Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference. Theoretical Computer Science, 289(1):503--516, 2002.]]
[14]
R. Hojati, S. C. Krishnan, and R. K. Brayton. Early quantification and partitioned transition relations. In Proceedings of the International Conference on Computer Design, pages 12--19, 1996.]]
[15]
Holger H. Hoos and Thomas Sttzle. SATLIB: An Online Resource for Research on SAT. In I. P. Gent, H. v. Maaren, T. Walsh, editors, SAT 2000, pages 283--292. IOS Press, 2000. SATLIB is available online at www.satlib.org.]]
[16]
Jinbo Huang and Adnan Darwiche. Toward good elimination orders for symbolic SAT solving. In Proceedings of the 16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI), November 2004.]]
[17]
Oliver Kullmann. An application of matroid theory to the SAT problem. In Proceedings of the 15th Annual IEEE Conference on Computational Complexity, pages 116--124, 2000.]]
[18]
Matthew Moskewicz, Conor Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 39th Design Automation Conference, 2001.]]
[19]
Yoonna Oh, Maher N. Mneimneh, Zaher S. Andraus, Karem A. Sakallah, and Igor L. Markov. AMUSE: a minimally-unsatisfiable subformula extractor. In Proceedings of the 41st Annual Conference on Design Automation, pages 518--523. ACM Press, 2004.]]
[20]
Christos H. Papadimitriou and David Wolfe. The complexity of facets resolved. In Proceedings of the 26th Annual Symposium on Foundations of Computer Science, pages 74--78, 1985.]]
[21]
Christos H. Papadimitriou and Mihalis Yannakakis. The complexity of facets (and some facets of complexity). In Proceedings of the 14th Annual ACM Symposium on Theory of Computing, pages 255--260. ACM Press, 1982.]]
[22]
The Annual SAT Competitions: http://www.satlive.org/SATCompetition/.]]
[23]
Carsten Sinz, Andreas Kaiser, and Wolfgang Kchlin. Formal methods for the validation of automotive product configuration data. Artificial Intelligence for Engineering Design, Analysis and Manufacturing, 17 (2), 2003.]]
[24]
Fabio Somenzi. CUDD: CU Decision Diagram Package. Release 2.4.0.]]
[25]
Stefan Szeider. Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable. In Proceedings of the Nineth International Computing and Combinatorics Conference, pages 548--558. Springer Verlag, 2003.]]
[26]
Dimitrios Thilikos, Maria Serna, and Hans Bodlaender. A polynomial algorithm for the cutwidth of bounded degree graphs with small treewidth. Lecture Notes in Computer Science, 2161:380--390, 2001.]]
[27]
H. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit enumeration of finite state machines using BDDs. In Proceedings of the IEEE International Conferece on Computer Aided Design, pages 130--133, 1990.]]
[28]
Alasdair Urquhart. Hard examples for resolution. Journal of the ACM, 34(1):209--219, 1987.]]
[29]
Lintao Zhang and Sharad Malik. Extracting small unsatisfiable cores from unsatisfiable Boolean formula. Presented at the Sixth International Conference on Theory and Applications of Satisfiability Testing, 2003.]]

Cited By

View all
  • (2023)Conflict-free electric vehicle routing problem: an improved compositional algorithmDiscrete Event Dynamic Systems10.1007/s10626-023-00388-634:1(21-51)Online publication date: 18-Dec-2023
  • (2017)Learning lemma support graphs in Quip and IC32017 IEEE 2nd International Verification and Security Workshop (IVSW)10.1109/IVSW.2017.8031554(105-110)Online publication date: Jul-2017
  • (2016)Extracting unsatisfiable cores for LTL via temporal resolutionActa Informatica10.1007/s00236-015-0242-153:3(247-299)Online publication date: 1-Apr-2016
  • Show More Cited By
  1. MUP: a minimal unsatisfiability prover

    Recommendations

    Comments

    Information & Contributors

    Information

    Published In

    cover image ACM Conferences
    ASP-DAC '05: Proceedings of the 2005 Asia and South Pacific Design Automation Conference
    January 2005
    1495 pages
    ISBN:0780387376
    DOI:10.1145/1120725
    • General Chair:
    • Ting-Ao Tang
    Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

    Sponsors

    Publisher

    Association for Computing Machinery

    New York, NY, United States

    Publication History

    Published: 18 January 2005

    Permissions

    Request permissions for this article.

    Check for updates

    Qualifiers

    • Article

    Conference

    ASPDAC05
    Sponsor:

    Acceptance Rates

    Overall Acceptance Rate 466 of 1,454 submissions, 32%

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

    • Downloads (Last 12 months)4
    • Downloads (Last 6 weeks)0
    Reflects downloads up to 13 Feb 2025

    Other Metrics

    Citations

    Cited By

    View all
    • (2023)Conflict-free electric vehicle routing problem: an improved compositional algorithmDiscrete Event Dynamic Systems10.1007/s10626-023-00388-634:1(21-51)Online publication date: 18-Dec-2023
    • (2017)Learning lemma support graphs in Quip and IC32017 IEEE 2nd International Verification and Security Workshop (IVSW)10.1109/IVSW.2017.8031554(105-110)Online publication date: Jul-2017
    • (2016)Extracting unsatisfiable cores for LTL via temporal resolutionActa Informatica10.1007/s00236-015-0242-153:3(247-299)Online publication date: 1-Apr-2016
    • (2014)Resolution proof transformation for compression and interpolationFormal Methods in System Design10.1007/s10703-014-0208-x45:1(1-41)Online publication date: 1-Aug-2014
    • (2012)Improved single pass algorithms for resolution proof reductionProceedings of the 10th international conference on Automated Technology for Verification and Analysis10.1007/978-3-642-33386-6_10(107-121)Online publication date: 3-Oct-2012
    • (2011)Reducing the size of resolution proofs in linear timeInternational Journal on Software Tools for Technology Transfer (STTT)10.5555/3220904.322114713:3(263-272)Online publication date: 1-Jun-2011
    • (2011)On improving MUS extraction algorithmsProceedings of the 14th international conference on Theory and application of satisfiability testing10.5555/2023474.2023493(159-173)Online publication date: 19-Jun-2011
    • (2011)On Improving MUS Extraction AlgorithmsTheory and Applications of Satisfiability Testing - SAT 201110.1007/978-3-642-21581-0_14(159-173)Online publication date: 2011
    • (2010)Boosting minimal unsatisfiable core extractionProceedings of the 2010 Conference on Formal Methods in Computer-Aided Design10.5555/1998496.1998537(221-229)Online publication date: 20-Oct-2010
    • (2010)Minimal UnsatisfiabilityProceedings of the 2010 40th IEEE International Symposium on Multiple-Valued Logic10.1109/ISMVL.2010.11(9-14)Online publication date: 26-May-2010
    • Show More Cited By

    View Options

    Login options

    View options

    PDF

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader

    Figures

    Tables

    Media

    Share

    Share

    Share this Publication link

    Share on social media