Journal on Satisfiability, Boolean Modeling and Computation - Volume 11, issue 1

Authors: Pulina, Luca | Seidl, Martina

Article Type: Editorial

DOI: 10.3233/SAT190114

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 11, no. 1, pp. 1-1, 2019

Authors: Wimmer, Ralf | Scholl, Christoph | Becker, Bernd

Article Type: Research Article

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. Show more

Keywords: Preprocessing, DQBF, Solver technology, Henkin quantifiers

DOI: 10.3233/SAT190115

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 11, no. 1, pp. 3-52, 2019

Authors: Ignatiev, Alexey | Morgado, Antonio | Marques-Silva, Joao

Article Type: Research Article

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. Show more

Keywords: Maximum Satisfiability, Relaxable/Soft Cardinality Constraints, Python

DOI: 10.3233/SAT190116

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 11, no. 1, pp. 53-64, 2019

Authors: Klieber, William

Article Type: Research Article

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.

Keywords: QBF, DPLL, non-clausal, Plaisted-Greenbaum encoding

DOI: 10.3233/SAT190117

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 11, no. 1, pp. 65-72, 2019

Authors: Joshi, Saurabh | Kumar, Prateek | Rao, Sukrut | Martins, Ruben

Article Type: Research Article

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. Show more

Keywords: MaxSAT, Incomplete, Weighted, Approximation

DOI: 10.3233/SAT190118

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 11, no. 1, pp. 73-97, 2019

Authors: Bacchus, Fahiem | Järvisalo, Matti | Martins, Ruben

Article Type: Research Article

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.

Keywords: MaxSAT, maximum satisfiability, empirical evaluation, solvers, benchmarks

DOI: 10.3233/SAT190119

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 11, no. 1, pp. 99-131, 2019

Authors: Heule, Marijn J. H. | Järvisalo, Matti | Suda, Martin

Article Type: Research Article

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.

Keywords: SAT, Boolean satisfiability, empirical evaluation, solvers, benchmarks

DOI: 10.3233/SAT190120

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 11, no. 1, pp. 133-154, 2019

Authors: Tentrup, Leander

Article Type: Research Article

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. Show more

Keywords: QBF solver, certification, conjunctive normal form, negation normal form

DOI: 10.3233/SAT190121

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 11, no. 1, pp. 155-210, 2019

Authors: Lonsing, Florian

Article Type: Research Article

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. Show more

Keywords: QBF solving, Q-resolution, QCDCL, preprocessing, QRAT proof system

DOI: 10.3233/SAT190122

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 11, no. 1, pp. 211-220, 2019

Authors: Weber, Tjark | Conchon, Sylvain | Déharbe, David | Heizmann, Matthias | Niemetz, Aina | Reger, Giles

Article Type: Research Article

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.

Keywords: SMT solver, SMT-COMP, SMT-LIB, Satisfiability Modulo Theories, competitions

DOI: 10.3233/SAT190123

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 11, no. 1, pp. 221-259, 2019

Authors: Peitl, Tomáš | Slivovsky, Friedrich | Szeider, Stefan

Article Type: Research Article

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.

Keywords: QBF

DOI: 10.3233/SAT190124

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 11, no. 1, pp. 261-272, 2019