Itauto: An Extensible Intuitionistic SAT Solver - Archive ouverte HAL Access content directly
Conference Papers Year :

Itauto: An Extensible Intuitionistic SAT Solver



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. 2012 ACM Subject Classification Theory of computation → Automated reasoning; Computing methodologies → Theorem proving algorithms Keywords and phrases SAT solver, proof by reflection Digital Object Identifier 10.4230/LIPIcs.ITP.2021.9 Supplementary Material Software: archived at swh:1:dir:986dc28c9844ba2faedc3d134b2acfb31e8c27c4 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.
Fichier principal
Vignette du fichier
LIPIcs-ITP-2021-9.pdf (773.44 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03508736 , version 1 (03-01-2022)



Frédéric Besson. Itauto: An Extensible Intuitionistic SAT Solver. ITP 2021 - 12th International Conference on Interactive Theorem Proving, Jun 2021, Roma, Italy. pp.1-18, ⟨10.4230/LIPIcs.ITP.2021.9⟩. ⟨hal-03508736⟩
39 View
24 Download



Gmail Facebook Twitter LinkedIn More