A parsing approach to SAT
We present a parsing approach to address the problem of propositional satisfiability (SAT). We use a very simple translation from formulae in conjunctive normal form (CNF) to strings to be parsed by an Earley type algorithm. The parsing approach enables both a SAT and an ALL-SAT solver. The parsing...
Guardado en:
| Publicado: |
2014
|
|---|---|
| Materias: | |
| Acceso en línea: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v8864_n_p3_Castaňo http://hdl.handle.net/20.500.12110/paper_03029743_v8864_n_p3_Castaňo |
| Aporte de: |
| Sumario: | We present a parsing approach to address the problem of propositional satisfiability (SAT). We use a very simple translation from formulae in conjunctive normal form (CNF) to strings to be parsed by an Earley type algorithm. The parsing approach enables both a SAT and an ALL-SAT solver. The parsing algorithm is based in a model of automata that uses multiple stacks, presented here with a grammar characterization. The time complexity of the algorithm is polynomial, where the degree of the polynomial is dependent on the number of stacks used. It is not dependent on the length of the input nor properties of the grammar. However the number of stacks used might be a function on the number of variables and this is an open question. The number of stacks effectively used in practice is dependent on ordering of variables and clauses. A prototype of the parser was implemented and tested. © Springer International Publishing Switzerland 2014. |
|---|