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

Authors: Biere, Armin

Article Type: Research Article

Abstract: In this article we describe and evaluate optimized compact data structures for watching literals. Experiments with our SAT solver PicoSAT show that this low-level optimization not only saves memory, but also turns out to speed up the SAT solver considerably. We also discuss how to store proof traces compactly in memory and further unique features of PicoSAT including an aggressive restart schedule.

Keywords: SAT solver, watched literals, occurrence lists, proof traces, restarts

DOI: 10.3233/SAT190039

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, no. 2-4, pp. 75-97, 2008

Authors: Heule, Marijn | van Maaren, Hans

Article Type: Research Article

Abstract: We show how to exploit the 32/64 bit architecture of modern computers to accelerate some of the algorithms used in satisfiability solving by modifying assignments to variables in parallel on a single processor. Techniques such as random sampling demonstrate that while using bit vectors instead of Boolean values solutions to satisfiable formulae can be obtained faster. Here, we reveal that more complex algorithms, like unit propagation and detection of autarkies, can be parallelized efficiently, as well. We capitalize on the developed parallel algorithms by modifying the state-of-the-art local search Sat solver UnitWalk accordingly. Experiments show that the …parallel version performs much faster than the original implementation. Show more

Keywords: local search, parallel computing, Boolean Algebra

DOI: 10.3233/SAT190040

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, no. 2-4, pp. 99-116, 2008

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

Article Type: Research Article

Abstract: We introduce a new jump strategy for look-ahead based satisfiability (Sat ) solvers that aims to boost their performance on satisfiable formulae, while maintaining their behavior on unsatisfiable instances. Direction heuristics select which Boolean value to assign to a decision variable. They are used in various state-of-the-art Sat solvers and may bias the distribution of solutions in the search-tree. This bias can clearly be observed on hard random k -Sat formulae. While alternative jump / restart strategies are based on exploring a random new part of the search-tree, the proposed one examines a part that is more …likely to contain a solution based on these observations. Experiments with – so-called distribution jumping – in the march_ks Sat solver, show that this new technique boosts the number of satisfiable formulae it can solve. Moreover, it proved essential for winning the satisfiable crafted category during the Sat 2007 competition. Show more

Keywords: direction heuristics, jumping strategy, look-ahead SAT solvers

DOI: 10.3233/SAT190041

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, no. 2-4, pp. 117-148, 2008

Authors: Nghia Pham, Duc | Thornton, John | Gretton, Charles | Sattar, Abdul

Article Type: Research Article

Abstract: In this paper we describe a stochastic local search (SLS) procedure for finding models of satisfiable propositional formulae. This new algorithm, gNovelty+ , draws on the features of two other WalkSAT family algorithms: AdaptNovelty+ and G2 WSAT, while also successfully employing a hybrid clause weighting heuristic based on the features of two dynamic local search (DLS) algorithms: PAWS and (R)SAPS. gNovelty+ was a Gold Medal winner in the random category of the 2007 SAT competition. In this paper we present a detailed description of the algorithm and extend the SAT competition results via an empirical study of …the effects of problem structure, parameter tuning and resolution preprocessors on the performance of gNovelty+ . The study compares gNovelty+ with three of the most representative WalkSAT-based solvers: AdaptG2 WSAT0, G2 WSAT and AdaptNovelty+ , and two of the most representative DLS solvers: RSAPS and PAWS. Our new results augment the SAT competition results and show that gNovelty+ is also highly competitive in the domain of solving structured satisfiability problems in comparison with other SLS techniques. Show more

Keywords: SAT-solver, local search, clause weighting, adaptive heuristic

DOI: 10.3233/SAT190042

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, no. 2-4, pp. 149-172, 2008

Authors: Spence, Ivor

Article Type: Research Article

Abstract: The Ternary Tree Solver (tts ) is a complete solver for propositional satisfiability which was designed to have good performance on the most difficult small instances. It uses a static ternary tree data structure to represent the simplified proposition under all permissible partial assignments and maintains a database of derived propositions known to be unsatisfiable. In the SAT2007 competition version 4.0 won the silver medal for the category handmade , speciality UNSAT solvers and was the top qualifier for the second stage for handmade benchmarks, solving 11 benchmarks which were not solved by any other entrant. We describe the …methods used by the solver and analyse the competition Phase 1 results on small benchmarks. We propose a first version of a comprehensive suite of small difficult satisfiability benchmarks (sdsb ) and compare the worst-case performance of the competition medallists on these benchmarks. Show more

Keywords: SAT-solver, difficult instance, variable ordering, simulated annealing, clause memoisation

DOI: 10.3233/SAT190043

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, no. 2-4, pp. 173-190, 2008

Authors: Pipatsrisawat, Knot | Palyan, Akop | Chavira, Mark | Choi, Arthur | Darwiche, Adnan

Article Type: Research Article

Abstract: We analyze, in this work, the performance of a recently introduced weighted Max-SAT solver, Clone, in the Max-SAT evaluation 2007. Clone utilizes a novel bound computation based on formula compilation that allows it to search in a reduced search space. We study how additional techniques from the SAT and Max-SAT literature affect the performance of Clone on problems from the evaluation. We then perform further investigations on factors that may affect the performance of leading Max-SAT solvers. We empirically identify two properties of weighted Max-SAT problems that can be used to adjust the difficulty level of the problems with respect …to the considered solvers. Show more

Keywords: Max-SAT, constraint relaxation, lower bound computation

DOI: 10.3233/SAT190044

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, no. 2-4, pp. 191-217, 2008

Authors: Wei, Wanxia | Li, Chu Min | Zhang, Harry

Article Type: Research Article

Abstract: We propose a new switching criterion, namely the evenness or unevenness of the distribution of variable weights, and use this criterion to combine intensification and diversification in local search for SAT. We refer to the ways in which state-of-the-art local search algorithms adaptG 2 WSAT P and VW select a variable to flip, as heuristic adaptG 2 WSAT P and heuristic VW , respectively. To evaluate the effectiveness of this criterion, we apply it to heuristic adaptG 2 WSAT P and heuristic VW , in which the former intensifies the search better than …the latter, and the latter diversifies the search better than the former. The resulting local search algorithm, which switches between heuristic adaptG 2 WSAT P and heuristic VW in every step according to this criterion, is called Hybrid . Our experimental results show that, on a broad range of SAT instances presented in this paper, Hybrid inherits the strengths of adaptG 2 WSAT P and VW , and exhibits generally better performance than adaptG 2 WSAT P and VW . In addition, Hybrid compares favorably with state-of-the-art local search algorithm R +adaptNovelty + on these instances. Furthermore, without any manual tuning parameters, Hybrid solves each of these instances in a reasonable time, while adaptG 2 WSAT P , VW , and R +adaptNovelty + have difficulty on some of these instances. Show more

Keywords: SAT, local search, switching criterion, intensification, diversification, distribution of variable weights

DOI: 10.3233/SAT190045

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, no. 2-4, pp. 219-237, 2008

Authors: Heras, Federico | Larrosa, Javier | de Givry, Simon | Schiex, Thomas

Article Type: Research Article

Abstract: In this technical report we briefly describe the instances submitted to the 2006 and 2007 Max-SAT Evaluations. First, we introduce the instances that can be directly encoded as Max-SAT. Then, we describe the methods used to translate problem instances coming from other optimization frameworks to Max-SAT. Finally, we present a quick reference table containing short descriptions of each set of problem instances.

Keywords: Max-SAT problem instances

DOI: 10.3233/SAT190046

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, no. 2-4, pp. 239-250, 2008

Authors: Argelich, Josep | Li, Chu-Min | Manyà, Felip | Planes, Jordi

Article Type: Research Article

Abstract: We describe the organization and report on the results of the First and Second Max-SAT Evaluations, which were organized as affiliated events of the 2006 and 2007 editions of the International Conference on Theory and Applications of Satisfiability Testing (SAT-2006 and SAT-2007), discuss the insights gained and point out new directions for forthcoming evaluations. The main objectives of both evaluations were assessing the advancements in the field of Max-SAT solvers through a comparison of their performances, identifying successful solving techniques and encouraging researchers to develop new ones, and creating a publicly available collection of challenging Max-SAT benchmarks.

Keywords: Max-SAT, Weighted Max-SAT, Partial Max-SAT, Weighted Partial Max-SAT, empirical evaluation, solvers, benchmarks

DOI: 10.3233/SAT190047

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, no. 2-4, pp. 251-278, 2008

Authors: Speckenmeyer, Ewald | Tacchella, Armando | Manquinho, Vasco | Li, Chu Min

Article Type: Editorial

DOI: 10.3233/SAT190048

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, no. 2-4, pp. 279-280, 2008