×

zbMATH — the first resource for mathematics

Propositional SAT solving. (English) Zbl 1392.68380
Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 247-275 (2018).
Summary: The Boolean Satisfiability Problem (SAT) is well known in computational complexity, representing the first decision problem to be proved NP-complete. SAT is also often the subject of work in proof complexity. Besides its theoretical interest, SAT finds a wide range of practical applications. Moreover, SAT solvers have been the subject of remarkable efficiency improvements since the mid-1990s, motivating their widespread use in many practical applications including Bounded and Unbounded Model Checking. The success of SAT solvers has also motivated the development of algorithms for natural extensions of SAT, including Quantified Boolean Formulas (QBF), Pseudo-Boolean constraints (PB), Maximum Satisfiability (MaxSAT) and Satisfiability Modulo Theories (SMT) which also see application in the model-checking context. This chapter first covers the organization of modern conflict-driven clause learning (CDCL) SAT solvers, which are used in the vast majority of practical applications of SAT. It then reviews the techniques shown to be effective in modern SAT solvers.
For the entire collection see [Zbl 1390.68001].

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] 1. Abío, I., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Mayer-Eichberger, V.: A new look at BDDs for pseudo-boolean constraints. J. Artif. Intell. Res. 45, 443-480 (2012) · Zbl 1252.68267
[2] 2. Achá, R.J.A., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Practical algorithms for unsatisfiability proof and core generation in SAT solvers. AI Commun. 23(2-3), 145-157 (2010) · Zbl 1208.68195
[3] 3. Ansótegui, C., Bonet, M.L., Levy, J.: SAT-based MaxSAT algorithms. Artif. Intell. 196, 77-105 (2013) · Zbl 1270.68265
[4] 4. Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality networks: a theoretical and empirical study. Constraints 16(2), 195-221 (2011) · Zbl 1217.68200
[5] 5. Audemard, G., Katsirelos, G., Simon, L.: A restriction of extended resolution for clause learning SAT solvers. In: Fox, M., Poole, D. (eds.) AAAI Conf. on Artificial Intelligence (AAAI), pp. 15-20. AAAI Press, Palo Alto (2010)
[6] 6. Audemard, G., Simon, L.: Experimenting with small changes in conflict-driven clause learning algorithms. In: Stuckey, P.J. (ed.) Intl. Conf. on Principles and Practice of Constraint Programming (CP). LNCS, vol. 5202, pp. 630-634. Springer, Heidelberg (2008)
[7] 7. Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) Intl. Joint Conf. on Artificial Intelligence (IJCAI), pp. 399-404. IJCAI/AAAI Press, Melbourne/Palo Alto (2009)
[8] 8. Bailleux, O., Boufkhad, Y., Roussel, O.: New encodings of pseudo-boolean constraints into CNF. In: Kullmann, O. (ed.) Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 5584, pp. 181-194. Springer, Heidelberg (2009) · Zbl 1247.68246
[9] 9. Baker, A.B.: The hazards of fancy backtracking. In: Hayes-Roth, B., Korf, R.E. (eds.) National Conference on Artificial Intelligence (AAAI), pp. 288-293. AAAI Press/MIT Press, Palo Alto/Cambridge (1994)
[10] 10. Bakker, R.R., Dikker, F., Tempelman, F., Wognum, P.M.: Diagnosing and solving over-determined constraint satisfaction problems. In: Bajcsy, R. (ed.) Intl. Joint Conf. on Artificial Intelligence (IJCAI), pp. 276-281. Morgan Kaufmann, Cambridge (1993)
[11] 11. Baptista, L., Marques-Silva, J.: Using randomization and learning to solve hard real-world instances of satisfiability. In: Dechter [30], pp. 489-494 · Zbl 1044.68736
[12] 12. Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825-885. IOS Press, Amsterdam (2009)
[13] 13. Batcher, K.E.: Sorting networks and their applications. In: AFIPS Spring Joint Computer Conference. AFIPS Conference Proceedings, vol. 32, pp. 307-314. Thomson Book Co., Washington D.C. (1968)
[14] 14. Bayardo, R.J. Jr., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Kuipers, B., Webber, B.L. (eds.) National Conference on Artificial Intelligence (AAAI), pp. 203-208. AAAI Press/MIT Press, Palo Alto/Cambridge (1997)
[15] 15. Belov, A., Chen, H., Mishchenko, A., Marques-Silva, J.: Core minimization in SAT-based abstraction. In: Macii, E. (ed.) Design, Automation & Test in Europe (DATE), pp. 1411-1416. EDA Consortium/ACM, San Jose/New York (2013)
[16] 16. Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun. 25(2), 97-116 (2012) · Zbl 1248.68450
[17] 17. Ben-Eliyahu, R., Dechter, R.: On computing minimal models. Ann. Math. Artif. Intell. 18(1), 3-27 (1996) · Zbl 0891.68109
[18] 18. Ben-Eliyahu-Zohary, R., Palopoli, L.: Reasoning with minimal models: efficient algorithms and applications. Artif. Intell. 96(2), 421-449 (1997) · Zbl 0903.68178
[19] 19. Biere, A.: PicoSAT essentials. J. Satisf. Boolean Model. Comput. 4(2-4), 75-97 (2008) · Zbl 1159.68403
[20] 20. Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, R. (ed.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 1579, pp. 193-207. Springer, Heidelberg (1999)
[21] 21. Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009) · Zbl 1183.68568
[22] 22. Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D.A. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol. 6538, pp. 70-87. Springer, Heidelberg (2011) · Zbl 1317.68109
[23] 23. Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Form. Asp. Comput. 20(4-5), 379-405 (2008) · Zbl 1149.68402
[24] 24. Brafman, R.I.: A simplifier for propositional formulas with many binary clauses. IEEE Trans. Syst. Man Cybern., Part B, Cybern. 34(1), 52-59 (2004)
[25] 25. Bryant, R.E.: Graph-based algorithms for boolean function manipulation. Trans. Comput. 35(8), 677-691 (1986) · Zbl 0593.94022
[26] 26. Büning, H.K., Bubeck, U.: Theory of quantified boolean formulas. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 735-760. IOS Press, Amsterdam (2009)
[27] 27. Büning, H.K., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 339-401. IOS Press, Amsterdam (2009)
[28] 28. Chinneck, J.W., Dravnieks, E.W.: Locating minimal infeasible constraint sets in linear programs. INFORMS J. Comput. 3(2), 157-168 (1991) · Zbl 0755.90055
[29] 29. Coelho, H., Studer, R., Wooldridge, M. (eds.): Proceedings of the ECAI 2010—19th European Conference on Artificial Intelligence, Lisbon, Portugal, August 16-20, 2010. IOS Press, Amsterdam (2010) · Zbl 1207.68003
[30] 30. Cook, S.A.: The complexity of theorem-proving procedures. In: Harrison, M.A., Banerji, R.B., Ullman, J.D. (eds.) Annual Symp. on Theory of Computing (STOC), pp. 151-158. ACM, New York (1971)
[31] 31. Crawford, J.M., Auton, L.D.: Experimental results on the crossover point in satisfiability problems. In: Fikes, R., Lehnert, W.G. (eds.) National Conference on Artificial Intelligence (AAAI), pp. 21-27. AAAI Press/MIT Press, Palo Alto/Cambridge (1993)
[32] 32. Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394-397 (1962) · Zbl 0217.54002
[33] 33. Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201-215 (1960) · Zbl 0212.34203
[34] 34. Dechter, R. (ed.): Principles and Practice of Constraint Programming—CP 2000, Proceedings of the 6th International Conference, Singapore, September 18-21, 2000. LNCS, vol. 1894. Springer, Heidelberg (2000) · Zbl 0947.00041
[35] 35. Dershowitz, N., Hanna, Z., Nadel, A.: A scalable algorithm for minimal unsatisfiable core extraction. In: Biere, A., Gomes, C.P. (eds.) Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 4121, pp. 36-41. Springer, Heidelberg (2006) · Zbl 1187.68538
[36] 36. Dubois, O., André, P., Boufkhad, Y., Carlier, J.: SAT versus UNSAT. In: Johnson, D.S., Trick, M. (eds.) Cliques, Coloring and Satisfiability: Second DIMACS Implementation Challenge. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, pp. 415-436. AMS, Providence (1996) · Zbl 0864.90090
[37] 37. Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 3569, pp. 61-75. Springer, Heidelberg (2005) · Zbl 1128.68463
[38] 38. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 2919, pp. 502-518. Springer, Heidelberg (2003)
[39] 39. Eén, N., Sörensson, N.: Translating pseudo-boolean constraints into SAT. J. Satisf. Boolean Model. Comput. 2(1-4), 1-26 (2006)
[40] 40. Freeman, J.W.: Improvements to propositional satisfiability search algorithms. Ph.D. thesis, University of Pennsylvania (1995)
[41] 41. Frisch, A.M., Peugniez, T.J.: Solving non-boolean satisfiability problems with stochastic local search. In: Nebel, B. (ed.) Intl. Joint Conf. on Artificial Intelligence (IJCAI), pp. 282-290. Morgan Kaufmann, Cambridge (2001)
[42] 42. Fujiwara, H., Shimono, T.: On the acceleration of test generation algorithms. Trans. Comput. 32(12), 1137-1144 (1983)
[43] 43. Giunchiglia, E., Marin, P., Narizzano, M.: Reasoning with quantified boolean formulas. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 761-780. IOS Press, Amsterdam (2009)
[44] 44. Goldberg, E.I., Novikov, Y.: BerkMin: a fast and robust Sat-solver. In: Design, Automation & Test in Europe (DATE), pp. 142-149. IEEE, Piscataway (2002) · Zbl 1121.68106
[45] 45. Gomes, C.P., Selman, B., Kautz, H.A.: Boosting combinatorial search through randomization. In: Mostow, J., Rich, C. (eds.) National Conference on Artificial Intelligence (AAAI), pp. 431-437. AAAI Press/MIT Press, Palo Alto/Cambridge (1998)
[46] 46. Grégoire, É., Mazure, B., Piette, C.: On approaches to explaining infeasibility of sets of boolean clauses. In: Intl. Conf. on Tools with Artificial Intelligence (ICTAI), vol. 1, pp. 74-83. IEEE, Piscataway (2008)
[47] 47. Guo, L., Hamadi, Y., Jabbour, S., Sais, L.: Diversification and intensification in parallel SAT solving. In: Cohen, D. (ed.) Intl. Conf. on Principles and Practice of Constraint Programming (CP). LNCS, vol. 6308, pp. 252-265. Springer, Heidelberg (2010)
[48] 48. Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a parallel SAT solver. J. Satisf. Boolean Model. Comput. 6(4), 245-262 (2009) · Zbl 1193.68227
[49] 49. Hamadi, Y., Wintersteiger, C.M.: Seven challenges in parallel SAT solving. AI Mag. 34(2), 99-106 (2013)
[50] 50. Hemery, F., Lecoutre, C., Sais, L., Boussemart, F.: Extracting MUCs from constraint networks. In: Brewka, G., Coradeschi, S., Perini, A., Traverso, P. (eds.) European Conf. on Artificial Intelligence (ECAI), pp. 113-117. IOS Press, Amsterdam (2006)
[51] 51. Heras, F., Larrosa, J., Oliveras, A.: MiniMaxSAT: an efficient weighted Max-SAT solver. J. Artif. Intell. Res. 31, 1-32 (2008) · Zbl 1183.68578
[52] 52. Huang, J.: The effect of restarts on the efficiency of clause learning. In: Veloso, M.M. (ed.) Intl. Joint Conf. on Artificial Intelligence (IJCAI), pp. 2318-2323 (2007)
[53] 53. Huang, J.: Extended clause learning. Artif. Intell. 174(15), 1277-1284 (2010) · Zbl 1210.68082
[54] 54. Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: Intl. Symp. on Software Testing and Analysis (ISSTA), pp. 14-25. ACM, New York (2000)
[55] 55. Janhunen, T., Niemelä, I.: Compact translations of non-disjunctive answer set programs to propositional clauses. In: Balduccini, M., Son, T.C. (eds.) Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning—Essays Dedicated to Michael Gelfond on the Occasion of His 65th Birthday. Lecture Notes in Artificial Intelligence, vol. 6565, pp. 111-130. Springer, Heidelberg (2011) · Zbl 1326.68058
[56] 56. Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.M.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 7317, pp. 114-128. Springer, Heidelberg (2012) · Zbl 1273.68178
[57] 57. Järvisalo, M., Biere, A., Heule, M.: Simulating circuit-level simplifications on CNF. J. Autom. Reason. 49(4), 583-619 (2012) · Zbl 1267.94144
[58] 58. Järvisalo, M., Heule, M., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Intl. Joint Conf. on Automated Reasoning (IJCAR). LNCS, vol. 7364, pp. 355-370. Springer, Heidelberg (2012) · Zbl 1358.68256
[59] 59. Jin, H., Han, H., Somenzi, F.: Efficient conflict analysis for finding all satisfying assignments of a boolean circuit. In: Halbwachs, N., Zuck, L.D. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 3440, pp. 287-300. Springer, Heidelberg (2005) · Zbl 1087.68631
[60] 60. Junker, U.: QuickXplain: preferred explanations and relaxations for over-constrained problems. In: McGuinness, D.L., Ferguson, G. (eds.) National Conference on Artificial Intelligence (AAAI), pp. 167-172. AAAI Press/MIT Press, Palo Alto/Cambridge (2004)
[61] 61. Kautz, H.A., Selman, B.: Planning as satisfiability. In: Neumann, B. (ed.) European Conf. on Artificial Intelligence (ECAI), pp. 359-363. Wiley, New York (1992)
[62] 62. Kleine-Büning, H., Letterman, T.: Propositional Logic: Deduction and Algorithms. Cambridge University Press, Cambridge (1999)
[63] 63. Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Springer, Heidelberg (2008) · Zbl 1149.68071
[64] 64. Kullmann, O. (ed.): Theory and Applications of Satisfiability Testing—SAT 2009, Proceedings of the 12th International Conference, SAT 2009, Swansea, UK, June 30-July 3, 2009. LNCS, vol. 5584. Springer, Heidelberg (2009) · Zbl 1165.68014
[65] 65. Laitinen, T., Junttila, T.A., Niemelä, I.: Extending clause learning DPLL with parity reasoning. In: Coelho et al. [61], pp. 21-26 · Zbl 1211.68385
[66] 66. Li, C.M., Manyà, F.: MaxSAT, hard and soft constraints. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 613-631. IOS Press, Amsterdam (2009)
[67] 67. Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. 40(1), 1-33 (2008) · Zbl 1154.68510
[68] 68. Lynce, I., Baptista, L., Marques-Silva, J.: Towards provably complete stochastic search algorithms for satisfiability. In: Brazdil, P., Jorge, A. (eds.) Portuguese Conf. on Artificial Intelligence (EPIA). LNCS, vol. 2258, pp. 363-370. Springer, Heidelberg (2001) · Zbl 1053.68684
[69] 69. Lynce, I., Marques-Silva, J.: Probing-based preprocessing techniques for propositional satisfiability. In: Intl. Conf. on Tools with Artificial Intelligence (ICTAI), pp. 105-110. IEEE, Piscataway (2003)
[70] 70. Lynce, I., Marques-Silva, J.: Efficient data structures for backtrack search SAT solvers. Ann. Math. Artif. Intell. 43(1), 137-152 (2005) · Zbl 1099.68025
[71] 71. Manquinho, V.M., Marques-Silva, J.: Satisfiability-based algorithms for boolean optimization. Ann. Math. Artif. Intell. 40(3-4), 353-372 (2004) · Zbl 1068.90081
[72] 72. Marques-Silva, J.: Search algorithms for satisfiability problems in combinational switching circuits. Ph.D. thesis, University of Michigan (1995)
[73] 73. Marques-Silva, J.: The impact of branching heuristics in propositional satisfiability algorithms. In: Barahona, P., Alferes, J.J. (eds.) Portuguese Conf. on Artificial Intelligence (EPIA). LNCS, vol. 1695, pp. 62-74. Springer, Heidelberg (1999)
[74] 74. Marques-Silva, J.: Algebraic simplification techniques for propositional satisfiability. In: Dechter [107], pp. 537-542 · Zbl 1044.68781
[75] 75. Marques-Silva, J., Heras, F., Janota, M., Previti, A., Belov, A.: On computing minimal correction subsets. In: Rossi, F. (ed.) Intl. Joint Conf. on Artificial Intelligence (IJCAI), pp. 615-622. IJCAI/AAAI, Melbourne/Palo Alto (2013)
[76] 76. Marques-Silva, J., Janota, M., Belov, A.: Minimal sets over monotone predicates in boolean formulae. In: Sharygina, N., Veith, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 8044, pp. 592-607. Springer, Heidelberg (2013)
[77] 77. Marques-Silva, J., Janota, M., Lynce, I.: On computing backbones of propositional theories. In: Coelho et al. [54], pp. 15-20 · Zbl 1211.68389
[78] 78. Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 131-153. IOS Press, Amsterdam (2009)
[79] 79. Marques-Silva, J., Sakallah, K.A.: Dynamic search-space pruning techniques in path sensitization. In: Lorenzetti, M.J. (ed.) Design Automation Conf. (DAC), pp. 705-711. ACM, New York (1994)
[80] 80. Marques-Silva, J., Sakallah, K.A.: GRASP—a new search algorithm for satisfiability. In: Rutenbar, R.A., Otten, R.H.J.M. (eds.) Intl. Conf. on Computer-Aided Design (ICCAD), pp. 220-227. IEEE/ACM, Piscataway/New York (1996)
[81] 81. Marques-Silva, J., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. Trans. Comput. 48(5), 506-521 (1999) · Zbl 1392.68388
[82] 82. Marques-Silva, J., Sakallah, K.A. (eds.): Theory and Applications of Satisfiability Testing—SAT 2007, Proceedings of the 10th International Conference, Lisbon, Portugal, May 28-31, 2007. LNCS, vol. 4501. Springer, Heidelberg (2007)
[83] 83. McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2404, pp. 250-264. Springer, Heidelberg (2002) · Zbl 1010.68509
[84] 84. McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A. Jr., Somenzi, F. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2725, pp. 1-13. Springer, Heidelberg (2003) · Zbl 1278.68184
[85] 85. Morgado, A., Heras, F., Liffiton, M.H., Planes, J., Marques-Silva, J.: Iterative and core-guided MaxSAT solving: a survey and assessment. Constraints 18(4), 478-534 (2013) · Zbl 1317.90199
[86] 86. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Design Automation Conf. (DAC), pp. 530-535. ACM, New York (2001)
[87] 87. Nam, G.J., Sakallah, K.A., Rutenbar, R.A.: Satisfiability-based detailed FPGA routing. In: Intl. Conf. on VLSI Design, pp. 574-577. IEEE, Piscataway (1999)
[88] 88. Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL( · Zbl 1326.68164
[89] 89. Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva and Sakallah [33], pp. 294-299
[90] 90. Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2(3), 293-304 (1986) · Zbl 0636.68119
[91] 91. Prestwich, S.D.: Variable dependency in local search: prevention is better than cure. In: Marques-Silva and Sakallah [32], pp. 107-120 · Zbl 1214.68369
[92] 92. Prestwich, S.D.: CNF encodings. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 75-97. IOS Press, Amsterdam (2009)
[93] 93. Ravi, K., Somenzi, F.: Minimal assignments for bounded model checking. In: Jensen, K., Podelski, A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 2988, pp. 31-45. Springer, Heidelberg (2004) · Zbl 1126.68486
[94] 94. Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23-41 (1965) · Zbl 0139.12303
[95] 95. Roussel, O., Manquinho, V.M.: Pseudo-boolean and cardinality constraints. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 695-733. IOS Press, Amsterdam (2009)
[96] 96. Sabharwal, A., Samulowitz, H., Sellmann, M.: Learning back-clauses in SAT. In: Cimatti, A., Sebastiani, R. (eds.) Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 7317, pp. 498-499. Springer, Heidelberg (2012)
[97] 97. Schulz, M.H., Trischler, E., Sarfert, T.M.: SOCRATES: a highly efficient automatic test pattern generation system. Trans. Comput.-Aided Des. Integr. Circuits Syst. 7(1), 126-137 (1988)
[98] 98. Selman, B., Kautz, H., Cohen, B.: Local search strategies for satisfiability testing. In: Johnson, D.S., Trick, M. (eds.) Cliques, Coloring and Satisfiability: Second DIMACS Implementation Challenge. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, pp. 521-532. AMS, Providence (1996) · Zbl 0864.90093
[99] 99. Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt, W.A. Jr., Johnson, S.D. (eds.) Formal Methods in Computer Aided Design (FMCAD). LNCS, vol. 1954, pp. 108-125. Springer, Heidelberg (2000)
[100] 100. Sheeran, M., Stålmarck, G.: A tutorial on Stålmarck’s proof procedure for propositional logic. Form. Methods Syst. Des. 16(1), 23-58 (2000)
[101] 101. Shlyakhter, I., Seater, R., Jackson, D., Sridharan, M., Taghdiri, M.: Debugging overconstrained declarative models using unsatisfiable cores. In: Intl. Conf. on Automated Software Engineering (ASE), pp. 94-105. IEEE, Piscataway (2003)
[102] 102. Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: van Beek, P. (ed.) Intl. Conf. on Principles and Practice of Constraint Programming (CP). LNCS, vol. 3709, pp. 827-831. Springer, Heidelberg (2005) · Zbl 1153.68488
[103] 103. Sinz, C., Iser, M.: Problem-sensitive restart heuristics for the DPLL procedure. In: Kullmann [98], pp. 356-362
[104] 104. de Siqueira, J.L.N., Puget, J.F.: Explanation-based generalisation of failures. In: Kodratoff, Y. (ed.) European Conf. on Artificial Intelligence (ECAI), pp. 339-344. Pitman, London (1988)
[105] 105. Sörensson, N., Biere, A.: Minimizing learned clauses. In: Kullmann [25], pp. 237-243
[106] 106. Stallman, R.M., Sussman, G.J.: Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artif. Intell. 9(2), 135-196 (1977) · Zbl 0372.94024
[107] 107. Stephan, P.R., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: Combinational test generation using satisfiability. Trans. Comput.-Aided Des. Integr. Circuits Syst. 15(9), 1167-1176 (1996)
[108] 108. Stuckey, P.J.: There are no CNF problems. In: Järvisalo, M., Gelder, A.V. (eds.) Theory and Applications of Satisfiability Testing (SAT). LNCS, vol. 7962, pp. 19-21. Springer, Heidelberg (2013)
[109] 109. Tarjan, R.E.: Finding dominators in directed graphs. SIAM J. Comput. 3(1), 62-89 (1974) · Zbl 0296.68030
[110] 110. Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Silenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part II, pp. 115-125. Springer, Heidelberg (1968) · Zbl 0197.00102
[111] 111. Urquhart, A.: The complexity of propositional proofs. Bull. Symb. Log. 1(4), 425-467 (1995) · Zbl 0845.03025
[112] 112. Van Gelder, A., Tsuji, Y.K.: Satisfiability testing with more reasoning and less guessing. Tech. rep., University of California at Santa Cruz (1995) · Zbl 0868.03007
[113] 113. Warners, J.P.: A linear-time transformation of linear inequalities into conjunctive normal form. Inf. Process. Lett. 68(2), 63-69 (1998) · Zbl 1339.68244
[114] 114. Wieringa, S.: Understanding, improving and parallelizing MUS finding using model rotation. In: Milano, M. (ed.) Intl. Conf. on Principles and Practice of Constraint Programming (CP). LNCS, vol. 7514, pp. 672-687. Springer, Heidelberg (2012)
[115] 115. Wolfram, D.A.: Forward checking and intelligent backtracking. Inf. Process. Lett. 32(2), 85-87 (1989) · Zbl 0688.68048
[116] 116. Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: SATzilla: Portfolio-based algorithm selection for SAT. J. Artif. Intell. Res. 32, 565-606 (2008) · Zbl 1182.68272
[117] 117. Zabih, R., McAllester, D.A.: A rearrangement search strategy for determining propositional satisfiability. In: Shrobe, H.E., Mitchell, T.M., Smith, R.G. (eds.) National Conference on Artificial Intelligence (AAAI), pp. 155-160. AAAI Press/MIT Press, Palo Alto/Cambridge (1988)
[118] 118. Zhang, H.: SATO: an efficient propositional prover. In: McCune, W. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol. 1249, pp. 272-275. Springer, Heidelberg (1997)
[119] 119. Zhang, H., Stickel, M.E.: Implementing the Davis-Putnam method. J. Autom. Reason. 24(1/2), 277-296 (2000) · Zbl 0967.68148
[120] 120. Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: Design, Automation & Test in Europe (DATE), pp. 10,880-10,885. IEEE, Piscataway (2003)
[121] 121. Zhu, C.S., Weissenbacher, G., Sethi, D., Malik, S.: SAT-based techniques for determining backbones for post-silicon fault localisation. In: Zilic, Z., Shukla, S.K. (eds.) Intl. High Level Design Validation and Test Workshop (HLDVT), pp. 84-91. IEEE, Piscataway (2011)
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.