Document Open Access Logo

Itauto: An Extensible Intuitionistic SAT Solver

Author Frédéric Besson

PDF
Thumbnail PDF

File

LIPIcs.ITP.2021.9.pdf
  • Filesize: 0.75 MB
  • 18 pages

Document Identifiers

Author Details

Frédéric Besson
  • Inria, Univ Rennes, Irisa, Rennes, France

Acknowledgements

Thanks are due to Alix Trieu for sharing with us his verified Patricia Tree library. Thanks are also due to Samuel Gruetter for stress testing the tactic; his feedbacks have been very valuable.

Cite As Get BibTex

Frédéric Besson. Itauto: An Extensible Intuitionistic SAT Solver. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ITP.2021.9

Abstract

We present the design and implementation of itauto, a Coq reflexive tactic for intuitionistic propositional logic. The tactic inherits features found in modern SAT solvers: definitional conjunctive normal form; lazy unit propagation and conflict driven backjumping. Formulae are hash-consed using native integers thus enabling a fast equality test and a pervasive use of Patricia Trees. We also propose a hybrid proof by reflection scheme whereby the extracted solver calls user-defined tactics on the leaves of the propositional proof search thus enabling theory reasoning and the generation of conflict clauses. The solver has decent efficiency and is more scalable than existing tactics on synthetic benchmarks and preliminary experiments are encouraging for existing developments.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Computing methodologies → Theorem proving algorithms
Keywords
  • SAT solver
  • proof by reflection

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. John Allen. Anatomy of LISP. McGraw-Hill, Inc., USA, 1978. Google Scholar
  2. Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, and Benjamin Werner. A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. In CPP, volume 7086 of LNCS, pages 135-150. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-25379-9_12.
  3. Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, and Laurent Théry. Extending Coq with Imperative Features and Its Application to SAT Verification. In ITP, volume 6172 of LNCS, pages 83-98. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14052-5_8.
  4. Frédéric Besson, Pierre-Emmanuel Cornilleau, and David Pichardie. Modular SMT Proofs for Fast Reflexive Checking Inside Coq. In CPP, volume 7086 of LNCS, pages 151-166. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-25379-9_13.
  5. Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending Sledgehammer with SMT Solvers. J. Autom. Reason., 51(1):109-128, 2013. URL: https://doi.org/10.1007/s10817-013-9278-5.
  6. Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, and Christoph Weidenbach. A verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. J. Autom. Reason., 61(1-4):333-365, 2018. URL: https://doi.org/10.1007/s10817-018-9455-7.
  7. Sascha Böhme and Tjark Weber. Fast LCF-Style Proof Reconstruction for Z3. In ITP, volume 6172 of LNCS, pages 179-194. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14052-5_14.
  8. Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Déharbe, and Pascal Fontaine. veriT: An Open, Trustable and Efficient SMT-Solver. In CADE, volume 5663 of LNCS, pages 151-156. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02959-2_12.
  9. Pierre Castéran and Yves Bertot. Interactive theorem proving and program development. Coq'Art: The Calculus of inductive constructions. Texts in Theoretical Computer Science. Springer Verlag, 2004. URL: https://hal.archives-ouvertes.fr/hal-00344237.
  10. Koen Claessen and Dan Rosén. SAT Modulo Intuitionistic Implications. In LPAR-20, volume 9450 of LNCS, pages 622-637. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48899-7_43.
  11. Pierre Corbineau. Deciding Equality in the Constructor Theory. In TYPES, volume 4502 of LNCS, pages 78-92. Springer, 2006. URL: https://doi.org/10.1007/978-3-540-74464-1_6.
  12. Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In TACAS, volume 4963 of LNCS, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  13. Morgan Deters, Andrew Reynolds, Tim King, Clark W. Barrett, and Cesare Tinelli. A tour of CVC4: How it works, and how to use it. In FMCAD, page 7. IEEE, 2014. URL: https://doi.org/10.1109/FMCAD.2014.6987586.
  14. Roy Dyckhoff. Contraction-Free Sequent Calculi for Intuitionistic Logic. J. Symb. Log., 57(3):795-807, 1992. URL: https://doi.org/10.2307/2275431.
  15. Mathias Fleury, Jasmin Christian Blanchette, and Peter Lammich. A verified SAT solver with watched literals using imperative HOL. In CPP, pages 158-171. ACM, 2018. URL: https://doi.org/10.1145/3167080.
  16. Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. DPLL( T): Fast Decision Procedures. In CAV, volume 3114 of LNCS, pages 175-188. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-27813-9_14.
  17. John Harrison and Laurent Théry. A Skeptic’s Approach to Combining HOL and Maple. J. Autom. Reason., 21(3):279-294, 1998. URL: https://doi.org/10.1023/A:1006023127567.
  18. Joe Hurd. First-order proof tactics in higher-order logic theorem provers. In Design and Application of Strategies/Tactics in Higher Order Logics, number NASA/CP-2003-212448 in NASA Technical Reports, pages 56-68, 2003. Google Scholar
  19. Stéphane Lescuyer and Sylvain Conchon. A Reflexive Formalization of a SAT Solver in Coq. In Emerging Trends of TPHOLs, 2008. Google Scholar
  20. Stéphane Lescuyer and Sylvain Conchon. Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme. In FroCoS, volume 5749 of LNCS, pages 287-303. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04222-5_18.
  21. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an Efficient SAT Solver. In DAC, pages 530-535. ACM, 2001. URL: https://doi.org/10.1145/378239.379017.
  22. Chris Okasaki and Andrew Gill. Fast mergeable integer maps. In Workshop on ML, pages 77-86, 1998. Google Scholar
  23. Lawrence C. Paulson and Kong Woei Susanto. Source-Level Proof Reconstruction for Interactive Theorem Proving. In TPHOLs, volume 4732 of LNCS, pages 232-245. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74591-4_18.
  24. David A. Plaisted and Steven Greenbaum. A Structure-Preserving Clause Form Translation. J. Symb. Comput., 2(3):293-304, 1986. URL: https://doi.org/10.1016/S0747-7171(86)80028-1.
  25. Matthieu Sozeau and Nicolas Oury. First-Class Type Classes. In TPHOLs, volume 5170 of LNCS, pages 278-293. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_23.
  26. G. S. Tseitin. On the Complexity of Derivation in Propositional Calculus, pages 466-483. Springer, 1983. URL: https://doi.org/10.1007/978-3-642-81955-1_28.
  27. Tjark Weber and Hasan Amjad. Efficiently checking propositional refutations in HOL theorem provers. J. Appl. Log., 7(1):26-40, 2009. URL: https://doi.org/10.1016/j.jal.2007.07.003.
  28. Hantao Zhang and Mark E. Stickel. An Efficient Algorithm for Unit Propagation. In AI-MATH, pages 166-169, 1996. Google Scholar
  29. Hantao Zhang and Mark E. Stickel. Implementing the Davis-Putnam Method. J. Autom. Reason., 24(1/2):277-296, 2000. URL: https://doi.org/10.1023/A:1006351428454.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact