ABSTRACT. Maximum Satisfiability (MaxSAT) is an important optimization problem with extensive applications. Among these applications, one usually benefits from having not just one single solution, but $k$ diverse solutions. Motivated by this, in this paper, we study an extension of MaxSAT, named Diversified Top-k MaxSAT (DTKMS) problem, which is to find k assignments such that each one satisfies all the hard clauses and all of them together satisfy the maximum number of soft clauses. This paper presents a local search algorithm LS-DTKMS for solving the problem, which exploits novel scoring functions to select variables and assignments. Experiments demonstrate that LS-DTKMS outperforms the top-k MaxSAT based DTKMS solvers and state-of-the-art solvers for diversified top-k clique problem.

ABSTRACT. It has been shown that Maximum Satisfiability (MaxSAT) problem instances can be effectively solved by partitioning the set of soft clauses into several disjoint sets. The partitioning methods can be based on clause weights (e.g., stratification) or based on graph representations of the formula. Afterwards, a merge procedure is applied to guarantee that an optimal solution is found.

This paper proposes a new framework called UpMax that decouples the partitioning procedure from the MaxSAT solving algorithms. As a result, new partitioning procedures can be defined independently of the MaxSAT algorithm to be used. Moreover, this decoupling also allows users that build new MaxSAT formulas to propose partition schemes based on knowledge of the problem to be solved. We illustrate this approach using several problems and show that partitioning has a large impact on the performance of unsatisfiability-based MaxSAT algorithms.

ABSTRACT. Most current complete MaxSAT algorithms fall into two categories: core-guided or implicit hitting set. The two kinds of algorithms seem to have complementary strengths in practice, so that each kind of solver is better able to handle different families of instances. This suggests that a hybrid might match and outperform either, but the techniques used seem incompatible. In this paper, we focus on PMRES, a core-guided algorithm based on max resolution. We show that PMRES implicitly discovers cores of the original formula, as has been previously shown for WPM1. Moreover, we show that in some cases, including unweighted instances, PMRES computes the optimum hitting set of these cores at each iteration. We also give a compact integer linear program which encodes this hitting set problem. Importantly, the continuous relaxation has an optimum that matches the bound computed by PMRES. This goes some way towards resolving the incompatibility of implicit hitting set and core-guided algorithms, since solvers based on the implicit hitting set algorithm typically solve the problem by encoding it as a linear program.

ABSTRACT. It is well-known that CDCL-based SAT solvers are, in a precisely defined way, equivalent to resolution. Hence, formulas that are hard for resolution will also be hard for CDCL. One of the most promising approaches to extend the power of CDCL and avoid this limitation is Satisfiability-Driven Clause Learning (SDCL), which allows a CDCL-based SAT solver to simulate more powerful proof systems by learning appropriate redundant clauses. In this paper, we present a MaxSAT-based technique that allows SDCL to learn shorter, and hence better, redundant clauses. This technique is implemented and evaluated in the MapleSAT-SDCL solver.

ABSTRACT. We continue the investigation on the relations of QCDCL and QBF resolution systems. In particular, we introduce QCDCL versions that tightly characterise QU-Resolution and (a slight variant of) long-distance Q-Resolution. We show that most QCDCL variants -- parameterised by different policies for decisions, unit propagations and reductions -- lead to incomparable systems for almost all choices of these policies.

ABSTRACT. When using a QBF solver for solving application problems encoded to quantified Boolean formulas (QBFs), mainly two things can potentially go wrong: (1) the solver could be buggy and return a wrong result or (2) the encoding is incorrect. To ensure the correctness of solvers, sophisticated fuzzing and testing techniques have been presented. To ultimately trust a solving result, solvers have to provide a proof certificate that can be independently checked. Much less attention, however, has been paid to the question how to ensure the correctness of encodings.

The validation of QBF encodings is particularly challenging because of the variable dependencies introduced by the quantifiers. In contrast to SAT, the solution of a true QBF is not simply a variable assignment, but a winning strategy. For each existential variable x, a winning strategy provides a function that defines how to set x based on the values of the universal variables that precede x in the quantifier prefix. Winning strategies for false formulas are defined dually.

In this paper, we provide a tool for validating encodings using winning strategies and interactive game play with a QBF solver. As the representation of winning strategies can get huge, we also introduce validation based on partial winning strategies. Finally, we employ winning strategies for testing if two different encodings of one problem have the same solutions.

ABSTRACT. In this paper, we present QMusExt, a tool for the extraction of minimal unsatisfiable sets (MUS)from quantified Boolean formulas (QBFs) in prenex conjunctive normal form (PCNF). Our tool generalizes an efficient algorithm for MUS extraction from propositional formulas that analyses and rewrites resolution proofs generated by SAT solvers.

In addition to extracting unsat cores from false formulas in PCNF, we apply QMusExt also to obtain satisfiable cores from q-resolutions proofs of true formulas in prenex disjunctive normal form(PDNF).