Local-search Extraction of MUSes
Tóm tắt
Từ khóa
Tài liệu tham khảo
Bailey, J., & Stuckey, P. J. (2005). Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In International Symposium on Practical Aspects of Declarative Languages (PADL’05), pages 174–186.
Boussemart, F., Hémery, F., Lecoutre, C., & Saïs, L. (2004). Boosting systematic search by weighting constraints. In European Conference on Artificial Intelligence (ECAI’04), pages 146–150.
Brisoux, L., Grégoire, É., & Saïs, L. (2001). Checking depth-limited consistency and inconsistency in knowledge-based systems. Int. J. Intell. Syst. 16(3): 333–360.
Bruni, R. (2003). Approximating minimal unsatisfiable subformulae by means of adaptive core search. Discrete Appl. Math. 130(2): 85–100.
Bruni, R. (2005). On exact selection of minimally unsatisfiable subformulae. Ann. Math. Artif. Intell. 43(1): 35–50.
Büning, H. K. (2000). On subclasses of minimal unsatisfiable formulas. Discrete Appl. Math. 107(1–3): 83–98.
Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem proving. J. Assoc. Comput. Mach. 5(7): 394–397.
Davydov, G., Davydova, I., & Büning, H. K. (1998). An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF. Ann. Math. Artif. Intell. 23(3,4): 229–245.
DIMACS (1993). Benchmarks on SAT. ftp://dimacs.rutgers.edu/pub/challenge/-satisfiability/ .
Eiter, T., & Gottlob, G. (1992). On the complexity of propositional knowledge base revision, updates and counterfactual. Artif. Intell. 57: 227–270.
Fleischner, H., Kullman, O., & Szeider, S. (2002). Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference. Theor. Comput. Sci. 289(1): 503–516.
Grégoire, É., Mazure, B., & Piette, C. (2007). Boosting a complete technique to find MSSes and MUSes thanks to a local search oracle. In International Joint Conference on Artificial Intelligence (IJCAI’07), vol. 2, pages 2300–2305.
Grégoire, É., & Ansart, D. (2000). Overcoming the Christmas tree syndrome. Int. J. Artif. Intell. Tools (IJAIT) 9(2): 97–111.
Grégoire, É., Mazure, B., & Saïs, L. (2002). Using failed local search for SAT as an oracle for tackling harder A.I. problems more efficiently. In International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA’02). LNCS, number 2443, pages 51–60. Springer.
Hamscher, W., Console, L., & de Kleer, J., eds. (1992) Readings in Model-based Diagnosis. San Mateo, CA: Morgan Kaufmann.
Huang, J. (2005). MUP: A minimal unsatisfiability prover. In Asia and South Pacific Design Automation Conference (ASP-DAC’05), pages 432–437.
Junker, U. (2001). QuickXPlain: Conflict detection for arbitrary constraint propagation algorithms. In IJCAI’01 Workshop on Modelling and Solving problems with constraints (CONS-1), pages 75–82.
Kautz, H., Selman, B., & McAllester, D. (2004). Walksat in the SAT 2004 competition. In International Conference on Theory and Applications of Satisfiability Testing (SAT’04).
Kullmann, O., Lynce, I., & Marques Silva, J. P. (2006). Categorisation of clauses in conjunctive normal forms: Minimally unsatisfiable sub-clause-sets and the lean kernel. In International Conference on Theory and Applications of Satisfiability Testing (SAT’06), pages 22–35.
Liffiton, M. H., & Sakallah, K. A. (2005). On finding all minimally unsatisfiable subformulas. In International Conference on Theory and Applications of Satisfiability Testing (SAT’05), pages 173–186.
Lynce, I., & Marques-Silva, J. (2004). On computing minimum unsatisfiable cores. In International Conference on Theory and Applications of Satisfiability Testing (SAT’04).
Mazure, B., Saïs, L., & Grégoire, É. (1996). A powerful heuristic to locate inconsistent kernels in knowledge-based systems. In International Conference on Information Processing and Management of Uncertainty in Knowledge-based Systems (IPMU’96), pages 1265–1269.
Mazure, B., Saïs, L., & Grégoire, É. (1998). Boosting complete techniques thanks to local search. Ann. Math. Artif. Intell. 22: 319–322.
Mneimneh, M. N., Lynce, I., Andraus, Z. S., Marques Silva, J. P., & Sakallah, K. A. (2005). A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas. In International Conference on Theory and Applications of Satisfiability Testing (SAT’05), pages 467–474.
Oh, Y., Mneimneh, M. N., Andraus, Z. S., Sakallah, K. A., & Markov, I. L. (2004). AMUSE: a minimally-unsatisfiable subformula extractor. In Design Automation Conference (DAC’04), pages 518–523.
Papadimitriou, C. H., & Wolfe, D. (1988). The complexity of facets resolved. J. Comput. Syst. Sci. 37(1): 2–13.
SATLIB (2004). Benchmarks on SAT. http://www.intellektik.informatik.tu-darmstadt.de/SATLIB/benchm.html .
Zhang, L., & Malik, S. (2003). Extracting small unsatisfiable cores from unsatisfiable boolean formula. In International Conference on Theory and Applications of Satisfiability Testing (SAT’03).