TY - GEN
T1 - A portfolio approach to enumerating minimal correction subsets for satisfiability problems
AU - Malitsky, Yuri
AU - O'Sullivan, Barry
AU - Previti, Alessandro
AU - Marques-Silva, Joao
PY - 2014
Y1 - 2014
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84902449417
U2 - 10.1007/978-3-319-07046-9_26
DO - 10.1007/978-3-319-07046-9_26
M3 - Conference proceeding
AN - SCOPUS:84902449417
SN - 9783319070452
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 368
EP - 376
BT - Integration of AI and OR Techniques in Constraint Programming - 11th International Conference, CPAIOR 2014, Proceedings
PB - Springer Verlag
T2 - 11th International Conference on the Integration of Artificial Intelligence (AI) and Operations Research (OR) Techniques in Constraint Programming, CPAIOR 2014
Y2 - 19 May 2014 through 23 May 2014
ER -