Implementing Efficient All Solutions SAT Solvers
Takahisa Toda, Takehide Soh

TL;DR
This paper surveys, implements, and experimentally evaluates various techniques for All Solutions SAT (AllSAT) solvers, providing insights into solver characteristics and sharing open-source implementations to facilitate further research.
Contribution
It offers a comprehensive survey, faithful implementation, and extensive experiments of AllSAT techniques, along with publicly available solver code for future development.
Findings
Solver characteristics revealed through experiments
Implementation of multiple AllSAT techniques
Open-source code for community use
Abstract
All solutions SAT (AllSAT for short) is a variant of propositional satisfiability problem. Despite its significance, AllSAT has been relatively unexplored compared to other variants. We thus survey and discuss major techniques of AllSAT solvers. We faithfully implement them and conduct comprehensive experiments using a large number of instances and various types of solvers including one of the few public softwares. The experiments reveal solver's characteristics. Our implemented solvers are made publicly available so that other researchers can easily develop their solver by modifying our codes and compare it with existing methods.
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.
