×

zbMATH — the first resource for mathematics

Semantically-guided goal-sensitive reasoning: model representation. (English) Zbl 1356.68180
Summary: SGGS (Semantically-Guided Goal-Sensitive reasoning) is a clausal theorem-proving method, which generalizes to first-order logic the Davis-Putnam-Loveland-Logemann procedure with conflict-driven clause learning (DPLL-CDCL). SGGS starts from an initial interpretation, and works towards modifying it into a model of a given set of clauses, reporting unsatisfiability if there is no model. The state of the search for a model is described by a structure, called SGGS clause sequence. We present SGGS clause sequences as a formalism to represent models; and we prove their properties related to the mechanisms of SGGS for clausal propagation, conflict solving, and conflict-driven model repair at the first-order level.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Bachmair, L; Ganzinger, H, Rewrite-based equational theorem proving with selection and simplification, J. Log. Comput., 4, 217-247, (1994) · Zbl 0814.68117
[2] Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.) : Handbook of Satisfiability, chapter 26, pp. 825-886. IOS Press (2009) · Zbl 0938.68818
[3] Baumgartner, P.: Hyper tableaux - the next generation. In: de Swart, H. (ed.) : Proceedings of the 7th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), volume 1397 of Lecture Notes in Artificial Intelligence, pp. 60-76. Springer (1998) · Zbl 0910.03007
[4] Baumgartner, P.: FDPLL - A first-order Davis-Putnam-Logeman-Loveland procedure. In: McAllester, D. (ed.) : Proceedings of the 17th International Conference on Automated Deduction (CADE), volume 1831 of Lecture Notes in Artificial Intelligence, pp. 200-219. Springer (2000) · Zbl 0963.68182
[5] Baumgartner, P; Fuchs, A; Tinelli, C, Implementing the model evolution calculus, International Journal on Artificial Intelligence Tools, 15, 21-52, (2006)
[6] Baumgartner, P., Fuchs, A., Tinelli, C.: Lemma learning in the model evolution calculus. In: Hermann, M., Voronkov, A. (eds.) : Proceedings of the 13th Conference on Logic, Programming and Automated Reasoning (LPAR), volume 4246 of Lecture Notes in Artificial Intelligence, pp. 572-586. Springer (2006) · Zbl 1165.03308
[7] Baumgartner, P; Furbach, U, Consolution as a framework for comparing calculi, J. Symb. Comput., 16, 445-477, (1993) · Zbl 0803.68120
[8] Baumgartner, P., Furbach, U.: Variants of clausal tableaux. In: Bibel, W., Schmitt, P.H. (eds.) : Automated Deduction - A Basis for Applications, volume I: Foundations - Calculi and Methods, chapter 3, pp. 73-102. Kluwer Academic Publishers (1998) · Zbl 0977.68076
[9] Baumgartner, P; Pelzer, B; Tinelli, C, Model evolution calculus with equality - revised and implemented, J. Symb. Comput., 47, 1011-1045, (2012) · Zbl 1258.03020
[10] Baumgartner, P; Tinelli, C, The model evolution calculus as a first-order DPLL method, Artif. Intell., 172, 591-632, (2008) · Zbl 1182.03034
[11] Baumgartner, P., Waldmann, U.: Superposition and model evolution combined. In: Schmidt, R. (ed.): Proceedings of the 22nd International Conference on Automated Deduction (CADE), volume 5663 of Lecture Notes in Artificial Intelligence, pp. 17-34. Springer (2009) · Zbl 1237.03010
[12] Bender, M., Pelzer, B., Schon, C.: E-KRHyper 1.4: Extensions for unique names and description logic. In: Bonacina, M.P. (ed.) : Proceedings of the 24th International Conference on Automated Deduction (CADE), volume 7898 of Lecture Notes in Artificial Intelligence, pp. 126-134. Springer (2013) · Zbl 1381.68258
[13] Billon, J.-P.: The disconnection method. In: Miglioli, P., Moscato, U., Mundici, D., Ornaghi, M. (eds.) : Proceedings of the 5th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), volume 1071 of Lecture Notes in Artificial Intelligence, pp. 110-126. Springer (1996)
[14] Bonacina, M.P.: A taxonomy of theorem-proving strategies. In: Wooldridge, M.J., Veloso, M. (eds.) : Artificial Intelligence Today - Recent Trends and Developments, volume 1600 of Lecture Notes in Artificial Intelligence, pp. 43-84. Springer (1999) · Zbl 0984.03011
[15] Bonacina, MP, Towards a unified model of search in theorem proving: subgoal-reduction strategies, J. Symb. Comput., 39, 209-255, (2005) · Zbl 1126.68071
[16] Bonacina, M.P.: On theorem proving for program checking - Historical perspective and recent developments. In: Fernàndez, M. (ed.) : Proceedings of the 12th International Symposium on Principles and Practice of Declarative Programming (PPDP), pp. 1-11. ACM Press (2010)
[17] Bonacina, M.P., Lynch, C.A., de Moura, L.: On deciding satisfiability by DPLL(\({Γ }+\mathcal {T}\)) and unsound theorem proving. In: Schmidt, R. (ed.) : Proceedings of the 22nd International Conference on Automated Deduction (CADE), volume 5663 of Lecture Notes in Artificial Intelligence, pp. 35-50. Springer (2009) · Zbl 1237.68176
[18] Bonacina, MP; Lynch, CA; de Moura, L, On deciding satisfiability by theorem proving with speculative inferences, J. Autom. Reason., 47, 161-189, (2011) · Zbl 1243.68265
[19] Bonacina, M.P., Plaisted, D.A.: Constraint manipulation in SGGS. In: Kutsia, T., Ringeissen, C. (eds.) : Proceedings of the 28th Workshop on Unification (UNIF), Technical Reports of the Research Institute for Symbolic Computation, pp. 47-54. Johannes Kepler Universität (2014). Available at http://vsl2014.at/meetings/UNIF-index.html
[20] Bonacina, M.P., Plaisted, D.A.: SGGS theorem proving: an exposition. In: Konev, B., De Moura, L., Schulz, S. (eds.) : Proceedings of the 4th Workshop on Practical Aspects in Automated Reasoning (PAAR), EasyChair Proceedings in Computing (EPiC), pp. 1-14 (2014)
[21] Bonacina, M.P., Plaisted, D.A.: Semantically guided goal-sensitive reasoning: inference system and completeness. In preparation (2015) · Zbl 1356.68180
[22] Bradley, A.R., Manna, Z.: The Calculus of Computation - Decision Procedures with Applications to Verification. Springer (2007) · Zbl 1126.03001
[23] Ricardo C., Leitsch, A., Peltier, N.: Automated Model Building. Kluwer Academic Publishers (2004) · Zbl 1085.03009
[24] Chang, C.-L., Lee, R.C.-T.: Symbolic Logic and Mechanical Theorem Proving. Academic Press (1973) · Zbl 0263.68046
[25] Chu, H; Plaisted, DA, Model finding in semantically guided instance-based theorem proving, Fundamenta Informaticae, 21, 221-235, (1994) · Zbl 0938.68818
[26] Chu, H., Plaisted, D.A.: CLINS-S: a semantically guided first-order theorem prover. J. Autom. Reason. 18(2) (1997) · Zbl 1258.03020
[27] Cotton, S. Natural domain SMT: A preliminary assessment. In: Chatterjee, K., Henzinger, T.A. (eds.) : Proceedings of the 8th International Conference on Formal Modeling of Timed Systems (FORMATS), volume 6246 of Lecture Notes in Computer Science, pp. 77-91. Springer (2010) · Zbl 1290.68112
[28] Davis, M.: The Universal Computer. The Road from Leibniz to Turing. Mathematics/Logic/Computing Series. CRC Press, Taylor and Francis Group (2012). Turing Centenary Edition · Zbl 1243.68013
[29] Davis, M; Logemann, G; Loveland, D, A machine program for theorem-proving, Commun. ACM, 5, 394-397, (1962) · Zbl 0217.54002
[30] Davis, M; Putnam, H, A computing procedure for quantification theory, J. ACM, 7, 201-215, (1960) · Zbl 0212.34203
[31] de Moura, L., Bjørner, N.: Deciding effectively propositional logic using DPLL and substitution sets. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) : Proceedings of the 4th International Conference on Automated Reasoning (IJCAR), volume 5195 of Lecture Notes in Artificial Intelligence, pp. 410-425. Springer (2008) · Zbl 1165.03320
[32] de Moura, L., Bjørner, N.: Engineering DPLL(T) + saturation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) : Proceedings of the 4th International Conference on Automated Reasoning (IJCAR), volume 5195 of Lecture Notes in Artificial Intelligence, pp. 475-490. Springer (2008) · Zbl 1165.68479
[33] de Moura, L., Bjørner, N.: Bugs, moles and skeletons: Symbolic reasoning for software development. In: Giesl, J., Hähnle, R. (eds.): Proceedings of the 5th International Conference on Automated Reasoning (IJCAR), volume 6173 of Lecture Notes in Artificial Intelligence, pp. 400-411. Springer (2010) · Zbl 1291.68377
[34] de Moura, L; Bjørner, N, Satisfiability modulo theories: introduction and applications, Commun. ACM, 54, 69-77, (2011)
[35] de Moura, L., Jovanovic, D.; A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) : Proceedings of the 14th International Conference on Verification with Model Checking and Abstract Interpretation (VMCAI), volume 7737 of Lecture Notes in Computer Science, pp. 1-12. Springer (2013) · Zbl 0212.34203
[36] Detlefs, DL; Nelson, G; Saxe, JB, Simplify: a theorem prover for program checking, J. ACM, 52, 365-473, (2005) · Zbl 1323.68462
[37] Eén, N., Sörensson, N.: An extensible SAT solver [extended version 1.2]. In: Giunchiglia, E., Tacchella, A. (eds.) : Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 2919 of Lecture Notes in Computer Science, pp. 502-518. Springer (2004) · Zbl 0217.54002
[38] Emmer, M., Khasidashvili, Z., Korovin, K., Sticksel, C., Voronkov, A.: EPR-based bounded model checking at word level. In: Gramlich, B., Miller, D., Sattler, U. (eds.) : Proceedings of the 6th International Conference on Automated Reasoning (IJCAR), volume 7364 of Lecture Notes in Artificial Intelligence, pp. 210-224. Springer (2012) · Zbl 1358.68190
[39] Fermüller, C., Leitsch, A., Hustadt, U., Tammet, T.: Resolution decision procedures. In: Robinson, A., Voronkov, A. (eds.) : Handbook of Automated Reasoning, vol. 2, chapter 25, pp. 1793-1849. Elsevier (2001) · Zbl 0993.68119
[40] Fietzke, A.: Labelled superposition. PhD thesis, Max Planck Institut für Informatik, Saabrücken (2013)
[41] Fietzke, A., Weidenbach, C. Labelled splitting. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) : Proceedings of the 4th International Conference on Automated Reasoning (IJCAR), volume 5195 of Lecture Notes in Artificial Intelligence, pp. 459-474. Springer (2008) · Zbl 1165.03314
[42] Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS), pp. 55-64. IEEE Computer Society Press (2003) · Zbl 0157.02405
[43] Ganzinger, H., Korovin, K.: Theory instantiation. In: Hermann, M., Voronkov, A. (eds.) : Proceedings of the 13th Conference on Logic, Programming and Automated Reasoning (LPAR), volume 4246 of Lecture Notes in Artificial Intelligence, pp. 497-511. Springer (2006) · Zbl 1165.03315
[44] Haller, L., Griggio, A., Brain, M., Kroening, D.: Deciding floating-point logic with systematic abstraction. In: Cabodi, G., Singh, S. (eds.) : Proceedings of the 12th Conference on Formal Methods for Computer-Aided Design (FMCAD). ACM and IEEE (2012) · Zbl 1317.68110
[45] Hoder, K., Voronkov, A.: The 481 ways to split a clause and deal with propositional variables. In: Bonacina, M.P. (ed.) : Proceedings of the 24th International Conference on Automated Deduction (CADE), volume 7898 of Lecture Notes in Artificial Intelligence, pp. 450-464. Springer (2013) · Zbl 1382.68216
[46] Hsiang, J; Rusinowitch, M, Proving refutational completeness of theorem proving strategies: the transfinite semantic tree method, J. ACM, 38, 559-587, (1991) · Zbl 0799.68170
[47] Jacobs, S; Waldmann, U, Comparing instance generation methods for automated reasoning, J. Autom. Reason., 38, 57-78, (2007) · Zbl 1113.68089
[48] Jain, H.: Verification using satisfiability checking, predicate abstraction and Craig interpolation. PhD thesis, School of Computer Science, Carnegie Mellon University (2008)
[49] Marques-Silva, J.P., Sakallah, K.A.: GRASP: A new search algorithm for satisfiability. In: Proceedings of the International Conference on Computer-Aided Design (ICCAD), pp 220-227 (1997)
[50] Jovanović, D., Barrett, C., de Moura, L.: The design and implementation of the model-constructing satisfiability calculus. In: Jobstman, B., Ray, S. (eds.) Proceedings of the 13th Conference on Formal Methods in Computer Aided Design (FMCAD). FMCAD Inc. (2013) · Zbl 0479.68092
[51] Jovanovic, D., de Moura, L.: Cutting to the chase: Solving linear integer arithmetic. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) : Proceedings of the 23rd International Conference on Automated Deduction (CADE), volume 6803 of Lecture Notes in Artificial Intelligence, pp. 338-353. Springer (2011) · Zbl 1314.90054
[52] Jovanovic, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) : Proceedings of the 6th International Conference on Automated Reasoning (IJCAR), volume 7364 of Lecture Notes in Artificial Intelligence, pp. 339-354. Springer (2012) · Zbl 1358.68257
[53] Korovin, K.: An invitation to instantiation-based reasoning: from theory to practice. In: Schmidt, R. (ed.) : Proceedings of the 22nd International Conference on Automated Deduction (CADE), volume 5663 of Lecture Notes in Artificial Intelligence, pp. 163-166. Springer (2009) · Zbl 0959.68115
[54] Korovin, K.: Inst-Gen: a modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) : Programming Logics: Essays in Memory of Harald Ganzinger, volume 7797 of Lecture Notes in Artificial Intelligence, pp. 239-270. Springer (2013) · Zbl 1385.68038
[55] Korovin, K., Sticksel, C.: iProver-Eq: An instantiation-based theorem prover with equality. In: Giesl, J., Hähnle, R. (eds.) : Proceedings of the 5th International Conference on Automated Reasoning (IJCAR), volume 6173 of Lecture Notes in Artificial Intelligence, pp. 196-202. Springer (2010) · Zbl 1291.68354
[56] Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: Gent, I.P. (ed.) : Proceedings of the 15th International Conference on Constraint Programming (CP), volume 5732 of Lecture Notes in Computer Science, pp. 509-523. Springer (2009) · Zbl 1336.68236
[57] Kovàcs, L., Voronkov, A.: First order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) : Proceedings of the 25th International Conference on Computer-Aided Verification (CAV), volume 8044 of Lecture Notes in Computer Science, pp. 1-35. Springer (2013) · Zbl 0803.68120
[58] Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. Springer (2008) · Zbl 1149.68071
[59] Lee, S.-J., Plaisted, D.A.: Theorem proving using hyper-matching strategy. In: Ras, Z. (ed.) : Methodologies for Intelligent Systems, pp. 467-476, North-Holland (1989). Presented at the International Symposium on Methodologies for Intelligent Systems, October 1989 · Zbl 0814.68117
[60] Lee, S.-J., Plaisted, D.A.: Inference by clause matching. In: Ras, Z., Zemankova, M. (eds.) : Intelligent Systems, pp. 200-235. Ellis Horwood (1990) · Zbl 0967.68148
[61] Lee, S-J; Plaisted, DA, Eliminating duplication with the hyperlinking strategy, J. Autom. Reason., 9, 25-42, (1992) · Zbl 0784.68077
[62] Leino, K., Rustan, M., Milicevic, A.: Program extrapolation with Jennisys. In: Proceedings of the 27th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp. 411-430. ACM (2012)
[63] Letz, R.: Clausal tableaux. In: Bibel, W., Schmitt, P.H. (eds.) : Automated Deduction - A Basis for Applications, volume I: Foundations - Calculi and Methods, chapter 2, pp. 43-72. Kluwer Academic Publishers (1998) · Zbl 0966.03013
[64] Letz, R., Stenz, G.: DCTP - a disconnection calculus theorem prover. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) : Proceedings of the 1st International Conference on Automated Reasoning (IJCAR), volume 2083 of Lecture Notes in Artificial Intelligence, pp. 381-385. Springer (2001) · Zbl 0988.68589
[65] Letz, R., Stenz, G.: Model elimination and connection tableau procedures. In: Robinson, A., Voronkov, A. (eds.) : Handbook of Automated Reasoning, chapter 28, pp. 2015-2114. Elsevier (2001) · Zbl 1011.68130
[66] Letz, R., Stenz, G.: Proof and model generation with disconnection tableaux. In: Nieuwenhuis, R., Voronkov, A. (eds.) : Proceedings of the 8th International Conference on Logic, Programming and Automated Reasoning (LPAR), volume 2250 of Lecture Notes in Artificial Intelligence, pp. 142-156. Springer (2001) · Zbl 1275.03081
[67] Letz, R., Stenz, G.: Integration of equality reasoning into the disconnection calculus. In: Egly, U., Fermüller, C.G. (eds.) : Proceedings of the 15th International Conference on Analytic Tableaux and Related Methods (TABLEAUX), volume 2381 of Lecture Notes in Artificial Intelligence, pp. 176-190. Springer (2002) · Zbl 1015.68172
[68] Loveland, DW, A simplified format for the model elimination procedure, J. ACM, 16, 349-363, (1969) · Zbl 0183.29603
[69] Malik, S; Zhang, L, Boolean satisfiability: from theoretical hardness to practical success, Commun. ACM, 52, 76-82, (2009)
[70] McCune, W.W.: Semantic guidance with carefully chosen interpretations. In: Proceedings of the 6th Workshop on Strategies in Automated Deduction (STRATEGIES) (2006)
[71] McMillan, K.L., Kuehlmann, A., Sagiv, M. In: Bouajjani, A., Maler, O. (eds.) Proceedings of the 21st Conference on Computer Aided Verification (CAV), volume 5643 of Lecture Notes in Computer Science, pp. 462-476. Springer (2009)
[72] Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Chaff, S.M.: In: Blaauw, D., Lavagno, L. (eds.) : Engineering an efficient SAT solver (2001)
[73] Navarro, J.A., Voronkov, A.: Proof systems for effectively propositional logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) : Proceedings of the 4th International Conference on Automated Reasoning (IJCAR), volume 5195 of Lecture Notes in Artificial Intelligence, pp. 426-440. Springer (2008) · Zbl 1165.03318
[74] Nieuwenhuis, R; Oliveras, A; Tinelli, C, Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-logemann-loveland procedure to DPLL(T), J. ACM, 53, 937-977, (2006) · Zbl 1326.68164
[75] Peterson, GE; Stickel, ME, Complete sets of reductions for some equational theories, J. ACM, 28, 233-264, (1981) · Zbl 0479.68092
[76] Plaisted, D.A.: Mechanical theorem proving. In: Banerji, R.B. (ed.) : Formal Techniques in Artificial Intelligence, pp. 269-320. Elsevier (1990) · Zbl 0704.68095
[77] Plaisted, D.A., Miller, S.: The relative power of semantics and unification. In: Voronkov, A., Weidenbach, C. (eds.) : Programming Logics: Essays in Memory of Harald Ganzinger, volume 7797 of Lecture Notes in Artificial Intelligence, pp. 317-344. Springer (2013) · Zbl 1383.68081
[78] Plaisted, D.A., Zhu, Y.: The Efficiency of Theorem Proving Strategies. Friedr Vieweg & Sohns (1997) · Zbl 0881.68106
[79] Plaisted, DA; Zhu, Y, Ordered semantic hyper linking, J. Autom. Reason., 25, 167-217, (2000) · Zbl 0959.68115
[80] Riazanov, A.: Implementing an efficient theorem prover. PhD thesis, Department of Computer Science, The University of Manchester (2003)
[81] Robinson, JA, Automatic deduction with hyper-resolution, Int. J. Comput. Math., 1, 227-234, (1965) · Zbl 0158.26003
[82] Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) : Proceedings of the 19th International Conference on Logic, Programming and Automated Reasoning (LPAR), volume 8312 of Lecture Notes in Artificial Intelligence, pp 735-743. Springer (2013) · Zbl 1407.68442
[83] Shankar, N.: Little engines of proof, 2002. Invited talk, Federated Logic Conference, Copenhagen, Denmark; and course notes of Fall 2003, http://www.csl.sri.com/users/shankar/LEP.html
[84] Slagle, JR, Automatic theorem proving with renamable and semantic resolution, J. ACM, 14, 687-697, (1967) · Zbl 0157.02405
[85] Smullyan, R.M.: First-Order Logic. Dover Publications, New York (1995). First published by Springer in 1968 · Zbl 0172.28901
[86] Stickel, ME, A unification algorithm for associative commutative functions, J. ACM, 28, 423-434, (1981) · Zbl 0462.68075
[87] Stickel, ME, A prolog technology theorem prover, New Generation Computing, 2, 371-383, (1984)
[88] Stickel, ME, Automated deduction by theory resolution, J. Autom. Reason., 1, 333-355, (1985) · Zbl 0616.68076
[89] Stickel, ME, A prolog technology theorem prover: implementation by an extended prolog compiler, J. Autom. Reason., 4, 353-380, (1988) · Zbl 0662.68104
[90] Stickel, ME, A prolog technology theorem prover: new exposition and implementation in prolog, Theor. Comput. Sci., 104, 109-128, (1992) · Zbl 0771.68096
[91] Van Gelder, A; Tsuji, YK, Satisfiability testing with more reasoning and less guessing, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 26, 559-586, (1996) · Zbl 0868.03007
[92] Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) : Handbook of Automated Reasoning, vol. 2, pp. 1965-2012. Elsevier (2001) · Zbl 1011.68129
[93] Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R. (ed.) : Proceedings of the 22nd International Conference on Automated Deduction (CADE), volume 5663 of Lecture Notes in Artificial Intelligence, pp. 140-145. Springer (2009)
[94] Wos, L; Carson, D; Robinson, G, Efficiency and completeness of the set of support strategy in theorem proving, J. ACM, 12, 536-541, (1965) · Zbl 0135.18401
[95] Zhang, H; Stickel, ME, Implementing the Davis-Putnam method, J. Autom. Reason., 24, 277-296, (2000) · Zbl 0967.68148
[96] Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Voronkov, A. (ed.) : Proceedings of the 18th International Conference on Automated Deduction (CADE), volume 2392 of Lecture Notes in Artificial Intelligence, pp. 295-313. Springer (2002) · Zbl 1072.68599
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.