We present our anytime MaxSAT solver TT-Open-WBO-Inc, focusing on its evolution since the initial version that won both of the weighted incomplete tracks of MaxSAT Evaluation 2019 (MSE19). The solver’s MSE20 version claimed victory in these tracks at MSE20 and secured second place in both unweighted incomplete tracks. The major innovation in the MSE20 version was the integration of SAT-based local search. The contributions of this paper include: (1) Introducing a previously unpublished variant of the SAT-based local search algorithm Polosat, Polosat-OBV, applied by default already in the MSE20 version, and showing its superiority for weighted solving; (2) Describing and analyzing TT-Open-WBO-Inc’s unweighted component, not studied in previous work; (3) Demonstrating that integrating the local search algorithm SATLike into TT-Open-WBO-Inc as a preprocessor enables it to outperform the winners of MSE20 in all four incomplete tracks.
Recently, the proof system MICE for the model counting problem #SAT was introduced by Fichte, Hecher and Roland (SAT’22). As demonstrated by Fichte et al., the system MICE can be used for proof logging for state-of-the-art #SAT solvers. We perform a proof-complexity study of MICE. For this we first simplify the rules of MICE and obtain a calculus MIC E ′ that is polynomially equivalent to MICE. We then establish an exponential lower bound for the number of proof steps in MIC E ′ (and hence also in MICE) for a specific family of CNFs. We also explain a tight connection between MIC E ′ proofs and decision DNNFs.
We give an analogue of the Riis Complexity Gap Theorem for Quantified Boolean Formulas (QBFs). Every first-order sentence φ without finite models gives rise to a sequence of QBFs whose minimal refutations in tree-like QResolution are either of polynomial size (if φ has no models) or at least exponential in size (if φ has some infinite model). However, differently from the translations to propositional logic, the translation to QBF must be given additional structure in order for the polynomial upper bound to hold in treelike Q-Resolution. This extra structure is not needed in the system tree-like ∀Exp+Res, where we see the complexity gap on a natural translation to QBF.
OMTPlan is a Python platform for optimal planning in numeric domains via reductions to Satisfiability Modulo Theories (SMT) and Optimization Modulo Theories (OMT). Currently, OMTPlan supports the expressive power of PDDL2.1 level 2 and features procedures for both satisficing and optimal planning. OMTPlan provides an open, easy to extend, yet efficient implementation framework. These goals are achieved through a modular design and the extensive use of state-of-the-art systems for SMT/OMT solving.
We define a distance function on propositional formulas in CNF as a measure of non-isomorphism of formulas: the larger the distance between two formulas is, the further they are from being isomorphic. This distance induces a metric on isomorphism classes of formulas. We show how this distance can be used for SAT solving, namely for per-instance algorithm selection where there is a “portfolio” of SAT solvers and there is a “meta-solver” that chooses a solver from the portfolio for a given input formula.
We consider the problem of planning with arithmetic theories, and focus on generating optimal plans for numeric domains with constant and state-dependent action costs. Solving these problems efficiently requires a seamless integration between propositional and numeric reasoning. We propose a novel approach that leverages Optimization Modulo Theories (OMT) solvers to implement a domain-independent optimal theory-planner. We present a new encoding for optimal planning in this setting and we evaluate our approach using well-known, as well as new, numeric benchmarks.
It is shown that disjunction of two switch-lists can blow up the representation size exponentially. Since switch-lists can be negated without any increase in size, this shows that conjunction of switch-lists also leads to an exponential blow-up in general.
This paper is a system description of the anytime MaxSAT solver TT-Open-WBO-Inc, which won both of the weighted incomplete tracks of MaxSAT Evaluation 2019. We implemented the recently introduced polarity and variable selection heuristics, TORC and TSB, respectively, in the Open-WBO-Inc-BMO algorithm within the open-source anytime MaxSAT solver Open-WBO-Inc. As a result, the solver is substantially more efficient.
Backdoor sets for the class CNF(2) of CNF-formulas in which every variable has at most two occurrences are studied in terms of parameterized complexity. The question whether there exists a CNF(2)-backdoor set of size k is hard for the class W[2], for both weak and strong backdoors, and in both cases it becomes fixed-parameter tractable when restricted to inputs in d-CNF for a fixed d. Besides that, it is shown that the problem of finding weak backdoor sets is W[2]-complete, for certain tractable cases. These are the first completeness results in lower levels of the W-hierarchy for any backdoor set problems.
Recent work proposed a toolkit PySAT aiming at fast and easy prototyping with propositional satisfiability (SAT) oracles in Python, which enabled one to exploit the power of the original implementations of the state-of-the-art SAT solvers in Python.
The series of MaxSAT Evaluations, organized yearly since 2006, has been the main forum for evaluating the state of the art in solvers for the Boolean optimization paradigm of maximum satisfiability (MaxSAT). This article provides an overview of the 2018 MaxSAT Evaluation, including a description of the main changes made in 2017 under a new organizing team, an overview of the solvers and benchmarks submitted in 2018, and detailed results of the 2018 evaluation.
GhostQ is a DPLL-based non-CNF QBF solver.This paper describes a noteworthy feature of GhostQ that has not yet been described in the peer-reviewed literature: support for Plaisted-Greenbaum encoding.For CNF inputs, GhostQ attempts to perform reverse engineering on the CNF formula to create an equivalent circuit representation.Support for reversing the Plaisted-Greenbaum transformation was added to the existing capability for reversing the Tseitin transformation.
The International Satisfiability Modulo Theories Competition is an annual competition between Satisfiability Modulo Theories (SMT) solvers. The 2018 edition of the competition was part of the FLoC Olympic Games, which comprised 14 competitions in various areas of computational logic. We report on the design and selected results of the SMT Competition during the last FLoC Olympiad, from 2015 to 2018. These competitions set several new records regarding the number of participants, number of benchmarks used, and amount of computation performed.
We present a detailed description, analysis, and evaluation of the clausal abstraction approach for solving quantified Boolean formulas (QBF). The clausal abstraction algorithm started as a solving algorithm for QBFs in prenex conjunctive normal form
Incomplete MaxSAT solving aims to quickly find a solution that attempts to minimize the sum of the weights of unsatisfied soft clauses without providing any optimality guarantees. In this paper, we propose two approximation strategies for improving incomplete weighted MaxSAT solving. In one of the strategies, we cluster the weights and approximate them with a representative weight. In another strategy, we break up the problem of minimizing the sum of weights of unsatisfiable clauses into multiple minimization subproblems. We have implemented these strategies in a tool Open-WBO-Inc. Using the subproblem minimization strategy, Open-WBO-Inc placed first and second in the weighted incomplete tracks in the MaxSAT Evaluation 2018 whereas the strategy based on weight approximation was placed fourth. We compare these strategies with the best incomplete MaxSAT solvers on benchmarks taken from MaxSAT Evaluation 2017 and MaxSAT Evaluation 2018 and show that the strategies proposed are competitive with the best of the solvers.
Boolean satisfiability (SAT) and related solver competitions organized during the last two decades have been a stimulating force to improve SAT solvers and related technologies. These competitions have encouraged the development of novel algorithms and optimized implementation-level techniques and data structures to increase the practical performance and robustness of solvers. The competition benchmark suites are commonly used by the research community as the standard test set to evaluate progress. Additionally, the competitions provide large amounts of openly available data on solver performance on a large spectrum of benchmark families that encode important real and artificial combinatorial problems. Overall, much more can be learned from such solver competitions than merely the ranking of the participating tools. For this special issue, we invited organizers as well as participants of SAT-related competitions and comparative events to report on their contributions. This includes the event organization itself as well as the description of solver techniques and thorough analysis and insights into the data produced by the competitions. In a two-stage reviewing process, we selected ten papers to be included in this special issue. In each of the two reviewing stages, each contribution was reviewed by at least three independent referees. This special issue contains the reports of three different competitions: the SAT 2018 Competition, the MaxSAT Competition 2018, as well as the SMT 2018 Competition. All of these competitions were part of the FLoC Olympic Games, the second edition of an event that happens every four years and which provides a common platform to very heterogeneous competitions. The other seven papers describe competition participants in detail and document solvers and preprocessors for MaxSAT, QBF, as well as DQBF. We thank all the contributors of the papers for publishing their competition reports and their work on competitive tools in this special issue. Last but not least, we want to express our deepest gratitude to the referees who supported us in the selection of the content of this special issue by providing careful and timely reports.
The SAT Competition series, which started in 2002, is arguably one of the central driving forces of SAT solver development and its benchmark suites have been used in evaluations of hundreds of research papers. This article provides an overview of the 2018 edition of the SAT Competitions, including the competition tracks and rules, benchmark submission and selection, and the results of the competition focusing on the best-performing solvers.
Preprocessing turned out to be an essential step for SAT, QBF, and DQBF solvers to reduce/modify the number of variables and clauses of the formula, before the formula is passed to the actual solving algorithm. These preprocessing techniques often re
Qute is a solver for Quantified Boolean Formulas (QBFs) based on Quantified Conflict-Driven Constraint Learning (QCDCL).Its main distinguishing feature is dependency learning, a lazy technique for relaxing restrictions on the order of variable assignments imposed by nested quantifiers.In this short note, we describe the configurations of Qute submitted to QBFEval'18, along with the parameter tuning process that went into creating them.
