A number of maxsat algorithms are based on the idea of generating unsatisfiable cores. A common approach is to use these cores to construct cardinality (or pseudo-boolean) constraints that are then added to the formula. Each iteration extracts a core of the modified formula that now contains cardinality constraints. Hence, the cores generated are not just cores of the original formula, they are cores of more complicated formulas. The effectiveness of core based algorithms for maxsat is strongly affected by the structure of the cores of the original formula. Hence it is natural to ask the question: how are the cores found by these algorithms related to the cores of the original formula? In this paper we provide a formal characterization of this relationship. Our characterization allows us to identify a possible inefficiency in these algorithms. Hence, finding ways to address it may lead to performance improvements in these state-of-the-art maxsat algorithms. © 2014 Springer International Publishing Switzerland.
CITATION STYLE
Bacchus, F., & Narodytska, N. (2014). Cores in core based MaxSat algorithms: An analysis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8561 LNCS, pp. 7–15). Springer Verlag. https://doi.org/10.1007/978-3-319-09284-3_2
Mendeley helps you to discover research relevant for your work.