research-article

A verified SAT solver with watched literals using imperative HOL

Authors:

Mathias Fleury,

Jasmin Christian Blanchette,

Peter LammichAuthors Info & Claims

CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs

Pages 158 - 171

https://doi.org/10.1145/3167080

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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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.

Digital Library

[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

Lammich P(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
https://doi.org/10.1007/s10817-024-09701-w
Tan YHeule MMyreen M(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
https://doi.org/10.1007/s10009-022-00690-y
Lotz KKulczynski MNowotka DPoulsen DSchlichtkrull A(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
https://doi.org/10.1007/978-3-031-40247-0_15
Show More Cited By

Index Terms

A verified SAT solver with watched literals using imperative HOL
1. Computing methodologies
  1. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms
      1. Theorem proving algorithms
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Software verification

Recommendations

A verified prover based on ordered resolution
CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

The superposition calculus, which underlies first-order theorem provers such as E, SPASS, and Vampire, combines ordered resolution and equality reasoning. As a step towards verifying modern provers, we specify, using Isabelle/HOL, a purely functional ...
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

We developed a formal framework for conflict-driven clause learning (CDCL) using the Isabelle/HOL proof assistant. Through a chain of refinements, an abstract CDCL calculus is connected first to a more concrete calculus, then to a SAT solver expressed ...
Refinement to Imperative HOL

Many algorithms can be implemented most efficiently with imperative data structures. This paper presents Sepref, a stepwise refinement based tool chain for the verification of imperative algorithms in Isabelle/HOL. As a back end we use imperative HOL, ...

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

Program Chairs:
June Andronick
Data61 at CSIRO, Australia / UNSW, Australia
,
Amy Felty
University of Ottawa, Canada

Copyright © 2018 ACM.

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

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGLOG: ACM Special Interest Group on Logic and Computation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 January 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

European Research Council

Conference

CPP '18

Sponsor:

SIGPLAN

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

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
154
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)2

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lammich P(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
https://doi.org/10.1007/s10817-024-09701-w
Tan YHeule MMyreen M(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
https://doi.org/10.1007/s10009-022-00690-y
Lotz KKulczynski MNowotka DPoulsen DSchlichtkrull A(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
https://doi.org/10.1007/978-3-031-40247-0_15
Baek SCarneiro MHeule M(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
https://doi.org/10.1007/978-3-030-72016-2_4
Tan YHeule MMyreen M(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
https://doi.org/10.1007/978-3-030-72013-1_12
Schlichtkrull ABlanchette JTraytel DWaldmann U(2020)Formalizing Bachmair and Ganzinger’s Ordered Resolution ProverJournal of Automated Reasoning10.1007/s10817-020-09561-0Online publication date: 17-Jun-2020
https://doi.org/10.1007/s10817-020-09561-0
Lammich P(2020)Efficient Verified Implementation of Introsort and PdqsortAutomated Reasoning10.1007/978-3-030-51054-1_18(307-323)Online publication date: 24-Jun-2020
https://doi.org/10.1007/978-3-030-51054-1_18
Blanchette JFontaine PSchulz STourret SWaldmann U(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
https://doi.org/10.4204/EPTCS.311.2
Schlichtkrull ABlanchette JTraytel DMahboubi AMyreen M(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
https://dl.acm.org/doi/10.1145/3293880.3294100
Blanchette JMahboubi AMyreen M(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
https://dl.acm.org/doi/10.1145/3293880.3294087
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents