Journal on Satisfiability, Boolean Modeling and Computation - Volume 2, issue 1-4
The scope of JSAT is propositional reasoning, modeling, and computation. The Satisfiability discipline is a central focus of JSAT. We welcome all sorts of contributions to this theme but also encourage authors to submit papers on related topics as Computational Logic, Constraint Programming, Satisfiability Modulo Theories, Quantified Boolean Logic, Pseudo Boolean Methods, zero-one Programming, Integer Programming and Operations Research, whenever the link to Satisfiability is apparent.
Especially JSAT welcomes substantial extensions of conference papers, where the actual conference contribution must be cited. As such, authors are able to provide more detailed information about their work (theoretical details, proofs or theorems, algorithmic or implementation details, more exhaustive empirical evaluations) which were enforced to be omitted in the conference proceedings simply because of strict page limitations.
JSAT also welcomes detailed descriptions of new promising but challenging applications around SAT, to make the SAT community aware of those new applications, and to provide it the opportunity to tackle those challenges.
Occasionally JSAT also publishes Research Notes. Research Notes are also thoroughly reviewed but are not considered full Journal publications and hence will be designated and must be referenced to as such. Also, JSAT publishes papers on System Descriptions, being contributions with a focus on the internals of a Solver.
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.
Keywords: pseudo-Boolean, SAT-solver, SAT translation, integer linear programming
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.
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.
Keywords: adaptive heuristics, look-ahead, SAT solving, SAT competition
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.
Keywords: random satisfiability problems, phase transition, threshold behaviour, critical exponent, SAT competition
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.
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.
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.
Keywords: satisfiability, SAT solver, pseudo-Boolean, inference-based learning
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.
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.