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

Authors: Le Berre, Daniel | Parrain, Anne

Article Type: Research Article

Abstract: Sat4j is a mature, open source library of SAT-based solvers in Java. It provides a modular SAT solver architecture designed to work with generic constraints. Such architecture is used to provide SAT, MaxSat and pseudo-boolean and solvers for lightweight constraint programming. Those solvers have been evaluated regularly in the corresponding international competitive events. The library has been adopted by several academic softwares and the widely used Eclipse platform, which relies on a pseudo-boolean solver from Sat4j for its plugins dependencies management since June 2008.

Keywords: resolution, cutting-planes, SAT-solver, MAXSAT

DOI: 10.3233/SAT190075

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 7, no. 2-3, pp. 59-64, 2010

Authors: Pulina, Luca | Tacchella, Armando

Article Type: Research Article

Abstract: In this paper we describe aqme ’10, the version of the Adaptive QBF Multi-Engine submitted to QBFEVAL’10.

Keywords: self-adaptive multi-engine solver, quantiÂŞed Boolean formulas, AQME

DOI: 10.3233/SAT190076

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 7, no. 2-3, pp. 65-70, 2010

Authors: Lonsing, Florian | Biere, Armin

Article Type: Research Article

Abstract: We present DepQBF 0.1, a new search-based solver for quantified boolean formulae (QBF). It integrates compact dependency graphs to overcome the restrictions imposed by linear quantifier prefixes of QBFs in prenex conjunctive normal form (PCNF). DepQBF 0.1 was placed first in the main track of QBFEVAL’10 in a score-based ranking. We provide a general system overview and describe selected orthogonal features such as restarts and removal of learnt constraints.

Keywords: QBF solving, DPLL, dependency schemes, restarts

DOI: 10.3233/SAT190077

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 7, no. 2-3, pp. 71-76, 2010

Authors: Balint, Adrian | Gall, Daniel | Kapler, Gregor | Retz, Robert

Article Type: Research Article

Abstract: The design of a SAT-solver or the modification of an existing one is always followed by a phase of intensive testing of the solver on a benchmark of instances. This task can be very time consuming even when using multi-core computers or computer clusters. To speed up this process we designed EDACC. A system capable of managing solvers with their parameters, instances, creating experiment jobs and running them on arbitrary multi-core systems. After loading solvers and instances into the system the user is able to configure the parameters of the solvers and choose the instances for the experiment and the …settings of the runs. Then EDACC generates the jobs for the experiment and stores them in a database. The user only has to start the EDACC-clients on the target computing system. Each client will load jobs from the database and try to use the full computing capacity of the system to accomplish its tasks. The client will also monitor the resources of the solvers such as time and memory. When a job is finished the client will write the results back to the database and choose another job until all jobs are finished. The clients can be distributed on a grid to increase the throughput. System crashes will not affect the results because the results are saved to a remote database. The user only has to restart the client. With the help of this system, testing and comparing solvers can be done much faster and much more efficiently. Show more

Keywords: SAT-solver testing, design of tests, computer clusters, jobs scheduling

DOI: 10.3233/SAT190078

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 7, no. 2-3, pp. 77-82, 2010

Authors: Giunchiglia, Enrico | Marin, Paolo | Narizzano, Massimo

Article Type: Research Article

Abstract: In this paper we outline QuBE7’s main features, describing first the options of the preprocessors, and then giving some details about how the core search-based solver (i) performs unit and pure literal propagation; and (ii) performs the “Conflict Analysis procedure” for non-chronological backtracking, generalised from the SAT to the QBF case. We conclude with the experimental evaluation, showing that QuBE7.0 is the a state-of-the-art single-engine QBF solver.

Keywords: QBF, solver, preprocessor

DOI: 10.3233/SAT190079

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 7, no. 2-3, pp. 83-88, 2010

Authors: Heras, Federico | Bañeres, David

Article Type: Research Article

Abstract: In this paper we analyze three well-known preprocessors for Max-SAT. The first preprocessor is based on the so-called variable saturation . The second preprocessor is based on the resolution mechanism incorporated in modern branch and bound solvers. The third preprocessor is specific for the Maximum Clique problem and other problems with similar encoding in WCNF such as minimum vertex covering and combinatorial auctions . Our experimental investigation is divided in two parts. In the first part, we study the effect of the preprocessors on several problem instances using different metrics. In the second part, the effect of each …preprocessor is analyzed in some of the most relevant Max-SAT local search algorithms of the literature including Gsat , Walksat , Adaptnovelty +, Irots and Saps . Results indicate that some of these algorithms find much better solutions after the preprocessor. Furthermore, some preprocessed instances can be solved to optimality with local search under very specific conditions. Show more

Keywords: max-SAT, stochastic local search, inference

DOI: 10.3233/SAT190080

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 7, no. 2-3, pp. 89-126, 2010