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_Castano http://hdl.handle.net/20.500.12110/paper_03029743_v8864_n_p3_Castano |
Aporte de: |
id |
paper:paper_03029743_v8864_n_p3_Castano |
---|---|
record_format |
dspace |
spelling |
paper:paper_03029743_v8864_n_p3_Castano2023-06-08T15:28:55Z A parsing approach to SAT 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. 2014 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v8864_n_p3_Castano 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 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. |
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 |
publishDate |
2014 |
url |
https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v8864_n_p3_Castano http://hdl.handle.net/20.500.12110/paper_03029743_v8864_n_p3_Castano |
_version_ |
1768541752253218816 |