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:
| Autor principal: | |
|---|---|
| Formato: | SER |
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_03029743_v8864_n_p3_Castano |
| Aporte de: |
| id |
todo:paper_03029743_v8864_n_p3_Castano |
|---|---|
| record_format |
dspace |
| spelling |
todo:paper_03029743_v8864_n_p3_Castano2023-10-03T15:19:39Z A parsing approach to SAT Castano, J.M. ALL-SAT Earley parsing Multi-stack automata SAT Automata theory Boolean algebra Boolean functions Computational complexity Formal logic ALL-SAT Conjunctive normal forms Earley parsing Multi-stack automata Order of variables Parsing algorithm Propositional satisfiability SAT Formal languages 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. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_03029743_v8864_n_p3_Castano |
| institution |
Universidad de Buenos Aires |
| institution_str |
I-28 |
| repository_str |
R-134 |
| collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
| topic |
ALL-SAT Earley parsing Multi-stack automata SAT Automata theory Boolean algebra Boolean functions Computational complexity Formal logic ALL-SAT Conjunctive normal forms Earley parsing Multi-stack automata Order of variables Parsing algorithm Propositional satisfiability SAT Formal languages |
| spellingShingle |
ALL-SAT Earley parsing Multi-stack automata SAT Automata theory Boolean algebra Boolean functions Computational complexity Formal logic ALL-SAT Conjunctive normal forms Earley parsing Multi-stack automata Order of variables Parsing algorithm Propositional satisfiability SAT Formal languages Castano, J.M. A parsing approach to SAT |
| topic_facet |
ALL-SAT Earley parsing Multi-stack automata SAT Automata theory Boolean algebra Boolean functions Computational complexity Formal logic ALL-SAT Conjunctive normal forms Earley parsing Multi-stack automata Order of variables Parsing algorithm Propositional satisfiability SAT Formal languages |
| description |
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. |
| format |
SER |
| author |
Castano, J.M. |
| author_facet |
Castano, J.M. |
| author_sort |
Castano, J.M. |
| title |
A parsing approach to SAT |
| title_short |
A parsing approach to SAT |
| title_full |
A parsing approach to SAT |
| title_fullStr |
A parsing approach to SAT |
| title_full_unstemmed |
A parsing approach to SAT |
| title_sort |
parsing approach to sat |
| url |
http://hdl.handle.net/20.500.12110/paper_03029743_v8864_n_p3_Castano |
| work_keys_str_mv |
AT castanojm aparsingapproachtosat AT castanojm parsingapproachtosat |
| _version_ |
1782025640971599872 |