Abstract
Given an inconsistent set of constraints, an often studied problem is to compute an irreducible subset of the constraints which, if relaxed, enable the remaining constraints to be consistent. In the case of unsatisfiable propositional formulas in conjunctive normal form, such irreducible sets of constraints are referred to as Minimal Correction Subsets (MCSes). MCSes find a growing number of applications, including the approximation of maximum satisfiability and as an intermediate step in the enumeration of minimal unsatisfiability. A number of efficient algorithms have been proposed in recent years, which exploit a wide range of insights into the MCS extraction problem. One open question is to find the best worst-case number of calls to a SAT oracle, when the calls to the oracle are kept simple, and given reasonable definitions of simple SAT oracle calls. This paper develops novel algorithms for computing MCSes which, in specific settings, are guaranteed to require asymptotically fewer than linear calls to a SAT oracle, where the oracle calls can be viewed as simple. The experimental results, obtained on existing problem instances, demonstrate that the new algorithms contribute to improving the state of the art.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
This is the case for example with the analysis of infeasible systems of linear inequalities [10].
- 2.
Nevertheless, irreducible inconsistent sets of linear inequalities have been studied for more than a century [10].
- 3.
By exploiting the reduction of MCS extraction to MSMP [29], a wealth of different MUS extraction algorithms can be used for MCS extraction, including the insertion-based algorithm.
- 4.
Available at http://logos.ucd.ie/web/doku.php?id=mcsxl.
References
Bacchus, F., Davies, J., Tsimpoukelli, M., Katsirelos, G.: Relaxation search: a simple way of managing optional clauses. In: AAAI, pp. 835–841 (2014)
Bacchus, F., Katsirelos, G.: Using minimal correction sets to more efficiently compute minimal unsatisfiable sets. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 70–86. Springer, Heidelberg (2015)
Bailey, J., Stuckey, P.J.: Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2004. LNCS, vol. 3350, pp. 174–186. Springer, Heidelberg (2005)
Bakker, R.R., Dikker, F., Tempelman, F., Wognum, P.M.: Diagnosing and solving over-determined constraint satisfaction problems. In: IJCAI, pp. 276–281 (1993)
Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun. 25(2), 97–116 (2012)
Ben-Eliyahu, R., Dechter, R.: On computing minimal models. Ann. Math. Artif. Intell. 18(1), 3–27 (1996)
Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press, Amsterdam (2009)
Birnbaum, E., Lozinskii, E.L.: Consistent subsets of inconsistent systems: structure and behaviour. J. Exp. Theor. Artif. Intell. 15(1), 25–46 (2003)
Cayrol, C., Lagasquie-Schiex, M.-C., Schiex, T.: Nonmonotonic reasoning: from complexity to algorithms. Ann. Math. Artif. Intell. 22(3–4), 207–236 (1998)
Chinneck, J.W.: Feasibility Infesasibility in Optimization: Algorithms and Computational Methods. International Series in Operations Research & Management Science, vol. 118. Springer, Heidelberg (2008)
Chinneck, J.W., Dravnieks, E.W.: Locating minimal infeasible constraint sets in linear programs. INFORMS J. Comput. 3(2), 157–168 (1991)
de Siqueira J.L.N., Puget, J.: Explanation-based generalisation of failures. In: ECAI, pp. 339–344 (1988)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). https://github.com/niklasso/minisat
Felfernig, A., Schubert, M., Zehentner, C.: An efficient diagnosis algorithm for inconsistent constraint sets. AI EDAM 26(1), 53–62 (2012)
Feydy, T., Somogyi, Z., Stuckey, P.J.: Half reification and flattening. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 286–301. Springer, Heidelberg (2011)
Grégoire, É., Lagniez, J., Mazure, B.: An experimentally efficient method for (MSS, coMSS) partitioning. In: AAAI, pp. 2666–2673 (2014)
Grégoire, É., Mazure, B., Piette, C.: On approaches to explaining infeasibility of sets of boolean clauses. In: ICTAI, pp. 74–83 (2008)
Hemery, F., Lecoutre, C., Sais, L., Boussemart, F.: Extracting MUCs from constraint networks. In: ECAI, pp. 113–117 (2006)
Ignatiev, A., Previti, A., Liffiton, M.H., Marques-Silva, J.: Smallest MUS extraction with minimal hitting set dualization. In: CP, pp. 173–182 (2015)
Jampel, M.: A brief overview of over-constrained systems. In: Jampel, M., Maher, M.J., Freuder, E.C. (eds.) CP-WS 1995. LNCS, vol. 1106, pp. 1–22. Springer, Heidelberg (1996)
Janota, M., Marques-Silva, J.: On the query complexity of selecting minimal sets for monotone predicates. Artif. Intell. 233, 73–83 (2016)
Junker, U.: QuickXplain: Preferred explanations and relaxations for over-constrained problems. In: AAAI, pp. 167–172 (2004)
Kavvadias, D.J., Sideri, M., Stavropoulos, E.C.: Generating all maximal models of a boolean expression. Inf. Process. Lett. 74(3–4), 157–162 (2000)
Kullmann, O., Marques-Silva, J.: Computing maximal autarkies with few and simple oracle queries. In: Heule, M. (ed.) SAT 2015. LNCS, vol. 9340, pp. 138–155. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24318-4_11
Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning 40(1), 1–33 (2008)
Mangal, R., Zhang, X., Kamath, A., Nori, A.V., Naik, M.: Scaling relational inference using proofs and refutations. In: AAAI (2016)
Marques-Silva, J., Heras, F., Janota, M., Previti, A., Belov, A.: On computing minimal correction subsets. In: IJCAI, pp. 615–622 (2013)
Marques-Silva, J., Janota, M.: Computing minimal sets on propositional formulae I: problems & reductions. CoRR, abs/1402.3011 (2014)
Marques-Silva, J., Janota, M., Belov, A.: Minimal sets over monotone predicates in boolean formulae. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 592–607. Springer, Heidelberg (2013)
Marques-Silva, J., Previti, A.: On computing preferred MUSes and MCSes. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 58–74. Springer, Heidelberg (2014)
Mencía, C., Marques-Silva, J.: Efficient relaxations of over-constrained CSPs. In: ICTAI, pp. 725–732 (2014)
Mencía, C., Previti, A., Marques-Silva, J.: Literal-based MCS extraction. In: IJCAI, pp. 1973–1979 (2015)
Nöhrer, A., Biere, A., Egyed, A.: Managing SAT inconsistencies with HUMUS. In: VaMoS, pp. 83–91 (2012)
O’Callaghan, B., O’Sullivan, B., Freuder, E.C.: Generating corrective explanations for interactive constraint satisfaction. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 445–459. Springer, Heidelberg (2005)
Papadimitriou, C.H.: Computational Complexity. Addison Wesley, Boston (1994)
Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57–95 (1987)
Rosa, E.D., Giunchiglia, E.: Combining approaches for solving satisfiability problems with qualitative preferences. AI Commun. 26(4), 395–408 (2013)
Rosa, E.D., Giunchiglia, E., Maratea, M.: Solving satisfiability problems with preferences. Constraints 15(4), 485–515 (2010)
Walter, R., Felfernig, A., Kuchlin, W.: Inverse QUICKXPLAIN vs. MAXSAT - a comparison in theory and practice. In: Configuration Workshop, volume CEUR 1453, pp. 97–104 (2015)
Acknowledgement
This work was partly funded by grant TIN2013-46511-C2-2-P.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Mencía, C., Ignatiev, A., Previti, A., Marques-Silva, J. (2016). MCS Extraction with Sublinear Oracle Queries. In: Creignou, N., Le Berre, D. (eds) Theory and Applications of Satisfiability Testing – SAT 2016. SAT 2016. Lecture Notes in Computer Science(), vol 9710. Springer, Cham. https://doi.org/10.1007/978-3-319-40970-2_21
Download citation
DOI: https://doi.org/10.1007/978-3-319-40970-2_21
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-40969-6
Online ISBN: 978-3-319-40970-2
eBook Packages: Computer ScienceComputer Science (R0)