skip to main content
10.1145/1629911.1630057acmconferencesArticle/Chapter ViewAbstractPublication PagesdacConference Proceedingsconference-collections
research-article

Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts

Published: 26 July 2009 Publication History

Abstract

Boolean satisfiability (SAT) solvers are used heavily in hardware and software verification tools for checking satisfiability of Boolean formulas. Most state-of-the-art SAT solvers are based on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm and require the input formula to be in conjunctive normal form (CNF). We present a new SAT solver that operates on the negation normal form (NNF) of the given Boolean formulas/circuits. The NNF of a formula is usually more succinct than the CNF of the formula in terms of the number of variables. Our algorithm applies the DPLL algorithm to the graph-based representations of NNF formulas. We adapt the idea of the two-watched-literal scheme from CNF SAT solvers in order to efficiently carry out Boolean Constraint Propagation (BCP), a key task in the DPLL algorithm. We evaluate the new solver on a large collection of Boolean circuit benchmarks obtained from formal verification problems. The new solver outperforms the top solvers of the SAT 2007 competition and SAT-Race 2008 in terms of run time on a large majority of the benchmarks.

References

[1]
AIGER, http://fmv.jku.at/aiger.
[2]
Hardware model checking competition, http://fmv.jku.at/hwmcc07/.
[3]
Minisat sat solver. http://minisat.se/.
[4]
Picosat sat solver. http://fmv.jku.at/picosat/.
[5]
Rsat sat solver. http://reasoning.cs.ucla.edu/rsat/.
[6]
SAT competition 2007, www.satcompetition.org/2007/.
[7]
P. B. Andrews. An Introduction to Mathematical Logic and Type Theory: to Truth through Proof. Kluwer Academic Publishers, second edition, 2002.
[8]
A. Biere. Picosat essentials. Journal on Boolean Satisfiability, Boolean Modeling and Computation (JSAT), 4:75--97, 2008.
[9]
N. Eén and A. Biere. Effective Preprocessing in SAT Through Variable and Clause Elimination. In SAT, pages 61--75, 2005.
[10]
N. Eén, A. Mishchenko, and N. Sörensson. Applying Logic Synthesis for Speeding Up SAT. In SAT, pages 272--286, 2007.
[11]
N. Eén and N. Sörensson. An Extensible SAT-solver. In SAT, pages 502--518, 2003.
[12]
M. K. Ganai, P. Ashar, A. Gupta, L. Zhang, and S. Malik. Combining Strengths of Circuit-based and CNF-based Algorithms for a High-performance SAT solver. In DAC, 2002.
[13]
E. Goldberg and Y. Novikov. BerkMin: A Fast and Robust Sat-Solver. In DATE, 2002.
[14]
H. Jain. Verification using satisfiability checking, predicate abstraction, and craig interpolation. Technical Report CMU-CS-08-146, SCS, CMU, 2008.
[15]
H. Jain, C. Bartzis, and E. M. Clarke. Satisfiability checking of non-clausal formulas using general matings. In SAT, pages 75--89, 2006.
[16]
Feng Lu, Li-C. Wang, Kwang-Ting Cheng, and Ric C.-Y. Huang. A Circuit SAT Solver With Signal Correlation Guided Learning. In DATE, 2003.
[17]
J. P. Marques-Silva and K. A. Sakallah. GRASP - A New Search Algorithm for Satisfiability. In ICCAD, pages 220--227, November 1996.
[18]
M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In DAC, pages 530--535, June 2001.
[19]
K. Pipatsrisawat and A. Darwiche. A lightweight component caching scheme for satisfiability solvers. In SAT, pages 294--299, 2007.
[20]
C. Thiffault, F. Bacchus, and T. Walsh. Solving Non-clausal Formulas with DPLL Search. In SAT, 2004.
[21]
G. S. Tseitin. On the complexity of derivation in propositional calculus. In Studies in Constructive Maths and Mathematical Logic, pages 115--125, 1968.

Cited By

View all
  • (2014)A Syntactic Approach to Revising Epistemic States with Uncertain InputsProceedings of the 2014 IEEE 26th International Conference on Tools with Artificial Intelligence10.1109/ICTAI.2014.32(154-161)Online publication date: 10-Nov-2014
  • (2013)Model-Guided Approaches for MaxSAT SolvingProceedings of the 2013 IEEE 25th International Conference on Tools with Artificial Intelligence10.1109/ICTAI.2013.142(931-938)Online publication date: 4-Nov-2013
  • (2013)6 Years of SMT-COMPJournal of Automated Reasoning10.1007/s10817-012-9246-550:3(243-277)Online publication date: 1-Mar-2013
  • Show More Cited By

Index Terms

  1. Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts

    Recommendations

    Comments

    Information & Contributors

    Information

    Published In

    cover image ACM Conferences
    DAC '09: Proceedings of the 46th Annual Design Automation Conference
    July 2009
    994 pages
    ISBN:9781605584973
    DOI:10.1145/1629911
    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: 26 July 2009

    Permissions

    Request permissions for this article.

    Check for updates

    Author Tags

    1. Boolean satisfiability
    2. DPLL
    3. NNF
    4. verification

    Qualifiers

    • Research-article

    Conference

    DAC '09
    Sponsor:
    DAC '09: The 46th Annual Design Automation Conference 2009
    July 26 - 31, 2009
    California, San Francisco

    Acceptance Rates

    Overall Acceptance Rate 1,770 of 5,499 submissions, 32%

    Upcoming Conference

    DAC '25
    62nd ACM/IEEE Design Automation Conference
    June 22 - 26, 2025
    San Francisco , CA , USA

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

    • Downloads (Last 12 months)15
    • Downloads (Last 6 weeks)4
    Reflects downloads up to 09 Jan 2025

    Other Metrics

    Citations

    Cited By

    View all
    • (2014)A Syntactic Approach to Revising Epistemic States with Uncertain InputsProceedings of the 2014 IEEE 26th International Conference on Tools with Artificial Intelligence10.1109/ICTAI.2014.32(154-161)Online publication date: 10-Nov-2014
    • (2013)Model-Guided Approaches for MaxSAT SolvingProceedings of the 2013 IEEE 25th International Conference on Tools with Artificial Intelligence10.1109/ICTAI.2013.142(931-938)Online publication date: 4-Nov-2013
    • (2013)6 Years of SMT-COMPJournal of Automated Reasoning10.1007/s10817-012-9246-550:3(243-277)Online publication date: 1-Mar-2013
    • (2011)Minimally unsatisfiable boolean circuitsProceedings of the 14th international conference on Theory and application of satisfiability testing10.5555/2023474.2023492(145-158)Online publication date: 19-Jun-2011
    • (2011)Automated test case generation with SMT-solving and abstract interpretationProceedings of the Third international conference on NASA Formal methods10.5555/1986308.1986333(298-312)Online publication date: 18-Apr-2011
    • (2011)Optimizing the automatic test generation by SAT and SMT solving for Boolean expressionsProceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2011.6100079(388-391)Online publication date: 6-Nov-2011
    • (2011)Minimally Unsatisfiable Boolean CircuitsTheory and Applications of Satisfiability Testing - SAT 201110.1007/978-3-642-21581-0_13(145-158)Online publication date: 2011
    • (2011)Automated Test Case Generation with SMT-Solving and Abstract InterpretationNASA Formal Methods10.1007/978-3-642-20398-5_22(298-312)Online publication date: 2011
    • (2009)BeaverProceedings of the 21st International Conference on Computer Aided Verification10.1007/978-3-642-02658-4_53(668-674)Online publication date: 23-Jun-2009

    View Options

    Login options

    View options

    PDF

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader

    Media

    Figures

    Other

    Tables

    Share

    Share

    Share this Publication link

    Share on social media