Title: ASIG: An all-solution SAT solver for CNF formulas
Abstract: 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.
Publication Year: 2009
Publication Date: 2009-08-01
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 8
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot