A finite state intersection approach to propositional satisfiability
| Autor: | Castaño, J.M., Castaño, R. |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2012 |
| Předmět: |
Model counting
Construction approaches Conjunctive normal forms Propositional satisfiability SAT solvers Automata composition Regular expressions ALL-SAT Running time Decision theory Regular expression compilation Benchmarking Intersection grammars (FSIG) Several variables FSA intersection State-of-the-art performance Clause learning Boolean functions Pattern matching Finite automata Finite state |
| Zdroj: | Theor Comput Sci 2012;450:92-108 Biblioteca Digital (UBA-FCEN) Universidad Nacional de Buenos Aires. Facultad de Ciencias Exactas y Naturales instacron:UBA-FCEN |
| Popis: | We use a finite state (FSA) construction approach to address the problem of propositional satisfiability (SAT). We present 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. This automata construction can be considered essentially a finite state intersection grammar (FSIG). We also show how an FSIG approach can be encoded. Several variable ordering (state ordering) heuristics are compared in terms of the running time of the FSA and FSIG construction. We also present a strategy for clause ordering (automata composition). Running times of state-of-the-art model counters and BDD based SAT solvers are compared and we show that both the FSA and FSIG approaches obtain an state-of-the-art performance on some hard unsatisfiable benchmarks. It is also shown that clause learning techniques can help improve performance. This work brings up many questions on the possible use of automata and grammar models to address SAT. © 2012 Elsevier B.V. All rights reserved. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|