[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
10.1145/3167080acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

A verified SAT solver with watched literals using imperative HOL

Published: 08 January 2018 Publication History

Abstract

Based on our earlier formalization of conflict-driven clause learning (CDCL) in Isabelle/HOL, we refine the CDCL calculus to add a crucial optimization: two watched literals. We formalize the data structure and the invariants. Then we refine the calculus to obtain an executable SAT solver. Through a chain of refinements carried out using the Isabelle Refinement Framework, we target Imperative HOL and extract imperative Standard ML code. Although our solver is not competitive with the state of the art, it offers acceptable performance for some applications, and heuristics can be added to improve it further.

References

[1]
Gilles Audemard and Laurent Simon. 2009. Predicting Learnt Clauses Quality in Modern SAT Solvers. In IJCAI 2009, Craig Boutilier (Ed.). ijcai.org, 399–404.
[2]
Leo Bachmair and Harald Ganzinger. 2001. Resolution Theorem Proving. In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.). Vol. I. Elsevier, 19–99.
[3]
Ulrich Berger, Andrew Lawrence, Fredrik Nordvall Forsberg, and Monika Seisenberger. 2015. Extracting Verified Decision Procedures: DPLL and Resolution. Logical Methods in Computer Science 11, 1 (2015).
[4]
Armin Biere. 2016. Splatz, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2016. In SAT Competition 2016—Solver and Benchmark Descriptions (Department of Computer Science Series of Publications B), Tomáš Balyo, Marijn Heule, and Matti Järvisalo (Eds.), Vol. B-2016-1. University of Helsinki, 44–45.
[5]
Armin Biere and Andreas Fröhlich. 2015. Evaluating CDCL Variable Scoring Schemes. In SAT 2015 (LNCS), Marijn Heule and Sean Weaver (Eds.), Vol. 9340. Springer, 405–422.
[6]
Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). 2009. Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, Vol. 185. IOS Press.
[7]
Jasmin Christian Blanchette, Mathias Fleury, and Christoph Weidenbach. 2016. A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. In IJCAR 2016 (LNCS), Nicola Olivetti and Ashish Tiwari (Eds.), Vol. 9706. Springer, 25–44.
[8]
Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, and John Matthews. 2008. Imperative Functional Programming with Isabelle/HOL. In TPHOLs 2008 (LNCS), Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar (Eds.), Vol. 5170. Springer, 134–149.
[9]
Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt, Matt Kaufmann, and Peter Schneider-Kamp. 2017. Efficient Certified RAT Verification. In CADE-26 (LNCS), Leonardo de Moura (Ed.), Vol. 10395. Springer, 220–236.
[10]
Luís Cruz-Filipe, Joao Marques-Silva, and Peter Schneider-Kamp. 2017. Efficient Certified Resolution Proof Checking. In TACAS 2017 (LNCS), Axel Legay and Tiziana Margaria (Eds.), Vol. 10205. Springer, 118–135.
[11]
Martin Davis, George Logemann, and Donald W. Loveland. 1962. A Machine Program for Theorem-Proving. Commun. ACM 5, 7 (1962), 394–397.
[12]
Benjamin Delaware, Clément Pit-Claudel, Jason Gross, and Adam Chlipala. 2015. Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. In POPL 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 689–700.
[13]
Niklas Eén and Niklas Sörensson. 2003. An Extensible SAT-Solver. In SAT 2003 (LNCS), Enrico Giunchiglia and Armando Tacchella (Eds.), Vol. 2919. Springer, 502–518.
[14]
Mathias Fleury and Jasmin Christian Blanchette. 2017. Formalization of Weidenbach’s Automated Reasoning—The Art of Generic Problem Solving. (2017). https://bitbucket.org/isafol/isafol/src/master/ Weidenbach_Book/README.md, Formal proof development.
[15]
David Gries and Dennis M. Volpano. 1990. The Transform—A New Language Construct. Structured Programming 11, 1 (1990), 1–10.
[16]
Florian Haftmann and Tobias Nipkow. 2010. Code Generation via Higher-Order Rewrite Systems. In FLOPS 2010 (LNCS), Matthias Blume, Naoki Kobayashi, and Germán Vidal (Eds.), Vol. 6009. Springer, 103– 117.
[17]
Marijn Heule, Warren A. Hunt Jr., and Nathan Wetzler. 2014. Bridging the Gap between Easy Generation and Efficient Verification of Unsatisfiability Proofs. Softw. Test. Verif. Reliab. 24, 8 (2014), 593–607.
[18]
Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, and Nathan Wetzler. 2017. Efficient, Verified Checking of Propositional Proofs. In ITP 2017 (LNCS), Mauricio Ayala-Rincón and César A. Muñoz (Eds.), Vol. 10499. Springer, 269–284.
[19]
Peter Lammich. 2013. Automatic Data Refinement. In ITP 2013 (LNCS), Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.), Vol. 7998. Springer, 84–99.
[20]
Peter Lammich. 2015. Refinement to Imperative/HOL. In ITP 2015 (LNCS), Christian Urban and Xingyuan Zhang (Eds.), Vol. 9236. Springer, 253–269.
[21]
Peter Lammich. 2016. Refinement Based Verification of Imperative Data Structures. In CPP 2016, Jeremy Avigad and Adam Chlipala (Eds.). ACM, 27–36.
[22]
Peter Lammich. 2017. The GRAT Tool Chain—Efficient (UN)SAT Certificate Checking with Formal Correctness Guarantees. In SAT 2017 (LNCS), Serge Gaspers and Toby Walsh (Eds.), Vol. 10491. Springer, 457–463.
[23]
Peter Lammich and Thomas Tuerk. 2012. Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm. In ITP 2012 (LNCS), Lennart Beringer and Amy P. Felty (Eds.), Vol. 7406. Springer, 166–182.
[24]
Stephane Lescuyer. 2011. Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq. Ph.D. Dissertation. Université Paris-Sud.
[25]
Filip Marić. 2008. Formal Verification of Modern SAT Solvers. Archive of Formal Proofs (2008). http://isa-afp.org/entries/ SATSolverVerification.shtml, Formal proof development.
[26]
Filip Marić. 2010. Formal Verification of a Modern SAT Solver by Shallow Embedding into Isabelle/HOL. Theor. Comput. Sci. 411, 50 (2010), 4333–4356.
[27]
Daniel Matichuk, Toby C. Murray, and Makarius Wenzel. 2016. Eisbach: A Proof Method Language for Isabelle. J. Autom. Reasoning 56, 3 (2016), 261–282.
[28]
Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. 2001. Chaff: Engineering an Efficient SAT Solver. In DAC 2001. ACM, 530–535.
[29]
Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. 2006. Solving SAT and SAT Modulo Theories: From an Abstract Davis–Putnam– Logemann–Loveland Procedure to DPLL(T). J. ACM 53, 6 (2006), 937–977.
[30]
Duckki Oe, Aaron Stump, Corey Oliver, and Kevin Clancy. 2012. versat : A Verified Modern SAT Solver. In VMCAI 2012, Viktor Kuncak and Andrey Rybalchenko (Eds.). LNCS, Vol. 7148. Springer, 363–378.
[31]
Knot Pipatsrisawat and Adnan Darwiche. 2007. A Lightweight Component Caching Scheme for Satisfiability Solvers. In SAT 2007 (LNCS), João Marques-Silva and Karem A. Sakallah (Eds.), Vol. 4501. Springer, 294–299.
[32]
Lawrence Ryan. 2004. Efficient Algorithms for Clause-Learning SAT Solvers. Ph.D. Dissertation. Simon Fraser University.
[33]
Natarajan Shankar and Marc Vaucher. 2011. The Mechanical Verification of a DPLL-Based Satisfiability Solver. Electr. Notes Theor. Comput. Sci. 269 (2011), 3–17.
[34]
Niklas Sörensson and Armin Biere. 2009. Minimizing Learned Clauses. In SAT 2009 (LNCS), Oliver Kullmann (Ed.), Vol. 9340. Springer, 237– 243.
[35]
Aaron Stump, Morgan Deters, Adam Petcher, Todd Schiller, and Timothy W. Simpson. 2009. Verified Programming in Guru. In PLPV 2009, Thorsten Altenkirch and Todd D. Millstein (Eds.). ACM, 49–58.
[36]
René Thiemann and Christian Sternagel. 2009. Certification of Termination Proofs Using CeTA. In TPHOLs 2009 (LNCS), Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.), Vol. 5674. Springer, 452–468.
[37]
Christoph Weidenbach. 2015. Automated Reasoning Building Blocks. In Correct System Design: Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday (LNCS), Roland Meyer, André Platzer, and Heike Wehrheim (Eds.), Vol. 9360. Springer, 172–188.
[38]
Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt. 2014. DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. In SAT 2014 (LNCS), Carsten Sinz and Uwe Egly (Eds.), Vol. 8561. Springer, 422–429.

Cited By

View all
  • (2024)Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel SortingJournal of Automated Reasoning10.1007/s10817-024-09701-w68:3Online publication date: 19-Jun-2024
  • (2023)Verified Propagation Redundancy and Compositional UNSAT Checking in CakeMLInternational Journal on Software Tools for Technology Transfer10.1007/s10009-022-00690-y25:2(167-184)Online publication date: 27-Feb-2023
  • (2023)Verified Verifying: SMT-LIB for Strings in IsabelleImplementation and Application of Automata10.1007/978-3-031-40247-0_15(206-217)Online publication date: 10-Aug-2023
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs
January 2018
306 pages
ISBN:9781450355865
DOI:10.1145/3176245
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

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 January 2018

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Isabelle/HOL
  2. SAT solving
  3. conflict-driven clause learning (CDCL)
  4. stepwise refinement

Qualifiers

  • Research-article

Funding Sources

  • European Research Council

Conference

CPP '18
Sponsor:
CPP '18: Certified Proofs and Programs
January 8 - 9, 2018
CA, Los Angeles, USA

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

POPL '25

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)12
  • Downloads (Last 6 weeks)4
Reflects downloads up to 21 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2024)Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel SortingJournal of Automated Reasoning10.1007/s10817-024-09701-w68:3Online publication date: 19-Jun-2024
  • (2023)Verified Propagation Redundancy and Compositional UNSAT Checking in CakeMLInternational Journal on Software Tools for Technology Transfer10.1007/s10009-022-00690-y25:2(167-184)Online publication date: 27-Feb-2023
  • (2023)Verified Verifying: SMT-LIB for Strings in IsabelleImplementation and Application of Automata10.1007/978-3-031-40247-0_15(206-217)Online publication date: 10-Aug-2023
  • (2021)A Flexible Proof Format for SAT Solver-Elaborator CommunicationTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-72016-2_4(59-75)Online publication date: 20-Mar-2021
  • (2021)cake_lpr: Verified Propagation Redundancy Checking in CakeMLTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-72013-1_12(223-241)Online publication date: 23-Mar-2021
  • (2020)Formalizing Bachmair and Ganzinger’s Ordered Resolution ProverJournal of Automated Reasoning10.1007/s10817-020-09561-0Online publication date: 17-Jun-2020
  • (2020)Efficient Verified Implementation of Introsort and PdqsortAutomated Reasoning10.1007/978-3-030-51054-1_18(307-323)Online publication date: 24-Jun-2020
  • (2019)Proceedings of the Second International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary AchievementsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.311.2311(11-17)Online publication date: 31-Dec-2019
  • (2019)A verified prover based on ordered resolutionProceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3293880.3294100(152-165)Online publication date: 14-Jan-2019
  • (2019)Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk)Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3293880.3294087(1-13)Online publication date: 14-Jan-2019
  • 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

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media