Abstract
Even when it has been shown that no solution exists for a particular constraint satisfaction problem, one may still aim to restore consistency by relaxing the minimal number of constraints. In the context of a Boolean formula like SAT, such a relaxation is referred to as a Minimal Correction Subset (MCS). In the context of SAT, identifying MCSs for an instance is relevant in a wide range of applications, including MaxSAT solution approximation and Minimal Unsatisfiable Subset (MUS) enumeration. However, while there are a number of existing approaches to this problem, in this paper we demonstrate how performance can be significantly improved by employing algorithm portfolios. Yet, instead of applying the standard approach of selecting a single solver for the instance at hand, we present a new technique that within a predetermined timeout switches between enumeration algorithms multiple times. Through experimental study, this new approach is shown to outperform any possible optimal portfolio that solely relies on solvers that run uninterrupted for the allotted time.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bailey, J., Stuckey, P.J.: Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In: Practical Aspects of Declarative Languages, pp. 174–186 (2005)
Ben-Eliyahu, R., Dechter, R.: On computing minimal models. Ann. Math. Artif. Intell. 18(1), 3–27 (1996)
Birnbaum, E., Lozinskii, E.L.: Consistent subsets of inconsistent systems: structure and behaviour. J. Exp. Theor. Artif. Intell. 15(1), 25–46 (2003)
Collautti, M., Malitsky, Y., Mehta, D., O’Sullivan, B.: Snnap: Solver-based nearest neighbor for algorithm portfolios. In: Blockeel, H., Kersting, K., Nijssen, S., Železný, F. (eds.) ECML PKDD 2013, Part III. LNCS (LNAI), vol. 8190, pp. 435–450. Springer, Heidelberg (2013)
Felfernig, A., Schubert, M., Zehentner, C.: An efficient diagnosis algorithm for inconsistent constraint sets. AI EDAM 26(1), 53–62 (2012)
Gomes, C., Selman, B., Kautz, H.: Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. J. of Automated Reasoning, 67–100 (2000)
Hurley, B., O’Sullivan, B.: Adaptation in a CBR-based solver portfolio for the satisfiability problem. In: Agudo, B.D., Watson, I. (eds.) ICCBR 2012. LNCS, vol. 7466, pp. 152–166. Springer, Heidelberg (2012)
Jampel, M., Freuder, E.C., Maher, M.J. (eds.): Over-Constrained Systems. Springer (1996)
Junker, U.: QUICKXPLAIN: Preferred explanations and relaxations for over-constrained problems. In: AAAI, pp. 167–172 (2004)
Kadioglu, S., Malitsky, Y., Sabharwal, A., Samulowitz, H., Sellmann, M.: Algorithm selection and scheduling. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 454–469. Springer, Heidelberg (2011)
Kotthoff, L., Gent, I., Miguel, I.P.: An evaluation of machine learning in algorithm selection for search problems. AI Communications (2012)
Liffiton, M., Sakallah, K.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reasoning 40(1), 1–33 (2008)
Malitsky, Y., Sellmann, M.: Instance-specific algorithm configuration as a method for non-model-based portfolio generation. In: Beldiceanu, N., Jussien, N., Pinson, É. (eds.) CPAIOR 2012. LNCS, vol. 7298, pp. 244–259. Springer, Heidelberg (2012)
Marques-Silva, J., Heras, F., Janota, M., Previti, A., Belov, A.: On computing minimal correction subsets. In: IJCAI (2013)
O’Callaghan, B., O’Sullivan, B., Freuder, E.C.: Generating corrective explanations for interactive constraint satisfaction. In: Principles and Practice of Constraint Programming, pp. 445–459 (2005)
O’Mahony, E., Hebrard, E., Holland, A., Nugent, C., O’Sullivan, B.: Using case-based reasoning in an algorithm portfolio for constraint solving. In: AICS (2008)
Pulina, L., Tacchella, A.: A self-adaptive multi-engine solver for quantified boolean formulas. Constraints 14(1), 80–116 (2009)
Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57–95 (1987)
Silverthorn, B., Miikkulainen, R.: Latent class models for algorithm portfolio methods. AAAI (2010)
Sinz, C., Kaiser, A., Küchlin, W.: Formal methods for the validation of automotive product configuration data. AI EDAM 17(1), 75–97 (2003)
Soh, T., Inoue, K.: Identifying necessary reactions in metabolic pathways by minimal model generation. In: ECAI, pp. 277–282 (2010)
Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Satzilla: Portfolio-based algorithm selection for SAT. CoRR (2011)
Xu, L., Hutter, F., Shen, J., Hoos, H.H., Leyton-Brown, K.: Satzilla2012: Improved algorithm selection based on cost-sensitive classification models. SAT Competition (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Malitsky, Y., O’Sullivan, B., Previti, A., Marques-Silva, J. (2014). A Portfolio Approach to Enumerating Minimal Correction Subsets for Satisfiability Problems. In: Simonis, H. (eds) Integration of AI and OR Techniques in Constraint Programming. CPAIOR 2014. Lecture Notes in Computer Science, vol 8451. Springer, Cham. https://doi.org/10.1007/978-3-319-07046-9_26
Download citation
DOI: https://doi.org/10.1007/978-3-319-07046-9_26
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-07045-2
Online ISBN: 978-3-319-07046-9
eBook Packages: Computer ScienceComputer Science (R0)