POS-10: Papers with Abstracts

Abstract. 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.

Abstract. 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

Abstract. 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.

Abstract. 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.

Abstract. 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.