{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T14:01:08Z","timestamp":1777125668580,"version":"3.51.4"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2008,3,5]],"date-time":"2008-03-05T00:00:00Z","timestamp":1204675200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Comb Optim"],"published-print":{"date-parts":[[2009,8]]},"DOI":"10.1007\/s10878-008-9142-4","type":"journal-article","created":{"date-parts":[[2008,3,4]],"date-time":"2008-03-04T12:42:20Z","timestamp":1204634540000},"page":"124-150","source":"Crossref","is-referenced-by-count":16,"title":["Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems"],"prefix":"10.1007","volume":"18","author":[{"given":"Christian","family":"Desrosiers","sequence":"first","affiliation":[]},{"given":"Philippe","family":"Galinier","sequence":"additional","affiliation":[]},{"given":"Alain","family":"Hertz","sequence":"additional","affiliation":[]},{"given":"Sandrine","family":"Paroz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2008,3,5]]},"reference":[{"key":"9142_CR1","doi-asserted-by":"crossref","unstructured":"Amaldi E, Pfetsch ME, Trotter LEJ (1999) Some structural and algorithmic properties of the maximum feasible subsystem problem. In: Proceedings of the 7th international IPCO conference on integer programming and combinatorial optimization, June 1999, pp 45\u201359","DOI":"10.1007\/3-540-48777-8_4"},{"key":"9142_CR2","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/978-3-540-30557-6_14","volume-title":"Proceedings of the 7th international symposium on practical aspects of declarative languages (PADL05)","author":"J Bailey","year":"2005","unstructured":"Bailey J, Stuckey PJ (2005) Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Proceedings of the 7th international symposium on practical aspects of declarative languages (PADL05). Lecture notes in computer science, vol 3350. Springer, Berlin, pp 174\u2013186"},{"key":"9142_CR3","volume-title":"Handbook of combinatorial optimization","author":"R Battiti","year":"1998","unstructured":"Battiti R, Protasi M (1998) Approximate algorithms and heuristics for MAX-SAT. In: Ding-zhu D (ed) Handbook of combinatorial optimization, vol 1. Kluwer Academic, Boston"},{"key":"9142_CR4","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1023\/A:1009725216438","volume":"2","author":"B Borchers","year":"1999","unstructured":"Borchers B, Furman J (1999) A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems. J Comb Optim 2:299\u2013306","journal-title":"J Comb Optim"},{"issue":"2","key":"9142_CR5","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/S0166-218X(02)00399-2","volume":"130","author":"R Bruni","year":"2003","unstructured":"Bruni R (2003) Approximating minimal unsatisfiable subformulae by means of adaptive core search. Discrete Appl Math 130(2):85\u2013100","journal-title":"Discrete Appl Math"},{"issue":"2","key":"9142_CR6","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1287\/ijoc.9.2.164","volume":"9","author":"JW Chinneck","year":"1997","unstructured":"Chinneck JW (1997) Finding a useful subset of constraints for analysis in an infeasible linear program. INFORMS J Comput 9(2):164\u2013174","journal-title":"INFORMS J Comput"},{"key":"9142_CR7","unstructured":"Culberson J (2004) http:\/\/web.cs.ualberta.ca\/~joe\/Coloring\/index.html"},{"issue":"1","key":"9142_CR8","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0304-3975(01)00174-8","volume":"289","author":"E Dantsin","year":"2002","unstructured":"Dantsin E, Goerdt A, Hirsch EA, Kannan R, Kleinberg J, Papadimitriou C, Raghavan P, Sch\u00f6ning U (2002) A deterministic (2\u22122\/(k+1)) n algorithm for k-SAT based on local search. Theor Comput Sci 289(1):69\u201383","journal-title":"Theor Comput Sci"},{"issue":"7","key":"9142_CR9","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 (1962) A machine program for theorem-proving. Commun ACM 5(7):394\u2013397","journal-title":"Commun ACM"},{"issue":"2","key":"9142_CR10","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1016\/j.dam.2006.07.019","volume":"156","author":"C Desrosiers","year":"2008","unstructured":"Desrosiers C, Galinier P, Hertz A (2008) Efficient algorithms for finding critical subgraphs. Discrete Appl Math 156(2):244\u2013266","journal-title":"Discrete Appl Math"},{"key":"9142_CR11","unstructured":"Dimacs ftp site (1993) ftp:\/\/dimacs.rutgers.edu\/pub\/challenge\/sat\/benchmarks\/cnf"},{"issue":"1","key":"9142_CR12","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1016\/S0304-3975(01)00337-1","volume":"289","author":"H Fleischner","year":"2002","unstructured":"Fleischner H, Kullmann O, Szeider S (2002) Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference. Theor Comput Sci 289(1):503\u2013516","journal-title":"Theor Comput Sci"},{"key":"9142_CR13","unstructured":"Franco J, Gu J, Purdom PW, Wah BW (1997) Satisfiability problem: theory and applications. In DIMACS series in discrete mathematics and theoretical computer science, pp 19\u2013152"},{"key":"9142_CR14","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1016\/j.dam.2006.04.043","volume":"155","author":"P Galinier","year":"2007","unstructured":"Galinier P, Hertz A (2007) Solution techniques for the large set covering problem. Discrete Appl Math 155:312\u2013326","journal-title":"Discrete Appl Math"},{"issue":"1","key":"9142_CR15","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1287\/ijoc.2.1.61","volume":"2","author":"J Gleeson","year":"1990","unstructured":"Gleeson J, Ryan J (1990) Identifying minimally infeasible subsystems of inequalities. ORSA J Comput 2(1):61\u201363","journal-title":"ORSA J Comput"},{"key":"9142_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-6089-0","volume-title":"Tabu search","author":"F Glover","year":"1997","unstructured":"Glover F, Laguna M (1997) Tabu search. Kluwer Academic, Boston"},{"key":"9142_CR17","unstructured":"Goldberg E, Novikov Y (2000) Berkmin: a fast and robust SAT-solver. In: Design, automation, and test in Europe \u201902, March 2000, pp 142\u2013149"},{"issue":"4","key":"9142_CR18","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/BF02241270","volume":"44","author":"P Hansen","year":"1990","unstructured":"Hansen P, Jaumard B (1990) Algorithms for the maximum satisfiability problem. Computing 44(4):279\u2013303","journal-title":"Computing"},{"issue":"10","key":"9142_CR19","first-page":"1","volume":"7","author":"F Herrmann","year":"2002","unstructured":"Herrmann F, Hertz A (2002) Finding the chromatic number by means of critical graphs. ACM J Exp Algorithmics 7(10):1\u20139","journal-title":"ACM J Exp Algorithmics"},{"key":"9142_CR20","doi-asserted-by":"crossref","unstructured":"Huang J (2005) Mup: a minimal unsatisfiability prover. In: Proceedings of the tenth Asia and South Pacific design automation conference (ASP-DAC-05), pp. 432\u2013437","DOI":"10.1145\/1120725.1120907"},{"issue":"3","key":"9142_CR21","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1016\/S0020-0190(02)00267-3","volume":"84","author":"H Kleine B\u00fcning","year":"2002","unstructured":"Kleine B\u00fcning H, Zhao X (2002) Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency. Inf Process Lett 84(3):147\u2013151","journal-title":"Inf Process Lett"},{"key":"9142_CR22","unstructured":"Levesque H, Mitchell D, Selman B (1992) GSAT\u2014a new method for solving hard satisfiability problems. In: Proceedings of the 10th national conference on artificial Intelligence (AAAI-92), pp 440\u2013446"},{"key":"9142_CR23","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/11499107_13","volume-title":"Proceedings of the 8th international conference on theory and applications of satisfiability testing (SAT-2005)","author":"MH Liffiton","year":"2005","unstructured":"Liffiton MH, Sakallah KA (2005) On finding all minimally unsatisfiable subformulas. In: Proceedings of the 8th international conference on theory and applications of satisfiability testing (SAT-2005). Lecture notes in computer science, vol 3569. Springer, Berlin, pp 173\u2013186"},{"key":"9142_CR24","unstructured":"Madigan CF, Malik S, Moskewicz MW, Zhang L, Zhao Y (2001) Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th conference on design automation, June 2001, pp 530\u2013535"},{"issue":"5","key":"9142_CR25","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":"9142_CR26","unstructured":"Mazure B, Sa\u00efs L, Gr\u00e9goire E (1997) Tabu search for SAT. In: Proceedings of the 14th national conference on artificial intelligence (AAAI-97), pp 281\u2013285"},{"issue":"3\u20134","key":"9142_CR27","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1023\/A:1018999721141","volume":"22","author":"B Mazure","year":"1998","unstructured":"Mazure B, Sa\u00efs L, Gr\u00e9goire E (1998) Boosting complete techniques thanks to local search methods. Ann Math Artif Intell 22(3\u20134):319\u2013331","journal-title":"Ann Math Artif Intell"},{"issue":"1","key":"9142_CR28","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1023\/A:1006343127545","volume":"24","author":"P Mills","year":"2000","unstructured":"Mills P, Tsang E (2000) Guided local search for solving SAT and weighted MAX-SAT problems. J Autom Reas 24(1):205\u2013223","journal-title":"J Autom Reas"},{"key":"9142_CR29","doi-asserted-by":"crossref","unstructured":"Mneimneh M, Lynce I, Andraus Z, Marques-Silva J, Sakallah K (2005) A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas. In: Proceedings of international conference on theory and applications of satisfiability testing, vol 3569, pp 467\u2013474","DOI":"10.1007\/11499107_40"},{"key":"9142_CR30","doi-asserted-by":"crossref","first-page":"518","DOI":"10.1145\/996566.996710","volume-title":"Proceedings of the 41st annual conference on design automation","author":"Y Oh","year":"2004","unstructured":"Oh Y, Mneimneh MN, Andraus ZS, Sakallah KA, Markov IL (2004) AMUSE: a minimally-unsatisfiable subformula extractor. In: Proceedings of the 41st annual conference on design automation. ACM, New York, pp 518\u2013523"},{"key":"9142_CR31","unstructured":"Sat benchmarks from automotive product configuration (2003) http:\/\/www-sr.informatik.uni-tuebingen.de\/~sinz\/DC\/"},{"key":"9142_CR32","unstructured":"Shang Y, Wah BW (1997) Discrete Lagrangian-based search for solving MAX-SAT problems. In: Proceedings of the 15th international joint conference on artificial intelligence, pp 378\u2013383"},{"key":"9142_CR33","doi-asserted-by":"crossref","unstructured":"Zhang H (1997) SATO: an efficient propositional prover. In: Proceedings of international conference on automated deduction (CADE-97), pp 272\u2013275","DOI":"10.1007\/3-540-63104-6_28"},{"key":"9142_CR34","unstructured":"Zhang L, Malik S (2003) Extracting small unsatisfiable cores from unsatisfiable boolean formulas. In: Sixth international conference on theory and applications of satisfiability testing (SAT2003), May 2003, pp 518\u2013523"}],"container-title":["Journal of Combinatorial Optimization"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10878-008-9142-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10878-008-9142-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10878-008-9142-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T00:18:12Z","timestamp":1559261892000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10878-008-9142-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,3,5]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,8]]}},"alternative-id":["9142"],"URL":"https:\/\/doi.org\/10.1007\/s10878-008-9142-4","relation":{},"ISSN":["1382-6905","1573-2886"],"issn-type":[{"value":"1382-6905","type":"print"},{"value":"1573-2886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,3,5]]}}}