Recent searches
Search options
#SAT_Solver
0 posts0 participants0 posts today
Verifying a SAT solver from ground up. ~ Mathias Fleury. https://youtu.be/-NTodQdAjgQ #ITP #IsabelleHOL #SAT_solver
SATurn: SAT Solver-prover in lean 4. ~ Siddhartha Gadgil. https://github.com/siddhartha-gadgil/Saturn #ITP #LeanProver #Lean4 #SAT_Solver
GitHubGitHub - siddhartha-gadgil/Saturn: Experiments with SAT solvers with proofs in Lean 4Experiments with SAT solvers with proofs in Lean 4 - GitHub - siddhartha-gadgil/Saturn: Experiments with SAT solvers with proofs in Lean 4
No order-10 projective planes via SAT. ~ David Michael Roberts (@highergeometer). https://thehighergeometer.wordpress.com/2023/08/09/no-order-10-projective-planes-via-sat/ #SAT_solver #Math
theHigherGeometer · No order-10 projective planes via SATThe proof that there is no finite projective plane of “order 10” (namely, one with 9 points per line) was a gory and large multi-part computation. The last phase, on a CRAY supercompute…
EduSAT: A pedagogical tool for theory and applications of boolean satisfiability. ~ Yiqi Zhao, Ziyan An, Meiyi Ma, Taylor Johnson. https://arxiv.org/abs/2308.07890 #Logic #SAT_Solver #SMT
arXiv.orgEduSAT: A Pedagogical Tool for Theory and Applications of Boolean SatisfiabilityBoolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) are
widely used in automated verification, but there is a lack of interactive tools
designed for educational purposes in this field. To address this gap, we
present EduSAT, a pedagogical tool specifically developed to support learning
and understanding of SAT and SMT solving. EduSAT offers implementations of key
algorithms such as the Davis-Putnam-Logemann-Loveland (DPLL) algorithm and the
Reduced Order Binary Decision Diagram (ROBDD) for SAT solving. Additionally,
EduSAT provides solver abstractions for five NP-complete problems beyond SAT
and SMT. Users can benefit from EduSAT by experimenting, analyzing, and
validating their understanding of SAT and SMT solving techniques. Our tool is
accompanied by comprehensive documentation and tutorials, extensive testing,
and practical features such as a natural language interface and SAT and SMT
formula generators, which also serve as a valuable opportunity for learners to
deepen their understanding. Our evaluation of EduSAT demonstrates its high
accuracy, achieving 100% correctness across all the implemented SAT and SMT
solvers. We release EduSAT as a python package in .whl file, and the source can
be identified at https://github.com/zhaoy37/SAT_Solver.
Satisfiability-aided language models using declarative prompting. ~ Xi Ye, Qiaochu Chen, Isil Dillig, Greg Durrett. https://arxiv.org/abs/2305.09656 #LLMs #SAT_Solver
arXiv.orgSatLM: Satisfiability-Aided Language Models Using Declarative PromptingPrior work has combined chain-of-thought prompting in large language models (LLMs) with programmatic representations to perform effective and transparent reasoning. While such an approach works well for tasks that only require forward reasoning (e.g., straightforward arithmetic), it is less effective for constraint solving problems that require more sophisticated planning and search. In this paper, we propose a new satisfiability-aided language modeling (SatLM) approach for improving the reasoning capabilities of LLMs. We use an LLM to generate a declarative task specification rather than an imperative program and leverage an off-the-shelf automated theorem prover to derive the final answer. This approach has two key advantages. The declarative specification is closer to the problem description than the reasoning steps are, so the LLM can parse it out of the description more accurately. Furthermore, by offloading the actual reasoning task to an automated theorem prover, our approach can guarantee the correctness of the answer with respect to the parsed specification and avoid planning errors in the solving process. We evaluate SATLM on 8 different datasets and show that it consistently outperforms program-aided LMs in the imperative paradigm. In particular, SATLM outperforms program-aided LMs by 23% on a challenging subset of the GSM arithmetic reasoning dataset; SATLM also achieves a new SoTA on LSAT and BoardgameQA, surpassing previous models that are trained on the respective training sets.
Generating extended resolution proofs with a BDD-based SAT solver. ~ Randal E. Bryant, Marijn J. H. Heule. https://arxiv.org/abs/2105.00885 #Logic #ATP #SAT_Solver
arXiv.orgGenerating Extended Resolution Proofs with a BDD-Based SAT SolverIn 2006, Biere, Jussila, and Sinz made the key observation that the
underlying logic behind algorithms for constructing Reduced, Ordered Binary
Decision Diagrams (BDDs) can be encoded as steps in a proof in the extended
resolution logical framework. Through this, a BDD-based Boolean satisfiability
(SAT) solver can generate a checkable proof of unsatisfiability for a set of
clauses. Such a proof indicates that the formula is truly unsatisfiable without
requiring the user to trust the BDD package or the SAT solver built on top of
it.
We extend their work to enable arbitrary existential quantification of the
formula variables, a critical capability for BDD-based SAT solvers. We
demonstrate the utility of this approach by applying a BDD-based solver,
implemented by modifying an existing BDD package, to several challenging
Boolean satisfiability problems. Our resultsdemonstrate scaling for parity
formulas, as well as the Urquhart, mutilated chessboard, and pigeonhole
problems far beyond that of other proof-generating SAT solvers.