Incremental SAT Library Integration Using Abstract Stobjs
Sol Swords (Centaur Technology, Inc.)
TL;DR
This paper presents a method to integrate incremental SAT solvers into ACL2 using an abstract stobj model, enabling formal reasoning about solver behavior and correctness of algorithms built on it.
Contribution
It introduces an abstract stobj model for incremental SAT libraries in ACL2, facilitating sound integration and correctness proofs.
Findings
Successfully modeled incremental SAT solver behavior as an abstract stobj.
Enabled formal reasoning about algorithms using the SAT library.
Provided a framework for verifying correctness assuming bug-free library implementation.
Abstract
We describe an effort to soundly use off-the-shelf incremental SAT solvers within ACL2 by modeling the behavior of a SAT solver library as an abstract stobj. The interface allows ACL2 programs to use incremental SAT solvers, and the abstract stobj model allows us to reason about the behavior of an incremental SAT library so as to show that algorithms implemented using it are correct, as long as the library is bug-free.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Business Process Modeling and Analysis · Logic, programming, and type systems