Journal on Satisfiability, Boolean Modeling and Computation - Volume 7, issue 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: Current parallel SAT solvers suffer from a non-deterministic behavior. This is the consequence of their architectures which rely on weak synchronizing in an attempt to maximize performance. This behavior is a clear downside for practitioners, who are used to both runtime and solution reproducibility. In this paper, we propose the first Deterministic Parallel DPLL engine. Our experimental results clearly show that our approach preserves the performance of the parallel portfolio approach while ensuring full reproducibility of the results.
Abstract: We present the solver RestartSAT which includes a novel technique to reduce the cost to perform a restart in CDCL SAT solvers. This technique, called ReusedTrail , exploits the observation that CDCL solvers often reassign the same variables to the same truth values after a restart. It computes a partial restart level for which it is guaranteed that all variables below this level will be reassigned after a full restart. RestartSAT , an extended version of MiniSAT , incorporates ReusedTrail which can be implemented easily in almost any CDCL solver. On average, it saves over a third of…the decisions and propagations necessary to solve a problem using a Luby restart policy with unit run 1. Experimental results show that RestartSAT solves over a dozen more application instances than the default MiniSAT .
Abstract: The runsolver tool was designed for the 2005 edition of the pseudo-Boolean competition in order to solve the problem of correctly measuring the resources used by solvers, especially solvers with multiple processes. Since then, it has been improved in several directions and adopted by several other competitions or frameworks. This paper presents the inner working of this tool and the technical problems that it addresses.
Abstract: A fundamental question of longstanding theoretical interest is to prove the lowest exact count of real additions and multiplications required to compute a power-of-two discrete Fourier transform (DFT). For 35 years the split-radix algorithm held the record by requiring just 4 n log 2 n − 6 n + 8 arithmetic operations on real numbers for a size-n DFT, and was widely believed to be the best possible. Recent work by Van Buskirk and Lundy demonstrated improvements to the split-radix operation count by using multiplier coefficients or “twiddle factors” that are not n…th roots of unity for a size-n DFT. This paper presents a Boolean Satisfiability-based proof of the lowest operation count for certain classes of DFT algorithms. First, we present a novel way to choose new yet valid twiddle factors for the nodes in flowgraphs generated by common power-of-two fast Fourier transform algorithms, FFTs. With this new technique, we can generate a large family of FFTs realizable by a fixed flowgraph. This solution space of FFTs is cast as a Boolean Satisfiability problem, and a modern Satisfiability Modulo Theory solver is applied to search for FFTs requiring the fewest arithmetic operations. Surprisingly, we find that there are FFTs requiring fewer operations than the split-radix even when all twiddle factors are n th roots of unity.
Keywords: fast Fourier transform, FFT, SMT-solver, Boolean modeling
Abstract: This article identifies good practices for SAT encodings by analysing interviews with a number of well known SAT experts. The purpose is both to determine the confidence in different encoding strategies, by analysing whether there is consensus among the experts or not, as well as bringing out hidden knowledge to SAT users. There is consensus that encoding techniques usually have a dramatic impact on the efficiency of the SAT solver, that it often takes much work to find a good encoding, and that the size of an encoding is only very loosely related to the hardness of finding a…solution. Topics where the interviewees disagree include the feasibility of including arithmetics in SAT problems and whether to formulate problems as clauses or circuits. The article describes a number of strategies that are good in different situations, such as different ways to represent numbers and how to use incrementality.