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

Copyright Owner and License

Authors

Additional URL

https://doi.org/10.1145/3324884.3416569

Share

COinS