A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas

Aharoni, R., & Linial, N. (1986). Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas. Journal of Combinatorial Theory Series A, 43(2), 196–204.

Andraus, Z. S., Liffiton, M. H., & Sakallah, K. A. (2006). Refinement strategies for verification methods based on datapath abstraction. In Proceedings of the 2006 conference on Asia South Pacific design automation (ASP-DAC’06) (pp. 19–24).

Andraus, Z. S., Liffiton, M. H., & Sakallah, K. A. (2007). CEGAR-based formal hardware verification: A case study. Technical Report CSE-TR-531-07, University of Michigan.

Bailey, J., & Stuckey, P. J. (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 (PADL’05), LNCS (Vol. 3350, pp. 174–186).

Birnbaum, E., & Lozinskii, E. L. (2003). Consistent subsets of inconsistent systems: Structure and behaviour. Journal of Experimental and Theoretical Artificial Intelligence, 15, 25–46.

Bruni, R., & Sassano, A. (2001). Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae. In LICS 2001 workshop on theory and applications of satisfiability testing (SAT-2001), Electronic Notes in Discrete Mathematics (Vol. 9, pp. 162–173).

Büning, H. K. (2000). On subclasses of minimal unsatisfiable formulas. Discrete Applied Mathematics, 107(1–3), 83–98.

Büning, H. K., & Zhao, X. (2001). Minimal falsity for QBF with deficiency one. Workshop on Theory and Applications of Quantified Boolean Formulas.

Dasgupta, S., & Chandru, V. (2004). Minimal unsatisfiable sets: Classification and bounds. In M. J. Maher (Ed.), Advances in computer science—ASIAN 2004, LNCS (Vol. 3321, pp. 330–342). Springer.

Davydov, G., Davydova, I., & Büning, H. K. (1998). An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF. Annals of Mathematics and Artificial Intelligence, 23(3–4), 229–245.

Eén, N., & Sörensson, N. (2003). An extensible SAT-solver. In Proceedings of the 6th international conference on theory and applications of satisfiability testing (SAT-2003), LNCS (Vol. 2919, pp. 502–518).

Fleischner, H., Kullmann, O., & Szeider, S. (2002). Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference. Theoretical Computer Science, 289(1), 503–516.

Gershman, R., Koifman, M., & Strichman, O. (2006). Deriving small unsatisfiable cores with dominators. In Proceedings of the 18th international conference on computer aided verification (CAV’06) (pp. 109–122).

Goldberg, E., & Novikov, Y. (2003). Verification of proofs of unsatisfiability for CNF formulas. In Proceedings of the conference on design, automation, and test in Europe (DATE’03) (pp. 10886–10891).

Grégoire, É., Mazure, B., & Piette, C. (2007). Local-search extraction of MUSes. Constraints, 12(3), 325–344.

Hachtel, G. D., & Somenzi, F. (1996). Logic synthesis and verification algorithms. Kluwer Academic.

Han, B., & Lee, S.-J. (1999). Deriving minimal conflict sets by CS-trees with mark set in diagnosis from first principles. IEEE Transactions on Systems, Man, and Cybernetics, Part B, 29(2), 281–286, April.

Huang, J. (2005). MUP: A minimal unsatisfiability prover. In Proceedings of the 10th Asia and South Pacific design automation conference (ASP-DAC’05) (pp. 432–437).

Jain, H., Kroening, D., Sharygina, N., & Clarke, E. (2005). Word level predicate abstraction and refinement for verifying RTL verilog. In Proceedings of the 42nd annual conference on design automation (DAC’05) (pp. 445–450).

Kullmann, O. (2000). An application of matroid theory to the SAT problem. In 15th annual IEEE conference on computational complexity (pp. 116–124), July.

Kurshan, R. P. (1994). Computer aided verification of coordinating processes. Princeton University Press, Princeton, NJ.

Liffiton, M. H., & Sakallah, K. A. (2005). On finding all minimally unsatisfiable subformulas. In Proceedings of the 8th international conference on theory and applications of satisfiability testing (SAT-2005), LNCS (Vol. 3569, pp. 173–186).

Liffiton, M. H., & Sakallah, K. A. (2008). Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning, 40(1), 1–33, January.

Lynce, I., & Marques-Silva, J. (2004). On computing minimum unsatisfiable cores. In The 7th international conference on theory and applications of satisfiability testing (SAT-2004).

Mneimneh, M. N., Lynce, I., Andraus, Z. S., Silva, J. P. M., & Sakallah, K. A. (2005). A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas. In Proceedings of the 8th international conference on theory and applications of satisfiability testing (SAT-2005), LNCS (Vol. 3569, pp. 467–474).

Nam, G.-J., Aloul, F. A., Sakallah, K. A., & Rutenbar, R. A. (2004). A comparative study of two Boolean formulations of FPGA detailed routing constraints. IEEE Transactions on Computers, 53(6), 688–696.

Oh, Y., Mneimneh, M. N., Andraus, Z. S., Sakallah, K. A., & Markov, I. L. (2004). AMUSE: A minimally-unsatisfiable subformula extractor. In Proceedings of the 41st annual conference on design automation (DAC’04) (pp. 518–523).

Papadimitriou, C. H., & Wolfe, D. (1988). The complexity of facets resolved. Journal of Computer and System Sciences, 37(1), 2–13.

Sinz, C. (2003). SAT benchmarks from automotive product configuration. Website. http://www-sr.informatik.uni-tuebingen.de/∼sinz/DC/ .

Sinz, C., Kaiser, A., & Küchlin, W. (2003). Formal methods for the validation of automotive product configuration data. Artificial Intelligence for Engineering Design, Analysis and Manufacturing, 17(1), 75–97.

Szeider, S. (2004). Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable. Journal of Computer and System Sciences, 69(4), 656–674, December.

Zhang, J., Li, S., & Shen, S. (2006). Extracting minimum unsatisfiable cores with a greedy genetic algorithm. In AI 2006: Advances in artificial intelligence, LNCS (Vol. 4304, pp. 847–856).

Zhang, L., & Malik, S. (2003). Extracting small unsatisfiable cores from unsatisfiable Boolean formula. In The 6th international conference on theory and applications of satisfiability testing (SAT-2003).

Zhang, L., & Malik, S. (2003). Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In Proceedings of the conference on design, automation, and test in Europe (DATE’03) (pp. 10880–10885).