Journal on Satisfiability, Boolean Modeling and Computation ISSN: 1574-0617

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 fast publication.

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:

JSAT promotes Open Science. As such, the authors are encouraged to provide additional resources to complement their article:

The above icons before the title of the article mean that the article is complemented by those resources. Articles provided all of them are awarded the open science badge.

Table of Contents

Notes from the Guest Editors, Luca Pulina, Martina Seidl, 1.
The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation, Ralf Wimmer, Christoph Scholl, Bernd Becker, 3-52. Preprocessing DQBF Solver technology Henkin quantifiers
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.
open science RC2: an Efficient MaxSAT Solver, Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva, 53-64. Maximum Satisfiability Relaxable/Soft Cardinality Constraints Python
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.
Software Benchmarks Data Scripts/Tools
GhostQ System Description, William Klieber, 65-72. QBF DPLL non-clausal Plaisted-Greenbaum encoding
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.
open science Open-WBO-Inc: Approximation Strategies for Incomplete Weighted MaxSAT, Saurabh Joshi, Prateek Kumar, Sukrut Rao, Ruben Martins, 73-97. MaxSAT Incomplete Weighted Approximation
Abstract: Incomplete MaxSAT solving aims to quickly find a solution that attempts to minimize the sum of the weights of unsatis fied 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 unsatis fiable 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.
Software Benchmarks Data Scripts/Tools
MaxSAT Evaluation 2018: New Developments and Detailed Results, Fahiem Bacchus, Matti Järvisalo, Ruben Martins, 99-131. MaxSAT Maximum Satis ability Empirical Evaluation Solvers Benchmarks
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 evaluation.
Software Benchmarks Data
SAT Competition 2018, Marijn J. H. Heule, Matti Järvisalo, Martin Suda, 133-154. SAT Boolean satisfiability empirical evaluation solvers benchmarks
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.
Software Benchmarks Data
CAQE and QuAbS: Abstraction Based QBF Solvers, Leander Tentrup, 155-210. QBF solver certification conjunctive normal form negation normal form
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.
Software Benchmarks Data
QBFRelay, QRATPre+, and DepQBF: Incremental Preprocessing Meets Search-Based QBF Solving, Florian Lonsing, 211-220. QBF solving Q-resolution QCDCL preprocessing QRAT proof system
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.
Software Benchmarks Data
open science The SMT Competition 2015-2018, Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, Giles Reger, 221-259. SMT solver SMT-COMP SMT-LIB Satisfiability Modulo Theories Competitions
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 computation performed.
Software Benchmarks Data Scripts/Tools
Qute in the QBF Evaluation 2018, Tomás Peitl, Friedrich Slivovsky, Stefan Szeider, 261-272. QBF
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.
Software Benchmarks Data