Variable and clause ordering in an FSA approach to propositional satisfiability

Abstract

We use a finite state (FSA) construction approach to address the problem of propositional satisfiability (SAT). We use a very simple translation from formulas in conjunctive normal form (CNF) to regular expressions and use regular expressions to construct an FSA. As a consequence of the FSA construction, we obtain an ALL-SAT solver and model counter. We compare how several variable ordering (state ordering) heuristics affect the running time of the FSA construction. We also present a strategy for clause ordering (automata composition). We compare the running time of state-of-the-art model counters, BDD based sat solvers and we show that this FSA approach obtains state-of-the-art performance on some hard unsatisfiable benchmarks. This work brings up many questions on the possible use of automata to address SAT. © 2011 Springer-Verlag.