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: | Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
Springer Verlag
2014
|
| Acceso en línea: | Registro en Scopus DOI Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 06663caa a22007937a 4500 | ||
|---|---|---|---|
| 001 | PAPER-14724 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230420114330.0 | ||
| 008 | 190411s2014 xx ||||fo|||| 00| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-84921390037 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 100 | 1 | |a Castaňo, J.M. | |
| 245 | 1 | 2 | |a A parsing approach to SAT |
| 260 | |b Springer Verlag |c 2014 | ||
| 270 | 1 | 0 | |m Castaňo, J.M.; Depto. de Computación, FCEyN, UBAArgentina |
| 504 | |a Barton, G.E., Computational complexity in two-level morphology (1986) Proc. of the 24th ACL, pp. 53-59. , New York | ||
| 504 | |a Biere, A., Heule, M., van Maaren, H., Walsh, T., (2009) Handbook of Satisfiability, , IOS Press | ||
| 504 | |a Büchi, J.R., Weak second-order arithmetic and finite automata (1960) Zeit. Math. Logik. Grund. Math, pp. 66-92 | ||
| 504 | |a Castaño, J., Global index grammars and descriptive power (2004) Journal of Logic, Language and Information, 13, pp. 403-419 | ||
| 504 | |a Cherubini, A., Breveglieri, L., Citrini, C., Reghizzi, S., Multipushdown languages and grammars (1996) International Journal of Foundations of Computer Science, 7 (3), pp. 253-292 | ||
| 504 | |a Dassow, J., Păun, G., Salomaa, A., Grammars with controlled derivations (1997) Handbook of Formal Languages, 2. , Springer, Berlin | ||
| 504 | |a Earley, J., An Efficient Context-free Parsing Algorithm (1970) Communications of the ACM, 13, pp. 94-102 | ||
| 504 | |a Elgot, C.C., (1961) Decision problems of automata design and related arithmetics, , Transactions of the American Mathematical Society | ||
| 504 | |a Gómez-Rodríguez, C., Kuhlmann, M., Satta, G., Efficient parsing of well-nested linear context-free rewriting systems (2010) Human Language Technologies: The 2010 Annual Conference of the North American Chapter of the Association for Computational Linguistics, pp. 276-284. , HLT 2010,. Association for Computational Linguistics, Stroudsburg | ||
| 504 | |a Khabbaz, N.A., A geometric hierarchy of languages (1974) Journal of Computer and System Sciences, 8 (2), pp. 142-157 | ||
| 504 | |a Neuhaus, P., Broker, N., The complexity of recognition of linguistically adequate dependency grammars (1997) Proceedings of the 35th AnnualMeeting of the Association for Computational Linguistics, pp. 337-343. , Association for Computational Linguistics, Madrid | ||
| 504 | |a Purdom, P.W., Jr., Brown, C.A., Parsing extended LR(k) grammars (1981) Acta Informatica, 15 (2), pp. 115-127 | ||
| 504 | |a Ristad, E.S., Computational complexity of current GPSG theory (1986) Proc. of the 24th ACL, pp. 30-39. , New York | ||
| 504 | |a Satta, G., Recognition of Linear Context-Free Rewriting Systems (1992) ACL, pp. 89-95 | ||
| 504 | |a Satta, G., Some computational complexity results for synchronous context-free grammars (2005) Proceedings of HLT/EMNLP 2005, pp. 803-810 | ||
| 504 | |a Seki, H., Matsumura, T., Fujii, M., Kasami, T., On multiple context-free grammars (1991) Theoretical Computer. Science, pp. 191-229 | ||
| 504 | |a Shieber, S., Schabes, Y., Pereira, F., Principles and implementation of deductive parsing (1995) Journal of Logic Programming, 24, pp. 3-36 | ||
| 504 | |a Sikkel, K., (1997) Parsing schemata, , Springer | ||
| 504 | |a Tomita, M., An efficiente augmented-context-free parsing algorithm (1987) Computational Linguistics, 13, pp. 31-46 | ||
| 504 | |a La Torre, S., Madhusudan, P., Parlato, G., A robust class of context-sensitive languages (2007) LICS, pp. 161-170. , IEEE Computer Society | ||
| 504 | |a Vardi, M.Y., Logic and Automata: A Match Made in Heaven (2003) ICALP 2003. LNCS, 2719, pp. 64-65. , Springer, Heidelberg | ||
| 504 | |a Vardi, M.Y., Wolper, P., Automata-theoretic techniques for modal logics of programs (1986) J. Comput. Syst. Sci, 32, pp. 183-221 | ||
| 504 | |a Wartena, C., Storage products and linear control of derivations (2008) Theory of Computing Systems, 42 (2), pp. 157-186 | ||
| 504 | |a Weir, D., A geometric hierarchy beyond context-free languages (1992) Theoretical Computer Science, 104 (2), pp. 235-261 | ||
| 506 | |2 openaire | ||
| 520 | 3 | |a 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. |l eng | |
| 593 | |a Depto. de Computación, FCEyN, UBA, Buenos Aires, Argentina | ||
| 690 | 1 | 0 | |a ALL-SAT |
| 690 | 1 | 0 | |a EARLEY PARSING |
| 690 | 1 | 0 | |a MULTI-STACK AUTOMATA |
| 690 | 1 | 0 | |a SAT |
| 690 | 1 | 0 | |a AUTOMATA THEORY |
| 690 | 1 | 0 | |a BOOLEAN ALGEBRA |
| 690 | 1 | 0 | |a BOOLEAN FUNCTIONS |
| 690 | 1 | 0 | |a COMPUTATIONAL COMPLEXITY |
| 690 | 1 | 0 | |a FORMAL LOGIC |
| 690 | 1 | 0 | |a ALL-SAT |
| 690 | 1 | 0 | |a CONJUNCTIVE NORMAL FORMS |
| 690 | 1 | 0 | |a EARLEY PARSING |
| 690 | 1 | 0 | |a MULTI-STACK AUTOMATA |
| 690 | 1 | 0 | |a ORDER OF VARIABLES |
| 690 | 1 | 0 | |a PARSING ALGORITHM |
| 690 | 1 | 0 | |a PROPOSITIONAL SATISFIABILITY |
| 690 | 1 | 0 | |a SAT |
| 690 | 1 | 0 | |a FORMAL LANGUAGES |
| 773 | 0 | |d Springer Verlag, 2014 |g v. 8864 |h pp. 3-14 |p Lect. Notes Comput. Sci. |x 03029743 |w (AR-BaUEN)CENRE-983 |t Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-84921390037&doi=10.1007%2f978-3-319-12027-0_1&partnerID=40&md5=d1d4f32adfcc275ceecda7d229463311 |y Registro en Scopus |
| 856 | 4 | 0 | |u https://doi.org/10.1007/978-3-319-12027-0_1 |y DOI |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_03029743_v8864_n_p3_Castano |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v8864_n_p3_Castano |y Registro en la Biblioteca Digital |
| 961 | |a paper_03029743_v8864_n_p3_Castano |b paper |c PE | ||
| 962 | |a info:eu-repo/semantics/article |a info:ar-repo/semantics/artículo |b info:eu-repo/semantics/publishedVersion | ||
| 963 | |a VARI | ||
| 999 | |c 75677 | ||