ASIG: An all-solution SAT solver for CNF formulas

An all-solution Boolean satisfiability (SAT) solver aims to find all the satisfying assignments. In this paper, we introduce ASIG, an all-solution solver for satisfiability problems. ASIG operates on conjunctive normal forms (CNFs) instead of circuits or hybrid representations as most other all-solution solvers did. ASIG prevents the same solution from being found again by creating a blocking clause from a solution and adding it into the clause database. To ensure efficiency, ASIG embeds an incremental mechanism into zchaff to avoid starting search from scratch in searching for a new solution. ASIG also implements some other blocking clause management strategies such as earlier termination and blocking clause merging to further improve efficiency. All our work is tested and analyzed on a set of CNF benchmarks.