Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems

• 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–59

• 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–186

  Google Scholar 

• 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

  Google Scholar 

• Borchers B, Furman J (1999) A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems. J Comb Optim 2:299–306

  Article  MATH  MathSciNet  Google Scholar 

• Bruni R (2003) Approximating minimal unsatisfiable subformulae by means of adaptive core search. Discrete Appl Math 130(2):85–100

  Article  MATH  MathSciNet  Google Scholar 

• Chinneck JW (1997) Finding a useful subset of constraints for analysis in an infeasible linear program. INFORMS J Comput 9(2):164–174

  Article  MATH  MathSciNet  Google Scholar 

• Culberson J (2004) http://web.cs.ualberta.ca/~joe/Coloring/index.html

• Dantsin E, Goerdt A, Hirsch EA, Kannan R, Kleinberg J, Papadimitriou C, Raghavan P, Schöning U (2002) A deterministic (2−2/(k+1))ⁿ algorithm for k-SAT based on local search. Theor Comput Sci 289(1):69–83

  Article  MATH  Google Scholar 

• Davis M, Logemann G, Loveland D (1962) A machine program for theorem-proving. Commun ACM 5(7):394–397

  Article  MATH  MathSciNet  Google Scholar 

• Desrosiers C, Galinier P, Hertz A (2008) Efficient algorithms for finding critical subgraphs. Discrete Appl Math 156(2):244–266

  Article  MATH  MathSciNet  Google Scholar 

• Dimacs ftp site (1993) ftp://dimacs.rutgers.edu/pub/challenge/sat/benchmarks/cnf

• 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–516

  Article  MATH  MathSciNet  Google Scholar 

• 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–152

• Galinier P, Hertz A (2007) Solution techniques for the large set covering problem. Discrete Appl Math 155:312–326

  Article  MATH  MathSciNet  Google Scholar 

• Gleeson J, Ryan J (1990) Identifying minimally infeasible subsystems of inequalities. ORSA J Comput 2(1):61–63

  MATH  Google Scholar 

• Glover F, Laguna M (1997) Tabu search. Kluwer Academic, Boston

  MATH  Google Scholar 

• Goldberg E, Novikov Y (2000) Berkmin: a fast and robust SAT-solver. In: Design, automation, and test in Europe ’02, March 2000, pp 142–149

• Hansen P, Jaumard B (1990) Algorithms for the maximum satisfiability problem. Computing 44(4):279–303

  Article  MATH  MathSciNet  Google Scholar 

• Herrmann F, Hertz A (2002) Finding the chromatic number by means of critical graphs. ACM J Exp Algorithmics 7(10):1–9

  MathSciNet  Google Scholar 

• 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–437

• Kleine Büning H, Zhao X (2002) Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency. Inf Process Lett 84(3):147–151

  Article  MATH  Google Scholar 

• Levesque H, Mitchell D, Selman B (1992) GSAT—a new method for solving hard satisfiability problems. In: Proceedings of the 10th national conference on artificial Intelligence (AAAI-92), pp 440–446

• 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–186

  Google Scholar 

• 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–535

• Marques Silva JP, Sakallah KA (1999) GRASP: a search algorithm for propositional satisfiability. IEEE Trans Comput 48(5):506–521

  Article  MathSciNet  Google Scholar 

• Mazure B, Saïs L, Grégoire E (1997) Tabu search for SAT. In: Proceedings of the 14th national conference on artificial intelligence (AAAI-97), pp 281–285

• Mazure B, Saïs L, Grégoire E (1998) Boosting complete techniques thanks to local search methods. Ann Math Artif Intell 22(3–4):319–331

  Article  MATH  Google Scholar 

• Mills P, Tsang E (2000) Guided local search for solving SAT and weighted MAX-SAT problems. J Autom Reas 24(1):205–223

  Article  MATH  MathSciNet  Google Scholar 

• 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–474

• 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–523

  Chapter  Google Scholar 

• Sat benchmarks from automotive product configuration (2003) http://www-sr.informatik.uni-tuebingen.de/~sinz/DC/

• 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–383

• Zhang H (1997) SATO: an efficient propositional prover. In: Proceedings of international conference on automated deduction (CADE-97), pp 272–275

• 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–523

Download references