@inproceedings{9f8e3ca6713341d0896da74b2b6b1126,
title = "All-SAT using minimal blocking clauses",
abstract = "The All-SAT problem deals with determining all the satisfying assignments that exist for a given propositional logic formula. This problem occurs in verification applications including predicate abstraction and unbounded model checking. A typical All-SAT solver is based on iteratively computing satisfying assignments using a traditional Boolean satisfiability (SAT) solver and adding blocking clauses which are the complement of the total/partial assignments. We argue that such an algorithm is doing more work than needed and introduce new algorithms that are more efficient. Experiments show that these algorithms generate solutions with up to 14X fewer partial assignments and are up to three orders of magnitude faster.",
keywords = "All-SAT, Reachability, SAT, SAT solver, Verification",
author = "Yinlei Yu and Pramod Subramanyan and Nestan Tsiskaridze and Sharad Malik",
year = "2014",
doi = "10.1109/VLSID.2014.22",
language = "English (US)",
isbn = "9781479925124",
series = "Proceedings of the IEEE International Conference on VLSI Design",
pages = "86--91",
booktitle = "Proceedings - 27th International Conference on VLSI Design, VLSID 2014; Held Concurrently with 13th International Conference on Embedded Systems Design",
note = "27th International Conference on VLSI Design, VLSID 2014 - Held Concurrently with 13th International Conference on Embedded Systems Design ; Conference date: 05-01-2014 Through 09-01-2014",
}