Journal on Satisfiability, Boolean Modeling and Computation ISSN:
JSAT is an open access peer reviewed journal, publishing high quality original research papers and
survey papers which evidently contribute to deeper insight. It is an electronic medium, guaranteeing
JSAT volume 11 Special volume on SAT 2018 Competitions and Evaluations
Guest editors: Martina Seidl and Luca Pulina
This volume is dedicated to the competitive events organized around the SAT 2018
conference during FLoC 2018, namely:
Abstract: 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 reduce the computation time of the solver by orders of magnitude. In this paper, we present the preprocessor HQSpre that was developed for Dependency Quantified Boolean Formulas (DQBFs) and that generalizes different preprocessing techniques for SAT and QBF problems to DQBF. We give a presentation of the underlying theory together with detailed proofs as well as implementation details contributing to the efficiency of the preprocessor. HQSpre has been used with obvious success by the winners of the DQBF track, and, even more interestingly, the QBF tracks of QBFEVAL’18.
Abstract: 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. Maximum satisfiability (MaxSAT) is a well-known optimization version of SAT, which can be solved with a series of calls to a SAT oracle. Based on this fact and motivated by the ideas underlying the PySAT toolkit, this paper describes and evaluates RC2 (stands for relaxable cardinality constraints), a new core-guided MaxSAT solver written in Python, which won both unweighted and weighted categories of the main track of MaxSAT Evaluation 2018.
Abstract: 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.
Abstract: 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.
Abstract: 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
Abstract: 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.
Abstract: 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 (PCNF) incorporating an efficient Skolem and Herbrand function extraction.
Extracting witnesses from solving is especially important as it enables the certification of the solver's verdict and it is the foundation for applications built on QBF, like verification and synthesis.
Later, the algorithmic ideas were extended to non-prenex and negation normal form formulas, leading the way for improved performance in solving and function extraction.
The implementations of the algorithms in the solvers CAQE and QuAbS won the QBF competition (QBFEVAL'18) in their respective categories, prenex CNF and prenex non-CNF.
Abstract: DepQBF is a search-based quantified Boolean formula (QBF) solver
implementing the QCDCL paradigm. We submitted DepQBF as part of
several tool packages to the QBFEVAL'18 competition, which was part of the FLoC
Olympic Games 2018. These packages
integrate DepQBF as a back end QBF solver and a preprocessing front end
called QBFRelay. This front end consists of a shell script that runs
several preprocessors in multiple rounds on a given QBF,
thus resulting in incremental preprocessing. QBFRelay employs publicly
available preprocessors developed by the QBF community and,
additionally, our novel preprocessor QRATPre+ that is based on a
generalization of the \qrat proof system. We present an overview of
DepQBF, QRATPre+, and QBFRelay and report on the performance of our
submissions, which were awarded a medal in the FLoC Olympic Games.
Abstract: 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
Abstract: 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.