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

Authors: Le Berre, Daniel | Simon, Laurent

Article Type: Editorial

DOI: 10.3233/SAT190013

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 2, no. 1-4, pp. i-xiv, 2006

Authors: Eén, Niklas | Sörensson, Niklas

Article Type: Research Article

Abstract: In this paper, we describe and evaluate three different techniques for translating pseudo-boolean constraints (linear constraints over boolean variables) into clauses that can be handled by a standard SAT-solver. We show that by applying a proper mix of translation techniques, a SAT-solver can perform on a par with the best existing native pseudo-boolean solvers. This is particularly valuable in those cases where the constraint problem of interest is naturally expressed as a SAT problem, except for a handful of constraints. Translating those constraints to get a pure clausal problem will take full advantage of the latest improvements in …SAT research. A particularly interesting result of this work is the efficiency of sorting networks to express pseudo-boolean constraints. Although tangential to this presentation, the result gives a suggestion as to how synthesis tools may be modified to produce arithmetic circuits more suitable for SAT based reasoning. Show more

Keywords: pseudo-Boolean, SAT-solver, SAT translation, integer linear programming

DOI: 10.3233/SAT190014

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 2, no. 1-4, pp. 1-26, 2006

Authors: Haanpää, Harri | Järvisalo, Matti | Kaski, Petteri | Niemelä, Ilkka

Article Type: Research Article

Abstract: A family of satisfiable benchmark instances in conjunctive normal form is introduced. The instances are constructed by transforming a random regular graph into a system of linear equations followed by clausification. Schemes for introducing nonlinearity to the instances are developed, making the instances suitable for benchmarking solvers with equivalence reasoning techniques. An extensive experimental evaluation shows that state-of-the-art solvers scale exponentially in the instance size. Compared with other well-known families of satisfiable benchmark instances, the present instances are among the hardest.

Keywords: benchmarking, Boolean satisfiability, equivalence reasoning, satisfiable instances

DOI: 10.3233/SAT190015

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 2, no. 1-4, pp. 27-46, 2006

Authors: Heule, Marijn J.H. | van Maaren, Hans

Article Type: Research Article

Abstract: We introduce the march_dl satisfiability (SAT) solver, a successor of march_eq . The latter was awarded state-of-the-art in two categories during the Sat 2004 competition. The focus lies on presenting those features that are new in march_dl . Besides a description, each of these features is illustrated with some experimental results. By extending the pre-processor, using adaptive heuristics, and by using a new branching strategy, march_dl is able to solve nearly all benchmarks faster than its predecessor. Moreover, various instances which were beyond the reach of march_eq , can now be solved - relatively easily - due …to these new features. Show more

Keywords: adaptive heuristics, look-ahead, SAT solving, SAT competition

DOI: 10.3233/SAT190016

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 2, no. 1-4, pp. 47-59, 2006

Authors: Kullmann, Oliver

Article Type: Research Article

Abstract: An analysis of the SAT 2005 sub-competition on random instances is given. This year this (sub-)competition set-up was geared to establish a basic setting, focusing on the instances near the (infamous) “50% densities”, so first we have to establish a more quantitative understanding of phase transitions here. We present extended empirical results, clearly showing that the models used before, which are motivated by large-scale considerations, are inadequate at the relatively small scale considered here. Then the series’ and all individual instances used in the competition are described. We give a formal definition of the competition evaluation, and analyse the results …of the competition, looking into the details of the scoring mechanism as well as into alternative evaluation methods. Show more

Keywords: random satisfiability problems, phase transition, threshold behaviour, critical exponent, SAT competition

DOI: 10.3233/SAT190017

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 2, no. 1-4, pp. 61-102, 2006

Authors: Manquinho, Vasco M. | Roussel, Olivier

Article Type: Research Article

Abstract: The first evaluation of pseudo-Boolean solvers was organized as a subtrack of the SAT 2005 competition. The first goal of this event is to take a snapshot of the current state of the art in the field of pseudo-Boolean constraints. The second goal is to stimulate the research efforts in this field and contribute to the creation of better technologies. This paper details the organization and the results of this event.

Keywords: pseudo-Boolean, evaluation, benchmarks

DOI: 10.3233/SAT190018

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 2, no. 1-4, pp. 103-143, 2006

Authors: Narizzano, Massimo | Pulina, Luca | Tacchella, Armando

Article Type: Research Article

Abstract: This paper reports about the 2005 comparative evaluation of solvers for quantified Boolean formulas (QBFs), the third in a series of non-competitive events established with the aim of assessing the advancements in the field of QBF reasoning and related research. We evaluated thirteen solvers on a test set of more than three thousands QBFs, selected from instances submitted to the evaluation and from those available at http://www.qbflib.org . In the paper we present the evaluation infrastructure, from the criteria used to assemble the test set to the hardware set up, and we show different views about the results obtained, highlighting …the strength of different solvers and the relative hardness of the instances included in the test set. Show more

Keywords: quantified Boolean formulas, empirical evaluation, automated reasoning tools

DOI: 10.3233/SAT190019

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 2, no. 1-4, pp. 145-164, 2006

Authors: Sheini, Hossein M. | Sakallah, Karem A.

Article Type: Research Article

Abstract: This paper introduces a new hybrid method for efficiently integrating Pseudo-Boolean (PB) constraints into generic SAT solvers in order to solve PB satisfiability and optimization problems. To achieve this, we adopt the cutting-plane technique to draw inferences among PB constraints and combine it with generic implication graph analysis for conflict-induced learning. Novel features of our approach include a light-weight and efficient hybrid learning and backjumping strategy for analyzing PB constraints and CNF clauses in order to simultaneously learn both a CNF clause and a PB constraint with minimum overhead and use both to determine the backtrack level. Several techniques for …handling the original and learned PB constraints are introduced. Overall, our method benefits significantly from the pruning power of the learned PB constraints, while keeping the overhead of adding them into the problem low. In this paper, we also address two other methods for solving PB problems, namely Integer Linear Programming (ILP) and pre-processing to CNF SAT, and present a thorough comparison between them and our hybrid method. Experimental comparison of our method against other hybrid approaches is also demonstrated. Additionally, we provide details of the MiniSAT-based implementation of our solver Pueblo to enable the reader to construct a similar one. Show more

Keywords: satisfiability, SAT solver, pseudo-Boolean, inference-based learning

DOI: 10.3233/SAT190020

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 2, no. 1-4, pp. 165-189, 2006

Authors: Bailleux, Olivier | Boufkhad, Yacine | Roussel, Olivier

Article Type: Research Article

Abstract: This paper introduces a new CNF encoding of pseudo-Boolean constraints, which allows unit propagation to maintain generalized arc consistency. In the worst case, the size of the produced formula can be exponentially related to the size of the input constraint, but some important classes of pseudo-Boolean constraints, including Boolean cardinality constraints, are encoded in polynomial time and size. The proposed encoding was integrated in a solver based on the zChaff SAT solver and submitted to the PB05 evaluation. The results provide new perspectives in the field of full CNF approach of pseudo-Boolean constraints solving.

Keywords: pseudo-Boolean, SAT translation

DOI: 10.3233/SAT190021

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 2, no. 1-4, pp. 191-200, 2006

Authors: Biere, Armin | Sinz, Carsten

Article Type: Research Article

Abstract: Many SAT instances can be decomposed into connected components either initially after preprocessing or during the solution phase when new unit conflict clauses are learned. This observation allows components to be solved individually. We present a technique to handle components within a GRASP like SAT solver without requiring much change to the solver. Results obtained when applying our implementation in the SAT solver COMPSAT to a number of realistic examples show that components really do occur in practice. We also provide some evidence that component structure can be used to improve performance.

Keywords: SAT, connected components

DOI: 10.3233/SAT190022

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 2, no. 1-4, pp. 201-208, 2006