Quantified maximum satisfiability: a core-guided approach

Alexey Ignatiev, Mikoláš Janota, Joao Marques-Silva

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

12 Citations (Scopus)


In recent years, there have been significant improvements in algorithms both for Quantified Boolean Formulas (QBF) and for Maximum Satisfiability (MaxSAT). This paper studies the problem of solving quantified formulas subject to a cost function, and considers the problem in a quantified MaxSAT setting. Two approaches are investigated. One is based on relaxing the soft clauses and performing a linear search on the cost function. The other approach, which is the main contribution of the paper, is inspired by recent work on MaxSAT, and exploits the iterative identification of unsatisfiable cores. The paper investigates the application of these approaches to the concrete problem of computing smallest minimal unsatisfiable subformulas (SMUS), a decision version of which is a well-known problem in the second level of the polynomial hierarchy. Experimental results, obtained on representative problem instances, indicate that the core-guided approach for the SMUS problem outperforms the use of linear search over the values of the cost function. More significantly, the core-guided approach also outperforms the state-of-the-art SMUS extractor Digger.

Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing, SAT 2013 - 16th International Conference, Proceedings
Number of pages17
ISBN (Print)9783642390708
Publication statusPublished - 2013
Externally publishedYes
Event16th International Conference on Theory and Applications of Satisfiability Testing, SAT 2013 - Helsinki, Finland
Duration: 8 Jul 201312 Jul 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7962 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference16th International Conference on Theory and Applications of Satisfiability Testing, SAT 2013

Cite this