{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:50:13Z","timestamp":1762102213436},"publisher-location":"Cham","reference-count":121,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319105741"},{"type":"electronic","value":"9783319105758"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_9","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"247-275","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Propositional SAT Solving"],"prefix":"10.1007","author":[{"given":"Joao","family":"Marques-Silva","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1613\/jair.3653","volume":"45","author":"I. Ab\u00edo","year":"2012","unstructured":"Ab\u00edo, I., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Mayer-Eichberger, V.: A\u00a0new look at BDDs for pseudo-boolean constraints. J.\u00a0Artif. Intell. Res. 45, 443\u2013480 (2012)","journal-title":"J.\u00a0Artif. Intell. Res."},{"issue":"2\u20133","key":"9_CR2","doi-asserted-by":"crossref","first-page":"145","DOI":"10.3233\/AIC-2010-0462","volume":"23","author":"R.J.A. Ach\u00e1","year":"2010","unstructured":"Ach\u00e1, R.J.A., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Practical algorithms for unsatisfiability proof and core generation in SAT solvers. AI Commun. 23(2\u20133), 145\u2013157 (2010)","journal-title":"AI Commun."},{"key":"9_CR3","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/j.artint.2013.01.002","volume":"196","author":"C. Ans\u00f3tegui","year":"2013","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J.: SAT-based MaxSAT algorithms. Artif. Intell. 196, 77\u2013105 (2013)","journal-title":"Artif. Intell."},{"issue":"2","key":"9_CR4","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/s10601-010-9105-0","volume":"16","author":"R. As\u00edn","year":"2011","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Cardinality networks: a\u00a0theoretical and empirical study. Constraints 16(2), 195\u2013221 (2011)","journal-title":"Constraints"},{"key":"9_CR5","first-page":"15","volume-title":"AAAI Conf. on Artificial Intelligence (AAAI)","author":"G. Audemard","year":"2010","unstructured":"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.\u00a015\u201320. AAAI Press, Palo Alto (2010)"},{"key":"9_CR6","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"630","DOI":"10.1007\/978-3-540-85958-1_55","volume-title":"Intl. Conf. on Principles and Practice of Constraint Programming (CP)","author":"G. Audemard","year":"2008","unstructured":"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.\u00a05202, pp.\u00a0630\u2013634. Springer, Heidelberg (2008)"},{"key":"9_CR7","first-page":"399","volume-title":"Intl. Joint Conf. on Artificial Intelligence (IJCAI)","author":"G. Audemard","year":"2009","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) Intl. Joint Conf. on Artificial Intelligence (IJCAI), pp.\u00a0399\u2013404. IJCAI\/AAAI Press, Melbourne\/Palo Alto (2009)"},{"key":"9_CR8","series-title":"LNCS","first-page":"181","volume-title":"Theory and Applications of Satisfiability Testing (SAT)","author":"O. Bailleux","year":"2009","unstructured":"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.\u00a05584, pp.\u00a0181\u2013194. Springer, Heidelberg (2009)"},{"key":"9_CR9","first-page":"288","volume-title":"National Conference on Artificial Intelligence (AAAI)","author":"A.B. Baker","year":"1994","unstructured":"Baker, A.B.: The hazards of fancy backtracking. In: Hayes-Roth, B., Korf, R.E. (eds.) National Conference on Artificial Intelligence (AAAI), pp.\u00a0288\u2013293. AAAI Press\/MIT Press, Palo Alto\/Cambridge (1994)"},{"key":"9_CR10","first-page":"276","volume-title":"Intl. Joint Conf. on Artificial Intelligence (IJCAI)","author":"R.R. Bakker","year":"1993","unstructured":"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.\u00a0276\u2013281. Morgan Kaufmann, Cambridge (1993)"},{"key":"9_CR11","doi-asserted-by":"crossref","first-page":"489","DOI":"10.1007\/3-540-45349-0_36","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2000","author":"Lu\u00eds Baptista","year":"2000","unstructured":"Baptista, L., Marques-Silva, J.: Using randomization and learning to solve hard real-world instances of satisfiability. In: Dechter [30], pp.\u00a0489\u2013494"},{"key":"9_CR12","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"825","volume-title":"Handbook of Satisfiability","author":"C.W. Barrett","year":"2009","unstructured":"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.\u00a0185, pp.\u00a0825\u2013885. IOS Press, Amsterdam (2009)"},{"key":"9_CR13","series-title":"AFIPS Conference Proceedings","first-page":"307","volume-title":"AFIPS Spring Joint Computer Conference","author":"K.E. Batcher","year":"1968","unstructured":"Batcher, K.E.: Sorting networks and their applications. In: AFIPS Spring Joint Computer Conference. AFIPS Conference Proceedings, vol.\u00a032, pp.\u00a0307\u2013314. Thomson Book Co., Washington D.C. (1968)"},{"key":"9_CR14","first-page":"203","volume-title":"National Conference on Artificial Intelligence (AAAI)","author":"R.J. Bayardo Jr.","year":"1997","unstructured":"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.\u00a0203\u2013208. AAAI Press\/MIT Press, Palo Alto\/Cambridge (1997)"},{"key":"9_CR15","doi-asserted-by":"crossref","first-page":"1411","DOI":"10.7873\/DATE.2013.288","volume-title":"Design, Automation & Test in Europe (DATE)","author":"A. Belov","year":"2013","unstructured":"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.\u00a01411\u20131416. EDA Consortium\/ACM, San Jose\/New York (2013)"},{"issue":"2","key":"9_CR16","doi-asserted-by":"crossref","first-page":"97","DOI":"10.3233\/AIC-2012-0523","volume":"25","author":"A. Belov","year":"2012","unstructured":"Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun. 25(2), 97\u2013116 (2012)","journal-title":"AI Commun."},{"issue":"1","key":"9_CR17","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/BF02136172","volume":"18","author":"R. Ben-Eliyahu","year":"1996","unstructured":"Ben-Eliyahu, R., Dechter, R.: On computing minimal models. Ann. Math. Artif. Intell. 18(1), 3\u201327 (1996)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"2","key":"9_CR18","doi-asserted-by":"crossref","first-page":"421","DOI":"10.1016\/S0004-3702(97)00060-X","volume":"96","author":"R. Ben-Eliyahu-Zohary","year":"1997","unstructured":"Ben-Eliyahu-Zohary, R., Palopoli, L.: Reasoning with minimal models: efficient algorithms and applications. Artif. Intell. 96(2), 421\u2013449 (1997)","journal-title":"Artif. Intell."},{"issue":"2\u20134","key":"9_CR19","first-page":"75","volume":"4","author":"A. Biere","year":"2008","unstructured":"Biere, A.: PicoSAT essentials. J.\u00a0Satisf. Boolean Model. Comput. 4(2\u20134), 75\u201397 (2008)","journal-title":"J.\u00a0Satisf. Boolean Model. Comput."},{"key":"9_CR20","series-title":"LNCS","first-page":"193","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"A. Biere","year":"1999","unstructured":"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.\u00a01579, pp.\u00a0193\u2013207. Springer, Heidelberg (1999)"},{"key":"9_CR21","series-title":"Frontiers in Artificial Intelligence and Applications","volume-title":"Handbook of Satisfiability","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press, Amsterdam (2009)"},{"key":"9_CR22","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","author":"A.R. Bradley","year":"2011","unstructured":"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.\u00a06538, pp.\u00a070\u201387. Springer, Heidelberg (2011)"},{"issue":"4\u20135","key":"9_CR23","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/s00165-008-0080-9","volume":"20","author":"A.R. Bradley","year":"2008","unstructured":"Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Form. Asp. Comput. 20(4\u20135), 379\u2013405 (2008)","journal-title":"Form. Asp. Comput."},{"issue":"1","key":"9_CR24","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/TSMCB.2002.805807","volume":"34","author":"R.I. Brafman","year":"2004","unstructured":"Brafman, R.I.: A simplifier for propositional formulas with many binary clauses. IEEE Trans. Syst. Man Cybern., Part B, Cybern. 34(1), 52\u201359 (2004)","journal-title":"IEEE Trans. Syst. Man Cybern., Part B, Cybern."},{"issue":"8","key":"9_CR25","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"Trans. Comput."},{"key":"9_CR26","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"735","volume-title":"Handbook of Satisfiability","author":"H.K. B\u00fcning","year":"2009","unstructured":"B\u00fcning, 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.\u00a0185, pp.\u00a0735\u2013760. IOS Press, Amsterdam (2009)"},{"key":"9_CR27","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"339","volume-title":"Handbook of Satisfiability","author":"H.K. B\u00fcning","year":"2009","unstructured":"B\u00fcning, 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.\u00a0185, pp.\u00a0339\u2013401. IOS Press, Amsterdam (2009)"},{"issue":"2","key":"9_CR28","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1287\/ijoc.3.2.157","volume":"3","author":"J.W. Chinneck","year":"1991","unstructured":"Chinneck, J.W., Dravnieks, E.W.: Locating minimal infeasible constraint sets in linear programs. INFORMS J. Comput. 3(2), 157\u2013168 (1991)","journal-title":"INFORMS J. Comput."},{"volume-title":"Proceedings of the ECAI 2010\u201419th European Conference on Artificial Intelligence","year":"2010","unstructured":"Coelho, H., Studer, R., Wooldridge, M. (eds.): Proceedings of the ECAI 2010\u201419th European Conference on Artificial Intelligence, Lisbon, Portugal, August 16\u201320, 2010. IOS Press, Amsterdam (2010)","key":"9_CR29"},{"key":"9_CR30","first-page":"151","volume-title":"Annual Symp. on Theory of Computing (STOC)","author":"S.A. Cook","year":"1971","unstructured":"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.\u00a0151\u2013158. ACM, New York (1971)"},{"key":"9_CR31","first-page":"21","volume-title":"National Conference on Artificial Intelligence (AAAI)","author":"J.M. Crawford","year":"1993","unstructured":"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.\u00a021\u201327. AAAI Press\/MIT Press, Palo Alto\/Cambridge (1993)"},{"issue":"7","key":"9_CR32","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"issue":"3","key":"9_CR33","first-page":"201","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J.\u00a0ACM 7(3), 201\u2013215 (1960)","journal-title":"J.\u00a0ACM"},{"key":"9_CR34","series-title":"LNCS","volume-title":"Principles and Practice of Constraint Programming\u2014CP 2000, Proceedings of the 6th International Conference","year":"2000","unstructured":"Dechter, R. (ed.): Principles and Practice of Constraint Programming\u2014CP 2000, Proceedings of the 6th International Conference, Singapore, September 18\u201321, 2000. LNCS, vol.\u00a01894. Springer, Heidelberg (2000)"},{"key":"9_CR35","series-title":"LNCS","first-page":"36","volume-title":"Theory and Applications of Satisfiability Testing (SAT)","author":"N. Dershowitz","year":"2006","unstructured":"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.\u00a04121, pp.\u00a036\u201341. Springer, Heidelberg (2006)"},{"key":"9_CR36","series-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1090\/dimacs\/026\/20","volume-title":"Cliques, Coloring and Satisfiability: Second DIMACS Implementation Challenge","author":"O. Dubois","year":"1996","unstructured":"Dubois, O., Andr\u00e9, 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.\u00a026, pp.\u00a0415\u2013436. AMS, Providence (1996)"},{"key":"9_CR37","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing (SAT)","author":"N. E\u00e9n","year":"2005","unstructured":"E\u00e9n, 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.\u00a03569, pp.\u00a061\u201375. Springer, Heidelberg (2005)"},{"key":"9_CR38","series-title":"LNCS","first-page":"502","volume-title":"Theory and Applications of Satisfiability Testing (SAT)","author":"N. E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) Theory and Applications of Satisfiability Testing (SAT). LNCS, vol.\u00a02919, pp.\u00a0502\u2013518. Springer, Heidelberg (2003)"},{"issue":"1\u20134","key":"9_CR39","first-page":"1","volume":"2","author":"N. E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-boolean constraints into SAT. J.\u00a0Satisf. Boolean Model. Comput. 2(1\u20134), 1\u201326 (2006)","journal-title":"J.\u00a0Satisf. Boolean Model. Comput."},{"unstructured":"Freeman, J.W.: Improvements to propositional satisfiability search algorithms. Ph.D. thesis, University of Pennsylvania (1995)","key":"9_CR40"},{"key":"9_CR41","first-page":"282","volume-title":"Intl. Joint Conf. on Artificial Intelligence (IJCAI)","author":"A.M. Frisch","year":"2001","unstructured":"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.\u00a0282\u2013290. Morgan Kaufmann, Cambridge (2001)"},{"issue":"12","key":"9_CR42","doi-asserted-by":"crossref","first-page":"1137","DOI":"10.1109\/TC.1983.1676174","volume":"32","author":"H. Fujiwara","year":"1983","unstructured":"Fujiwara, H., Shimono, T.: On the acceleration of test generation algorithms. Trans. Comput. 32(12), 1137\u20131144 (1983)","journal-title":"Trans. Comput."},{"key":"9_CR43","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"761","volume-title":"Handbook of Satisfiability","author":"E. Giunchiglia","year":"2009","unstructured":"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.\u00a0185, pp.\u00a0761\u2013780. IOS Press, Amsterdam (2009)"},{"key":"9_CR44","first-page":"142","volume-title":"Design, Automation & Test in Europe (DATE)","author":"E.I. Goldberg","year":"2002","unstructured":"Goldberg, E.I., Novikov, Y.: BerkMin: a fast and robust Sat-solver. In: Design, Automation & Test in Europe (DATE), pp.\u00a0142\u2013149. IEEE, Piscataway (2002)"},{"key":"9_CR45","first-page":"431","volume-title":"National Conference on Artificial Intelligence (AAAI)","author":"C.P. Gomes","year":"1998","unstructured":"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.\u00a0431\u2013437. AAAI Press\/MIT Press, Palo Alto\/Cambridge (1998)"},{"key":"9_CR46","first-page":"74","volume-title":"Intl. Conf. on Tools with Artificial Intelligence (ICTAI)","author":"\u00c9. Gr\u00e9goire","year":"2008","unstructured":"Gr\u00e9goire, \u00c9., Mazure, B., Piette, C.: On approaches to explaining infeasibility of sets of boolean clauses. In: Intl. Conf. on Tools with Artificial Intelligence (ICTAI), vol.\u00a01, pp.\u00a074\u201383. IEEE, Piscataway (2008)"},{"key":"9_CR47","series-title":"LNCS","first-page":"252","volume-title":"Intl. Conf. on Principles and Practice of Constraint Programming (CP)","author":"L. Guo","year":"2010","unstructured":"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.\u00a06308, pp.\u00a0252\u2013265. Springer, Heidelberg (2010)"},{"issue":"4","key":"9_CR48","first-page":"245","volume":"6","author":"Y. Hamadi","year":"2009","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a parallel SAT solver. J.\u00a0Satisf. Boolean Model. Comput. 6(4), 245\u2013262 (2009)","journal-title":"J.\u00a0Satisf. Boolean Model. Comput."},{"issue":"2","key":"9_CR49","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1609\/aimag.v34i2.2450","volume":"34","author":"Y. Hamadi","year":"2013","unstructured":"Hamadi, Y., Wintersteiger, C.M.: Seven challenges in parallel SAT solving. AI Mag. 34(2), 99\u2013106 (2013)","journal-title":"AI Mag."},{"key":"9_CR50","first-page":"113","volume-title":"European Conf. on Artificial Intelligence (ECAI)","author":"F. Hemery","year":"2006","unstructured":"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.\u00a0113\u2013117. IOS Press, Amsterdam (2006)"},{"key":"9_CR51","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1111\/j.1365-2788.1987.tb01337.x","volume":"31","author":"F. Heras","year":"2008","unstructured":"Heras, F., Larrosa, J., Oliveras, A.: MiniMaxSAT: an efficient weighted Max-SAT solver. J.\u00a0Artif. Intell. Res. 31, 1\u201332 (2008)","journal-title":"J.\u00a0Artif. Intell. Res."},{"key":"9_CR52","first-page":"2318","volume-title":"Intl. Joint Conf. on Artificial Intelligence (IJCAI)","author":"J. Huang","year":"2007","unstructured":"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.\u00a02318\u20132323 (2007)"},{"issue":"15","key":"9_CR53","doi-asserted-by":"crossref","first-page":"1277","DOI":"10.1016\/j.artint.2010.07.008","volume":"174","author":"J. Huang","year":"2010","unstructured":"Huang, J.: Extended clause learning. Artif. Intell. 174(15), 1277\u20131284 (2010)","journal-title":"Artif. Intell."},{"key":"9_CR54","first-page":"14","volume-title":"Intl. Symp. on Software Testing and Analysis (ISSTA)","author":"D. Jackson","year":"2000","unstructured":"Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: Intl. Symp. on Software Testing and Analysis (ISSTA), pp.\u00a014\u201325. ACM, New York (2000)"},{"key":"9_CR55","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/978-3-642-20832-4_8","volume-title":"Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning\u2014Essays Dedicated to Michael Gelfond on the Occasion of His 65th Birthday","author":"T. Janhunen","year":"2011","unstructured":"Janhunen, T., Niemel\u00e4, 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\u2014Essays Dedicated to Michael Gelfond on the Occasion of His 65th Birthday. Lecture Notes in Artificial Intelligence, vol.\u00a06565, pp.\u00a0111\u2013130. Springer, Heidelberg (2011)"},{"key":"9_CR56","series-title":"LNCS","first-page":"114","volume-title":"Theory and Applications of Satisfiability Testing (SAT)","author":"M. Janota","year":"2012","unstructured":"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.\u00a07317, pp.\u00a0114\u2013128. Springer, Heidelberg (2012)"},{"issue":"4","key":"9_CR57","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1007\/s10817-011-9239-9","volume":"49","author":"M. J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.: Simulating circuit-level simplifications on CNF. J.\u00a0Autom. Reason. 49(4), 583\u2013619 (2012)","journal-title":"J.\u00a0Autom. Reason."},{"key":"9_CR58","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Intl. Joint Conf. on Automated Reasoning (IJCAR)","author":"M. J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Intl. Joint Conf. on Automated Reasoning (IJCAR). LNCS, vol.\u00a07364, pp.\u00a0355\u2013370. Springer, Heidelberg (2012)"},{"key":"9_CR59","series-title":"LNCS","first-page":"287","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"H. Jin","year":"2005","unstructured":"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.\u00a03440, pp.\u00a0287\u2013300. Springer, Heidelberg (2005)"},{"key":"9_CR60","first-page":"167","volume-title":"National Conference on Artificial Intelligence (AAAI)","author":"U. Junker","year":"2004","unstructured":"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.\u00a0167\u2013172. AAAI Press\/MIT Press, Palo Alto\/Cambridge (2004)"},{"key":"9_CR61","first-page":"359","volume-title":"European Conf. on Artificial Intelligence (ECAI)","author":"H.A. Kautz","year":"1992","unstructured":"Kautz, H.A., Selman, B.: Planning as satisfiability. In: Neumann, B. (ed.) European Conf. on Artificial Intelligence (ECAI), pp.\u00a0359\u2013363. Wiley, New York (1992)"},{"key":"9_CR62","volume-title":"Propositional Logic: Deduction and Algorithms","author":"H. Kleine-B\u00fcning","year":"1999","unstructured":"Kleine-B\u00fcning, H., Letterman, T.: Propositional Logic: Deduction and Algorithms. Cambridge University Press, Cambridge (1999)"},{"key":"9_CR63","volume-title":"Decision Procedures: An Algorithmic Point of View","author":"D. Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Springer, Heidelberg (2008)"},{"key":"9_CR64","series-title":"LNCS","volume-title":"Theory and Applications of Satisfiability Testing\u2014SAT 2009, Proceedings of the 12th International Conference, SAT 2009","year":"2009","unstructured":"Kullmann, O. (ed.): Theory and Applications of Satisfiability Testing\u2014SAT 2009, Proceedings of the 12th International Conference, SAT 2009, Swansea, UK, June 30\u2013July 3, 2009. LNCS, vol.\u00a05584. Springer, Heidelberg (2009)"},{"unstructured":"Laitinen, T., Junttila, T.A., Niemel\u00e4, I.: Extending clause learning DPLL with parity reasoning. In: Coelho et al. [61], pp.\u00a021\u201326","key":"9_CR65"},{"key":"9_CR66","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"613","volume-title":"Handbook of Satisfiability","author":"C.M. Li","year":"2009","unstructured":"Li, C.M., Many\u00e0, 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.\u00a0185, pp.\u00a0613\u2013631. IOS Press, Amsterdam (2009)"},{"issue":"1","key":"9_CR67","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"M.H. Liffiton","year":"2008","unstructured":"Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J.\u00a0Autom. Reason. 40(1), 1\u201333 (2008)","journal-title":"J.\u00a0Autom. Reason."},{"key":"9_CR68","series-title":"LNCS","first-page":"363","volume-title":"Portuguese Conf. on Artificial Intelligence (EPIA)","author":"I. Lynce","year":"2001","unstructured":"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.\u00a02258, pp.\u00a0363\u2013370. Springer, Heidelberg (2001)"},{"key":"9_CR69","first-page":"105","volume-title":"Intl. Conf. on Tools with Artificial Intelligence (ICTAI)","author":"I. Lynce","year":"2003","unstructured":"Lynce, I., Marques-Silva, J.: Probing-based preprocessing techniques for propositional satisfiability. In: Intl. Conf. on Tools with Artificial Intelligence (ICTAI), pp.\u00a0105\u2013110. IEEE, Piscataway (2003)"},{"issue":"1","key":"9_CR70","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/s10472-005-0425-5","volume":"43","author":"I. Lynce","year":"2005","unstructured":"Lynce, I., Marques-Silva, J.: Efficient data structures for backtrack search SAT solvers. Ann. Math. Artif. Intell. 43(1), 137\u2013152 (2005)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"3\u20134","key":"9_CR71","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1023\/B:AMAI.0000012872.46214.11","volume":"40","author":"V.M. Manquinho","year":"2004","unstructured":"Manquinho, V.M., Marques-Silva, J.: Satisfiability-based algorithms for boolean optimization. Ann. Math. Artif. Intell. 40(3\u20134), 353\u2013372 (2004)","journal-title":"Ann. Math. Artif. Intell."},{"unstructured":"Marques-Silva, J.: Search algorithms for satisfiability problems in combinational switching circuits. Ph.D. thesis, University of Michigan (1995)","key":"9_CR72"},{"key":"9_CR73","series-title":"LNCS","first-page":"62","volume-title":"Portuguese Conf. on Artificial Intelligence (EPIA)","author":"J. Marques-Silva","year":"1999","unstructured":"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.\u00a01695, pp.\u00a062\u201374. Springer, Heidelberg (1999)"},{"key":"9_CR74","doi-asserted-by":"crossref","first-page":"537","DOI":"10.1007\/3-540-45349-0_45","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2000","author":"Jo\u00e3o Marques-Silva","year":"2000","unstructured":"Marques-Silva, J.: Algebraic simplification techniques for propositional satisfiability. In: Dechter [107], pp.\u00a0537\u2013542"},{"key":"9_CR75","first-page":"615","volume-title":"Intl. Joint Conf. on Artificial Intelligence (IJCAI)","author":"J. Marques-Silva","year":"2013","unstructured":"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.\u00a0615\u2013622. IJCAI\/AAAI, Melbourne\/Palo Alto (2013)"},{"key":"9_CR76","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"592","DOI":"10.1007\/978-3-642-39799-8_39","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"J. Marques-Silva","year":"2013","unstructured":"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.\u00a08044, pp.\u00a0592\u2013607. Springer, Heidelberg (2013)"},{"unstructured":"Marques-Silva, J., Janota, M., Lynce, I.: On computing backbones of propositional theories. In: Coelho et al. [54], pp.\u00a015\u201320","key":"9_CR77"},{"key":"9_CR78","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"131","volume-title":"Handbook of Satisfiability","author":"J. Marques-Silva","year":"2009","unstructured":"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.\u00a0185, pp.\u00a0131\u2013153. IOS Press, Amsterdam (2009)"},{"key":"9_CR79","doi-asserted-by":"crossref","first-page":"705","DOI":"10.1145\/196244.196621","volume-title":"Design Automation Conf. (DAC)","author":"J. Marques-Silva","year":"1994","unstructured":"Marques-Silva, J., Sakallah, K.A.: Dynamic search-space pruning techniques in path sensitization. In: Lorenzetti, M.J. (ed.) Design Automation Conf. (DAC), pp.\u00a0705\u2013711. ACM, New York (1994)"},{"key":"9_CR80","first-page":"220","volume-title":"Intl. Conf. on Computer-Aided Design (ICCAD)","author":"J. Marques-Silva","year":"1996","unstructured":"Marques-Silva, J., Sakallah, K.A.: GRASP\u2014a new search algorithm for satisfiability. In: Rutenbar, R.A., Otten, R.H.J.M. (eds.) Intl. Conf. on Computer-Aided Design (ICCAD), pp.\u00a0220\u2013227. IEEE\/ACM, Piscataway\/New York (1996)"},{"issue":"5","key":"9_CR81","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"Trans. Comput."},{"key":"9_CR82","series-title":"LNCS","volume-title":"Theory and Applications of Satisfiability Testing\u2014SAT 2007, Proceedings of the 10th International Conference","year":"2007","unstructured":"Marques-Silva, J., Sakallah, K.A. (eds.): Theory and Applications of Satisfiability Testing\u2014SAT 2007, Proceedings of the 10th International Conference, Lisbon, Portugal, May 28\u201331, 2007. LNCS, vol.\u00a04501. Springer, Heidelberg (2007)"},{"key":"9_CR83","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"K.L. McMillan","year":"2002","unstructured":"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.\u00a02404, pp.\u00a0250\u2013264. Springer, Heidelberg (2002)"},{"key":"9_CR84","series-title":"LNCS","first-page":"1","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"K.L. McMillan","year":"2003","unstructured":"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.\u00a02725, pp.\u00a01\u201313. Springer, Heidelberg (2003)"},{"issue":"4","key":"9_CR85","doi-asserted-by":"crossref","first-page":"478","DOI":"10.1007\/s10601-013-9146-2","volume":"18","author":"A. Morgado","year":"2013","unstructured":"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\u2013534 (2013)","journal-title":"Constraints"},{"key":"9_CR86","first-page":"530","volume-title":"Design Automation Conf. (DAC)","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Design Automation Conf. (DAC), pp.\u00a0530\u2013535. ACM, New York (2001)"},{"key":"9_CR87","first-page":"574","volume-title":"Intl. Conf. on VLSI Design","author":"G.J. Nam","year":"1999","unstructured":"Nam, G.J., Sakallah, K.A., Rutenbar, R.A.: Satisfiability-based detailed FPGA routing. In: Intl. Conf. on VLSI Design, pp.\u00a0574\u2013577. IEEE, Piscataway (1999)"},{"issue":"6","key":"9_CR88","first-page":"937","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T$T$). J.\u00a0ACM 53(6), 937\u2013977 (2006)","journal-title":"J.\u00a0ACM"},{"doi-asserted-by":"crossref","unstructured":"Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva and Sakallah [33], pp.\u00a0294\u2013299","key":"9_CR89","DOI":"10.1007\/978-3-540-72788-0_28"},{"issue":"3","key":"9_CR90","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J.\u00a0Symb. Comput. 2(3), 293\u2013304 (1986)","journal-title":"J.\u00a0Symb. Comput."},{"doi-asserted-by":"crossref","unstructured":"Prestwich, S.D.: Variable dependency in local search: prevention is better than cure. In: Marques-Silva and Sakallah [32], pp.\u00a0107\u2013120","key":"9_CR91","DOI":"10.1007\/978-3-540-72788-0_14"},{"key":"9_CR92","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"75","volume-title":"Handbook of Satisfiability","author":"S.D. Prestwich","year":"2009","unstructured":"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.\u00a0185, pp.\u00a075\u201397. IOS Press, Amsterdam (2009)"},{"key":"9_CR93","series-title":"LNCS","first-page":"31","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"K. Ravi","year":"2004","unstructured":"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.\u00a02988, pp.\u00a031\u201345. Springer, Heidelberg (2004)"},{"issue":"1","key":"9_CR94","first-page":"23","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J.\u00a0ACM 12(1), 23\u201341 (1965)","journal-title":"J.\u00a0ACM"},{"key":"9_CR95","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"695","volume-title":"Handbook of Satisfiability","author":"O. Roussel","year":"2009","unstructured":"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.\u00a0185, pp.\u00a0695\u2013733. IOS Press, Amsterdam (2009)"},{"key":"9_CR96","series-title":"LNCS","first-page":"498","volume-title":"Theory and Applications of Satisfiability Testing (SAT)","author":"A. Sabharwal","year":"2012","unstructured":"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.\u00a07317, pp.\u00a0498\u2013499. Springer, Heidelberg (2012)"},{"issue":"1","key":"9_CR97","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1109\/43.3140","volume":"7","author":"M.H. Schulz","year":"1988","unstructured":"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\u2013137 (1988)","journal-title":"Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"9_CR98","series-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1090\/dimacs\/026\/25","volume-title":"Cliques, Coloring and Satisfiability: Second DIMACS Implementation Challenge","author":"B. Selman","year":"1996","unstructured":"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.\u00a026, pp.\u00a0521\u2013532. AMS, Providence (1996)"},{"key":"9_CR99","series-title":"LNCS","first-page":"108","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, 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.\u00a01954, pp.\u00a0108\u2013125. Springer, Heidelberg (2000)"},{"issue":"1","key":"9_CR100","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1023\/A:1008725524946","volume":"16","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., St\u00e5lmarck, G.: A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic. Form. Methods Syst. Des. 16(1), 23\u201358 (2000)","journal-title":"Form. Methods Syst. Des."},{"key":"9_CR101","first-page":"94","volume-title":"Intl. Conf. on Automated Software Engineering (ASE)","author":"I. Shlyakhter","year":"2003","unstructured":"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.\u00a094\u2013105. IEEE, Piscataway (2003)"},{"key":"9_CR102","series-title":"LNCS","first-page":"827","volume-title":"Intl. Conf. on Principles and Practice of Constraint Programming (CP)","author":"C. Sinz","year":"2005","unstructured":"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.\u00a03709, pp.\u00a0827\u2013831. Springer, Heidelberg (2005)"},{"key":"9_CR103","first-page":"356","volume-title":"Lecture Notes in Computer Science","author":"Carsten Sinz","year":"2009","unstructured":"Sinz, C., Iser, M.: Problem-sensitive restart heuristics for the DPLL procedure. In: Kullmann [98], pp.\u00a0356\u2013362"},{"key":"9_CR104","first-page":"339","volume-title":"European Conf. on Artificial Intelligence (ECAI)","author":"J.L.N. Siqueira de","year":"1988","unstructured":"de Siqueira, J.L.N., Puget, J.F.: Explanation-based generalisation of failures. In: Kodratoff, Y. (ed.) European Conf. on Artificial Intelligence (ECAI), pp.\u00a0339\u2013344. Pitman, London (1988)"},{"key":"9_CR105","first-page":"237","volume-title":"Lecture Notes in Computer Science","author":"Niklas S\u00f6rensson","year":"2009","unstructured":"S\u00f6rensson, N., Biere, A.: Minimizing learned clauses. In: Kullmann [25], pp.\u00a0237\u2013243"},{"issue":"2","key":"9_CR106","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0004-3702(77)90029-7","volume":"9","author":"R.M. Stallman","year":"1977","unstructured":"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\u2013196 (1977)","journal-title":"Artif. Intell."},{"issue":"9","key":"9_CR107","doi-asserted-by":"crossref","first-page":"1167","DOI":"10.1109\/43.536723","volume":"15","author":"P.R. Stephan","year":"1996","unstructured":"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\u20131176 (1996)","journal-title":"Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"9_CR108","series-title":"LNCS","first-page":"19","volume-title":"Theory and Applications of Satisfiability Testing (SAT)","author":"P.J. Stuckey","year":"2013","unstructured":"Stuckey, P.J.: There are no CNF problems. In: J\u00e4rvisalo, M., Gelder, A.V. (eds.) Theory and Applications of Satisfiability Testing (SAT). LNCS, vol.\u00a07962, pp.\u00a019\u201321. Springer, Heidelberg (2013)"},{"issue":"1","key":"9_CR109","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1137\/0203006","volume":"3","author":"R.E. Tarjan","year":"1974","unstructured":"Tarjan, R.E.: Finding dominators in directed graphs. SIAM J. Comput. 3(1), 62\u201389 (1974)","journal-title":"SIAM J. Comput."},{"key":"9_CR110","first-page":"115","volume-title":"Studies in Constructive Mathematics and Mathematical Logic, Part II","author":"G.S. Tseitin","year":"1968","unstructured":"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.\u00a0115\u2013125. Springer, Heidelberg (1968)"},{"issue":"4","key":"9_CR111","doi-asserted-by":"crossref","first-page":"425","DOI":"10.2178\/bsl\/1203350879","volume":"1","author":"A. Urquhart","year":"1995","unstructured":"Urquhart, A.: The complexity of propositional proofs. Bull. Symb. Log. 1(4), 425\u2013467 (1995)","journal-title":"Bull. Symb. Log."},{"doi-asserted-by":"crossref","unstructured":"Van Gelder, A., Tsuji, Y.K.: Satisfiability testing with more reasoning and less guessing. Tech. rep., University of California at Santa Cruz (1995)","key":"9_CR112","DOI":"10.1090\/dimacs\/026\/27"},{"issue":"2","key":"9_CR113","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0020-0190(98)00144-6","volume":"68","author":"J.P. Warners","year":"1998","unstructured":"Warners, J.P.: A linear-time transformation of linear inequalities into conjunctive normal form. Inf. Process. Lett. 68(2), 63\u201369 (1998)","journal-title":"Inf. Process. Lett."},{"key":"9_CR114","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1007\/978-3-642-33558-7_49","volume-title":"Intl. Conf. on Principles and Practice of Constraint Programming (CP)","author":"S. Wieringa","year":"2012","unstructured":"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.\u00a07514, pp.\u00a0672\u2013687. Springer, Heidelberg (2012)"},{"issue":"2","key":"9_CR115","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0020-0190(89)90035-5","volume":"32","author":"D.A. Wolfram","year":"1989","unstructured":"Wolfram, D.A.: Forward checking and intelligent backtracking. Inf. Process. Lett. 32(2), 85\u201387 (1989)","journal-title":"Inf. Process. Lett."},{"key":"9_CR116","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1613\/jair.2490","volume":"32","author":"L. Xu","year":"2008","unstructured":"Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: SATzilla: Portfolio-based algorithm selection for SAT. J.\u00a0Artif. Intell. Res. 32, 565\u2013606 (2008)","journal-title":"J.\u00a0Artif. Intell. Res."},{"key":"9_CR117","first-page":"155","volume-title":"National Conference on Artificial Intelligence (AAAI)","author":"R. Zabih","year":"1988","unstructured":"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.\u00a0155\u2013160. AAAI Press\/MIT Press, Palo Alto\/Cambridge (1988)"},{"key":"9_CR118","series-title":"LNCS","first-page":"272","volume-title":"Intl. Conf. on Automated Deduction (CADE)","author":"H. Zhang","year":"1997","unstructured":"Zhang, H.: SATO: an efficient propositional prover. In: McCune, W. (ed.) Intl. Conf. on Automated Deduction (CADE). LNCS, vol.\u00a01249, pp.\u00a0272\u2013275. Springer, Heidelberg (1997)"},{"issue":"1\/2","key":"9_CR119","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1023\/A:1006351428454","volume":"24","author":"H. Zhang","year":"2000","unstructured":"Zhang, H., Stickel, M.E.: Implementing the Davis-Putnam method. J.\u00a0Autom. Reason. 24(1\/2), 277\u2013296 (2000)","journal-title":"J.\u00a0Autom. Reason."},{"key":"9_CR120","first-page":"10,880","volume-title":"Design, Automation & Test in Europe (DATE)","author":"L. Zhang","year":"2003","unstructured":"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.\u00a010,880\u201310,885. IEEE, Piscataway (2003)"},{"key":"9_CR121","first-page":"84","volume-title":"Intl. High Level Design Validation and Test Workshop (HLDVT)","author":"C.S. Zhu","year":"2011","unstructured":"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.\u00a084\u201391. IEEE, Piscataway (2011)"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,6]],"date-time":"2024-07-06T21:24:38Z","timestamp":1720301078000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":121,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_9","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}