POS on Saturday, July 10th

09:00‑10:00 Tutorial
Location: IF G.03
09:00 Youssef Hamadi (Microsoft Research)
From Parallel SAT to Distributed SAT

This tutorial will present an overview of parallelism in SAT. It will start with a presentation of classical divide and conquer techniques, discuss their ancient origin and compare them to more recent portfolio-based algorithms. It will then present the impact of clause-sharing on their performances and discuss various strategies used to control the communication overhead. A particular technique used to control the classical diversification/intensification tradeoff will also be presented. Finally, perspectives will be given which will relate the current parallel SAT technologies to the expected evolution of computational platforms, leading to distributed SAT solving scenarios.

10:30‑12:30 MAXSAT / Generalized-SAT session
Chair: Luca Pulina
Location: IF G.03
10:30 Adrian Kuegel
Improved Exact Solver for the Weighted MAX-SAT Problem

Many exact Max-SAT solvers use a branch and bound algorithm, where the lower bound is calculated with a combination of Max-SAT resolution and detection of disjoint inconsistent subformulas. We propose a propagation algorithm which improves the detection of disjoint inconsistent subformulas compared to algorithms previously used in Max-SAT solvers. We implemented this algorithm in our new solver akmaxsat and compared our solver with three solvers using unit propagation and restricted failed literal detection; these solvers are currently state-of-the-art on random Max-SAT instances. We also developed a lazy deletion data structure for our solver which speeds up lower bound calculation on instances with a high clauses-to-variables ratio. Our experiments show that our solver runs faster than the previously best solvers on randomly generated instances with a high clauses-to-variables ratio.

11:00 Carlos Ansótegui, María Luisa Bonet and Jordi Levy
On Solving MaxSAT Through SAT

In this paper we present a Partial MaxSAT solver based on successive calls to a SAT solver. At the kth iteration the SAT solver tries to certify that there exist an assignment that satisfies all but k clauses. The key idea is to add an additional variable to each soft clause and to introduce, at each iteration, at-least and at-most cardinality constraints restricting the possible values of these variables. We prove the correctness of our algorithm and compare it with other (Partial) MaxSAT solvers.

11:30 Daniel Le Berre and Anne Parrain
The SAT4J library 2.2, System Description

SAT4J is an open source library of SAT solvers written in Java which aims at allowing Java programmers to access SAT technology directly in Java. The SAT4J library started in 2004 as an implementation in Java of the Minisat specification [7] and has been developed since then with the spirit to allow testing various combination of features developed in new SAT solvers while keeping the technology easily accessible to a new comer and using both Java and Open Source development standards. The project is supported by the OW2 consortium infrastructure. SAT4J allows to solve a range of decision and optimization problems using pseudo boolean solving as a universal engine for which the problems are trans- lated. See Figure 1 for an overview of the features available in the library. SAT4J has been adopted by various Java based software, in the area of software engineering[2], but also in bioinformatics[6,11] or formal verification1 [12]. The inclusion of SAT4J into the widely used Eclipse open platform[10] makes it one of the most widely used SAT solver around the world (more than 13M downloads of Eclipse 3.4 between June 2008 and June 2009 and since then more than 10M downloads of Eclipse 3.5 as of March 2010 2).

12:00 Mate Soos
Enhanced Gaussian Elimination in DPLL-based SAT Solvers

When cryptographical problems are treated in SAT solvers, they often contain large set of XOR constraints. Treating these XOR constraints through on-the-fly Gaussian elimination during solving has been shown to be a viable approach by Soos et al. [1]. We describe various enhancements to this scheme which increase the performance and mostly eliminate the need for manual tuning of parameters. With these enhancements, we were able achieve speedups of up to 29% on the Bivium and up to 45% on the Trivium ciphers, contrary to the 1-5% speedup achieved by the original scheme.

[1] Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In Kullmann, O., ed.: Theory and Applications of Satisfiability Testing — SAT 2009. Volume 5584 of Lecture Notes in Computer Science., Springer (2009) 244–257

14:00‑15:00 Tooling and monitoring session
Chair: Armin Biere
Location: IF G.03
14:00 Norbert Manthey and Ari Saptawijaya
Towards Improving the Resource Usage of SAT-solvers

The paper presents our work on cache analysis of SAT-solving. The aim is to study how resources are utilized by a SAT-solver and to use this knowledge to improve the resource usage in SAT-solving. The analysis is performed mainly on our CDCL-based SAT-solver and additionally on MiniSAT and PrecoSAT. The measurement is conducted using sample-based profiling on some industrial benchmark from the SAT-competition 2009. During the measurement the following hardware events are traced: total cycles, stall cycles, L2 cache hits and L2 cache misses. From the measurement results, our runtime and implementation analysis unveil that several improvements on resource usage can be done, i.e. on data structures and memory access. These improvements bring about 60% speedup of runtime performance for our solver.

14:30 Adrian Balint, Daniel Gall, Gregor Kapler and Robert Retz
Experiment design and administration for computer clusters for SAT-solvers (EDACC)

The design of a SAT-solver or the modification of an existent one is always followed by a phase of intensified 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 arbitrarily 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 saves them in the 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 control the resources of the solvers such as time and memory. When a job is finished the client will write the results back in the database and choose another job until all jobs are finished. The clients can be only distributed on a grid to increase throughput. System crashes will not affect the results because the results are saved in a remote database, the user has to restart the client. With the help of this system benchmarking solvers can be done much faster and much more efficiently.

15:30‑17:00 QBF session
Chair: Daniel Le Berre
Location: IF G.03
15:30 Florian Lonsing and Armin Biere
DepQBF: A Dependency-Aware QBF Solver

We present DepQBF, a novel 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 version 0.1 was placed first in the main track of QBFEVAL'10 in a score-based ranking. Apart from a general system overview, we describe selected orthogonal features such as restarts and removal of learnt constraints which might be of independent interest.

16:00 Luca Pulina and Armando Tacchella
AQME'10 System Description

In this paper we describe AQME'10, the version of the Adaptive QBF Multi-Engine submitted to QBFEVAL'10.

16:30 Enrico Giunchiglia, Massimo Narizzano and Paolo Marin
QuBE7.0, System Description

In this paper we outline QuBE7's main features, describing first the options of the preprocessors, and then giving some detailes 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, generalized from the SAT to the QBF case. We conclude with the experimental evaluation, showing that QuBE7 is the a state-of-the-art single-engine QBF solver.