Publication Type
Conference Proceeding Article
Version
acceptedVersion
Publication Date
9-2020
Abstract
The All-SAT (All-SATisfiable) problem focuses on finding all satisfiable assignments of a given propositional formula, whose applications include model checking, automata construction, and logic minimization. A typical ALL-SAT solver is normally based on iteratively computing satisfiable assignments of the given formula. In this work, we introduce BASOLVER, a backbone-based All-SAT solver for propositional formulas. Compared to the existing approaches, BASOLVER generates shorter blocking clauses by removing backbone variables from the partial assignments and the blocking clauses. We compare BASOLVER with 4 existing ALL-SAT solvers, namely MBLOCKING, BC, BDD, and NBC. Experimental results indicate that although finding all the backbone variables consumes additional computing time, BASOLVER is still more efficient than the existing solvers because of the shorter blocking clauses and the backbone variables used in it. With the 608 formulas, BASOLVER solves the largest amount of formulas (86), which is 22%, 36%, 68%, 86% more formulas than MBLOCKING, BC, NBC, and BDD respectively. For the formulas that are both solved by BASOLVER and the other solvers, BASOLVER uses 88.4% less computing time on average than the other solvers. For the 215 formulas which first 1000 satisfiable assignments are found by at least one of the solvers, BASOLVER uses 180% less computing time on average than the other solvers.
Keywords
All-SAT, blocking clauses, satisfiability
Discipline
Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
2020 35th IEEE/ACM International Conference on Automated Software Engineering (ASE): Virtual, September 21-25: Proceedings
First Page
6
Last Page
17
ISBN
9781450367684
Identifier
10.1145/3324884.3416569
Publisher
ACM
City or Country
New York
Embargo Period
5-17-2021
Citation
ZHANG, Yueling; PU, Geguang; and SUN, Jun.
Accelerating All-SAT computation with short blocking clauses. (2020). 2020 35th IEEE/ACM International Conference on Automated Software Engineering (ASE): Virtual, September 21-25: Proceedings. 6-17.
Available at: https://ink.library.smu.edu.sg/sis_research/5944
Copyright Owner and License
Authors
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1145/3324884.3416569