Accelerating All-SAT Computation with Short Blocking Clauses

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.