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

Authors: Hamadi, Youssef | Jabbour, Said | Piette, Cedric | Sais, Lakhdar

Article Type: Research Article

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.

Keywords: SAT solving, parallelism

DOI: 10.3233/SAT190081

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 7, no. 4, pp. 127-132, 2011

Authors: van der Tak, Peter | Ramos, Antonio | Heule, Marijn

Article Type: Research Article

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

Keywords: CDCL solver, restart strategy

DOI: 10.3233/SAT190082

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 7, no. 4, pp. 133-138, 2011

Authors: Roussel, Olivier

Article Type: Research Article

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.

Keywords: solver control, resources limitation, competitions

DOI: 10.3233/SAT190083

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 7, no. 4, pp. 139-144, 2011

Authors: Haynal, Steve | Haynal, Heidi

Article Type: Research Article

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

Keywords: fast Fourier transform, FFT, SMT-solver, Boolean modeling

DOI: 10.3233/SAT190084

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 7, no. 4, pp. 145-187, 2011

Authors: Björk, Magnus

Article Type: Research Article

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

Keywords: SAT Encodings, SAT-Solvers, Applied SAT

DOI: 10.3233/SAT190085

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 7, no. 4, pp. 189-201, 2011