{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,26]],"date-time":"2023-08-26T09:50:00Z","timestamp":1693043400439},"reference-count":59,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2011,12,28]],"date-time":"2011-12-28T00:00:00Z","timestamp":1325030400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["4OR-Q J Oper Res"],"published-print":{"date-parts":[[2012,3]]},"DOI":"10.1007\/s10288-011-0191-7","type":"journal-article","created":{"date-parts":[[2011,12,27]],"date-time":"2011-12-27T10:48:45Z","timestamp":1324982925000},"page":"15-32","source":"Crossref","is-referenced-by-count":7,"title":["Learning from conflicts in propositional satisfiability"],"prefix":"10.1007","volume":"10","author":[{"given":"Youssef","family":"Hamadi","sequence":"first","affiliation":[]},{"given":"Sa\u00efd","family":"Jabbour","sequence":"additional","affiliation":[]},{"given":"Lakhdar","family":"Sa\u00efs","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,12,28]]},"reference":[{"key":"191_CR1","doi-asserted-by":"crossref","unstructured":"Audemard G, Bordeaux L, Hamadi Y, Jabbour S, Sais L (2008) A generalized framework for conflict analysis. In: SAT, pp 21\u201327","DOI":"10.1007\/978-3-540-79719-7_3"},{"key":"191_CR2","doi-asserted-by":"crossref","unstructured":"Audemard G, Bordeaux L, Hamadi Y, Jabbour S, Sais L (2008) A generalized framework for conflict analysis. Technical Report MSR-TR-2008-34, Microsoft Research, Feb 2008","DOI":"10.1007\/978-3-540-79719-7_3"},{"key":"191_CR3","doi-asserted-by":"crossref","unstructured":"Audemard G, Lagniez J-M, Mazure B, Sais L (2011) On freezing and reactivating learnt clauses. In: Proceedings of the 14th international conference on theory and applications of satisfiability testing (SAT\u20192011), pp 188\u2013200","DOI":"10.1007\/978-3-642-21581-0_16"},{"key":"191_CR4","unstructured":"Bayardo RJ, Miranker DP (1996) A complexity analysis of space-bounded learning algorithms for the constraint satisfaction problem. In: In Proceedings of the 13th national conference on artificial intelligence, pp 298\u2013304"},{"key":"191_CR5","unstructured":"Bayardo RJ Jr, Schrag RC (1997) Using CSP look-back techniques to solve real-world SAT instances. In: AAAI, pp 203\u2013208"},{"key":"191_CR6","volume-title":"Handbook of satisfiability: volume 185 frontiers in artificial intelligence and applications","author":"A Biere","year":"2009","unstructured":"Biere A, Biere A, Heule M, van Maaren H, Walsh T (2009) Handbook of satisfiability: volume 185 frontiers in artificial intelligence and applications. IOS Press, Amsterdam, The Netherlands"},{"key":"191_CR7","doi-asserted-by":"crossref","unstructured":"Biere A (2008) Adaptive restart strategies for conflict driven sat solvers. In: Proceedings of the 11th international conference on theory and applications of satisfiability testing (SAT\u201908), pp 28\u201333","DOI":"10.1007\/978-3-540-79719-7_4"},{"key":"191_CR8","doi-asserted-by":"crossref","unstructured":"Brisoux L, Gregoire E, Sais L (1999) Improving backtrack search for SAT by means of redundancy. In: International syposium on methodologies for intelligent systems, pp 301\u2013309","DOI":"10.1007\/BFb0095116"},{"issue":"1","key":"191_CR9","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1016\/0020-0190(81)90074-0","volume":"12","author":"M Bruynooghe","year":"1981","unstructured":"Bruynooghe M (1981) Solving combinatorial search problems by intelligent backtracking. Inf Process Lett 12(1): 36\u201339","journal-title":"Inf Process Lett"},{"key":"191_CR10","doi-asserted-by":"crossref","DOI":"10.1002\/9781118033166","volume-title":"Optimization methods for logical inference","author":"V Chandru","year":"1999","unstructured":"Chandru V, Hooker J (1999) Optimization methods for logical inference. Wiley, London"},{"key":"191_CR11","unstructured":"Crawford JM, Baker AB (1994) Experimental results on the application of satisfiability algorithms to scheduling problems. In: Proceedings of the 12th national conference on artificial intelligence (AAAI\u201994), pp 1092\u20131097"},{"issue":"7","key":"191_CR12","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 DW (1962) A machine program for theorem-proving. Commun ACM 5(7): 394\u2013397","journal-title":"Commun ACM"},{"key":"191_CR13","unstructured":"Dechter R (1986) Learning while searching in constraint-satisfaction-problems. In: AAAI, pp 178\u2013185"},{"issue":"3","key":"191_CR14","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1016\/0004-3702(90)90046-3","volume":"41","author":"R Dechter","year":"1990","unstructured":"Dechter R (1990) Enhancement schemes for constraint processing: backjumping, learning, and cutset decomposition. Artif Intell 41(3): 273\u2013312","journal-title":"Artif Intell"},{"issue":"3","key":"191_CR15","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0004-3702(79)90008-0","volume":"12","author":"J Doyle","year":"1979","unstructured":"Doyle J (1979) A truth maintenance system. Artif Intell 12(3): 231\u2013272","journal-title":"Artif Intell"},{"key":"191_CR16","doi-asserted-by":"crossref","unstructured":"Dubois O, Andr\u00e9 P, Boufkhad Y, Carlier Y (1996) Second DIMACS implementation challenge: cliques, coloring and satisfiability. In: DIMACS Series in Discrete Mathematics and Theoretical Computer Science, chapter SAT vs. UNSAT, vol 26. American Mathematical Society, pp 415\u2013436","DOI":"10.1090\/dimacs\/026\/20"},{"key":"191_CR17","unstructured":"Een N, S\u00f6rensson N (2005) Minisat\u2014a sat solver with conflict-clause minimization. In: Proceedings of the 8th international conference on theory and applications of satisfiability testing (SAT\u201905)"},{"key":"191_CR18","doi-asserted-by":"crossref","unstructured":"E\u00e9n N, Biere A (2005) Effective preprocessing in sat through variable and clause elimination. In: SAT, pp 61\u201375","DOI":"10.1007\/11499107_5"},{"key":"191_CR19","unstructured":"E\u00e9n N, S\u00f6rensson N (2003) An extensible sat-solver. In: Proceedings of the 6th international conference on theory and applications of satisfiability testing (SAT\u201903), pp 502\u2013518"},{"key":"191_CR20","unstructured":"Frost D, Dechter R (1994) Dead-end driven learning. In: AAAI, pp 294\u2013300"},{"key":"191_CR21","unstructured":"Gasching J (1979) Performance measurement and analysis of certain search algorithms. PhD thesis, Department of Computer science, Carnegie Mellon University"},{"key":"191_CR22","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1613\/jair.1","volume":"1","author":"ML Ginsberg","year":"1993","unstructured":"Ginsberg ML (1993) Dynamic backtracking. J Artif Intell Res (JAIR) 1: 25\u201346","journal-title":"J Artif Intell Res (JAIR)"},{"issue":"1\/2","key":"191_CR23","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1023\/A:1006314320276","volume":"24","author":"CP Gomes","year":"2000","unstructured":"Gomes CP, Selman B, Crato N, Kautz HA (2000) Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. J Autom Reasoning 24(1\/2): 67\u2013100","journal-title":"J Autom Reasoning"},{"key":"191_CR24","unstructured":"Gomes CP, Selman B, Kautz HA (1998) Boosting combinatorial search through randomization. In: AAAI\/IAAI, pp 431\u2013437"},{"key":"191_CR25","doi-asserted-by":"crossref","unstructured":"Hamadi Y, Jabbour S, Sais L (2009) Learning for dynamic subsumption. In: 21st IEEE international conference on tools with artificial intelligence\u2014ICTAI\u201909, pp 328\u2013335","DOI":"10.1109\/ICTAI.2009.22"},{"key":"191_CR26","doi-asserted-by":"crossref","unstructured":"Hamadi Y, Jabbour S, Sais L (2009) ManySAT: a parallel SAT solver. JSAT 6:245\u2013262","DOI":"10.3233\/SAT190070"},{"key":"191_CR27","doi-asserted-by":"crossref","unstructured":"Heule M, J\u00e4rvisalo M, Biere A (2010) Clause elimination procedures for cnf formulas. In: 17th International conference on logic for programming, artificial intelligence, and reasoning (LPAR\u201910), pp 357\u2013371","DOI":"10.1007\/978-3-642-16242-8_26"},{"key":"191_CR28","doi-asserted-by":"crossref","unstructured":"Heule M, J\u00e4rvisalo M, Biere A (2011) Efficient cnf simplification based on binary implication graphs. In: Proceedings of the 14th international conference on theory and applications of satisfiability testing (SAT\u201911), pp 201\u2013215","DOI":"10.1007\/978-3-642-21581-0_17"},{"key":"191_CR29","doi-asserted-by":"crossref","DOI":"10.1002\/9781118033036","volume-title":"Logic-based methods for optimization: combining optimization and constraint satisfaction","author":"J Hooker","year":"2000","unstructured":"Hooker J (2000) Logic-based methods for optimization: combining optimization and constraint satisfaction. Wiley, London"},{"issue":"3","key":"191_CR30","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1287\/ijoc.1.3.137","volume":"1","author":"JN Hooker","year":"1989","unstructured":"Hooker JN (1989) Input proofs and rank one cutting planes. INFORMS J Comput 1(3): 137\u2013145","journal-title":"INFORMS J Comput"},{"key":"191_CR31","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/BF01531074","volume":"1","author":"JN Hooker","year":"1990","unstructured":"Hooker JN, Fedjiki C (1990) Branch-and-cut solution of inference problems in propositional logic. Ann Math Artif Intell 1: 123\u2013139","journal-title":"Ann Math Artif Intell"},{"key":"191_CR32","unstructured":"Huang J (2007) The effect of restarts on the efficiency of clause learning. In: Proceedings of the 20th international joint conference on artificial intelligence (IJCAI\u201907), pp 2318\u20132323"},{"key":"191_CR33","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BF01531077","volume":"1","author":"RG Jeroslow","year":"1990","unstructured":"Jeroslow RG, Wang J (1990) Solving propositional satisfiability problems. Ann Math Artif Intell 1: 167\u2013187","journal-title":"Ann Math Artif Intell"},{"key":"191_CR34","unstructured":"Kautz HA, Horvitz E, Ruan Y, Gomes CP, Selman B (2002) Dynamic restart policies. In: AAAI\/IAAI, pp 674\u2013681"},{"key":"191_CR35","unstructured":"Li CM, Anbulagan (1997) Heuristics based on unit propagation for satisfiability problems. In: IJCAI\u201997, pp 366\u2013371"},{"key":"191_CR36","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0020-0190(93)90029-9","volume":"47","author":"M Luby","year":"1993","unstructured":"Luby M, Sinclair A, Zuckerman D (1993) Optimal speedup of las vegas algorithms. Inf Process Lett 47: 173\u2013180","journal-title":"Inf Process Lett"},{"key":"191_CR37","unstructured":"Marques Silva JP, Sakallah KA (1996) Grasp\u2014a new search algorithm for satisfiability. In: ICCAD, pp 220\u2013227"},{"issue":"5","key":"191_CR38","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva JP, Sakallah KA (1999) Grasp: a search algorithm for propositional satisfiability. IEEE Trans Comput 48(5): 506\u2013521","journal-title":"IEEE Trans Comput"},{"key":"191_CR39","doi-asserted-by":"crossref","unstructured":"Marques-silva JP (1999) The impact of branching heuristics in propositional satisfiability algorithms. In: In 9th Portuguese conference on artificial intelligence EPIA, pp 62\u201374","DOI":"10.1007\/3-540-48159-1_5"},{"key":"191_CR40","unstructured":"McAllester DA (1980) An outlook on truth maintenance. AI Memo 551, MIT AI Laboratory, August 1980"},{"key":"191_CR41","unstructured":"Morris P (1993) The breakout method for escaping from local minima. In: Proceedings of the 11th national conference on artificial intelligence (AAAI\u201993), pp 40\u201345"},{"key":"191_CR42","doi-asserted-by":"crossref","unstructured":"Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient sat solver. In: DAC, pp 530\u2013535","DOI":"10.1145\/378239.379017"},{"key":"191_CR43","unstructured":"Piette C, Hamadi Y, Sais L (2008) Vivifying propositional clausal formulae. In: Proceedings of the 18th European conference on artificial intelligence (ECAI\u201908), pp 525\u2013529"},{"key":"191_CR44","doi-asserted-by":"crossref","unstructured":"Pipatsrisawat K, Darwiche A (2007) A lightweight component caching scheme for satisfiability solvers. In: Proceedings of SAT\u201907, pp 294\u2013299","DOI":"10.1007\/978-3-540-72788-0_28"},{"key":"191_CR45","unstructured":"Pipatsrisawat K, Darwiche A (2008) A new clause learning scheme for efficient unsatisfiability proofs. In: AAAI, pp 1481\u20131484"},{"key":"191_CR46","doi-asserted-by":"crossref","unstructured":"Pipatsrisawat K, Darwiche A (2009) On the power of clause-learning sat solvers with restarts. In: CP, pp 654\u2013668","DOI":"10.1007\/978-3-642-04244-7_51"},{"key":"191_CR47","doi-asserted-by":"crossref","unstructured":"Pipatsrisawat K, Darwiche A (2009) Width-based restart policies for clause-learning satisfiability solvers. In: Proceedings of the 12th international conference on theory and applications of satisfiability testing (SAT\u201909), pp 341\u2013355","DOI":"10.1007\/978-3-642-02777-2_32"},{"key":"191_CR48","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1111\/j.1467-8640.1993.tb00310.x","volume":"9","author":"P Prosser","year":"1993","unstructured":"Prosser P (1993) Hybrid algorithms for the constraint satisfaction problem. Comput Intell 9: 268\u2013299","journal-title":"Comput Intell"},{"issue":"9","key":"191_CR49","doi-asserted-by":"crossref","first-page":"627","DOI":"10.2307\/2307285","volume":"62","author":"WV Quine","year":"1955","unstructured":"Quine WV (1955) A way to simplify truth functions. Am Math Mon 62(9): 627\u2013631","journal-title":"Am Math Mon"},{"key":"191_CR50","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson JA (1965) A machine-oriented logic based on the resolution principle. J ACM 12: 23\u201341","journal-title":"J ACM"},{"key":"191_CR51","volume-title":"Probleme SAT: Progr\u00e8s et D\u00e9fis","author":"L Sais","year":"2008","unstructured":"Sais L (2008) Probleme SAT: Progr\u00e8s et D\u00e9fis. Hermes Publishing Ltd, London"},{"key":"191_CR52","doi-asserted-by":"crossref","unstructured":"S\u00f6rensson N, Biere A (2009) Minimizing learned clauses. In: 12th International conference on theory and applications of satisfiability testing\u2014SAT\u20192009, pp 237\u2013243","DOI":"10.1007\/978-3-642-02777-2_23"},{"issue":"2","key":"191_CR53","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0004-3702(77)90029-7","volume":"9","author":"RM Stallman","year":"1977","unstructured":"Stallman RM, Sussman GJ (1977) Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artif Intell 9(2): 135\u2013196","journal-title":"Artif Intell"},{"key":"191_CR54","doi-asserted-by":"crossref","unstructured":"Subbarayan S, Pradhan DK (2004) Niver: non increasing variable elimination resolution for preprocessing sat instances. In: SAT (2004)","DOI":"10.1007\/11527695_22"},{"key":"191_CR55","unstructured":"Tseitin GS (1968) On the complexity of derivations in the propositional calculus. In: Slesenko HAO (ed) Structures in constructives mathematics and mathematical logic, Part II, pp 115\u2013125"},{"issue":"2","key":"191_CR56","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0020-0190(98)00144-6","volume":"68","author":"JP Warners","year":"1998","unstructured":"Warners JP (1998) A linear-time transformation of linear inequalities into conjunctive normal form. Inf Process Lett 68(2): 63\u201369","journal-title":"Inf Process Lett"},{"key":"191_CR57","doi-asserted-by":"crossref","unstructured":"Zhang H (1997) SATO: an efficient propositional prover. In: McCune W (ed) Proceedings of the 14th international conference on automated deduction, LNAI, vol 1249. Springer, Berlin, pp 272\u2013275","DOI":"10.1007\/3-540-63104-6_28"},{"key":"191_CR58","unstructured":"Zhang Lintao (2005) On subsumption removal and on-the-fly cnf simplification. In: SAT, pp 482\u2013489"},{"key":"191_CR59","unstructured":"Zhang L, Madigan CF, Moskewicz MH (2001) Efficient conflict driven learning in a boolean satisfiability solver. In: In ICCAD, pp 279\u2013285"}],"container-title":["4OR"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10288-011-0191-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10288-011-0191-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10288-011-0191-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,29]],"date-time":"2020-06-29T10:55:30Z","timestamp":1593428130000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10288-011-0191-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12,28]]},"references-count":59,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,3]]}},"alternative-id":["191"],"URL":"https:\/\/doi.org\/10.1007\/s10288-011-0191-7","relation":{},"ISSN":["1619-4500","1614-2411"],"issn-type":[{"value":"1619-4500","type":"print"},{"value":"1614-2411","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,12,28]]}}}