Modern Cooperative Parallel SAT Solving

Nowadays, powerful parallel SAT solvers are based on an algorithm portfolio. Thealternative approach, (iterative) search space partitioning, cannot keep up, although, ac-cording to the literature, iterative partitioning systems should scale better than portfoliosolvers. In this paper we identify key problems in current parallel cooperative SAT solvingapproaches, most importantly communication, how to partition the search space, and howto utilize the sequential search engine. First, we improve on each problem separately. Ina further step, we show that combining all the improvements leads to a state-of-the-artparallel SAT solver, which does not use the portfolio approach, but instead relies on it-erative partitioning. The experimental evaluation of this system completely changes thepicture about the performance of search space partitioning SAT solvers: on instances ofa combined benchmark of recent SAT competitions, the presented approach can keep upwith the winners of last years SAT competition. The combined improvements improve theexisting cooperative solver splitter by 24%: instead of 561 out of 880 instances, the newsolver Pcasso can solve 696 instances.

Download Full-text

Dolius: A Distributed Parallel SAT Solving Framework

10.29007/hvqt ◽

2018 ◽

Author(s):

Gilles Audemard ◽

Benoît Hoessen ◽

Saïd Jabbour ◽

Cédric Piette

Keyword(s):

Shared Memory ◽

State Of The Art ◽

Divide And Conquer ◽

Sat Solving ◽

Sat Solvers ◽

Sat Solver

Over the years, parallel SAT solving becomes more and more important. However, most of state-of-the-art parallel SAT solvers are portfolio-based ones. They aim at running several times the same solver with different parameters. In this paper, we propose a tool called Dolius, mainly based on the divide and conquer paradigm. In contrast to most current parallel efficient engines, Dolius does not need shared memory, can be distributed, and scales well when a large number of computing units is available. Furthermore, our tool contains an API allowing to plug any SAT solver in a simple way.

Download Full-text

Tuning Parallel SAT Solvers

10.29007/z3g2 ◽

2019 ◽

Author(s):

Thorsten Ehlers ◽

Dirk Nowotka

Keyword(s):

Model Checking ◽

Database Management ◽

Bounded Model Checking ◽

Experimental Results ◽

Massively Parallel ◽

Sat Solving ◽

Sat Solvers ◽

Sat Solver ◽

The Impact

In this paper we present new implementation details and benchmarking results for our parallel portfolio solver TopoSAT2. In particular, we discuss ideas and implementation details for the exchange of learned clauses in a massively-parallel SAT solver which is designed to run more that 1, 000 solver threads in parallel. Furthermore, we go back to the roots of portfolio SAT solving, and discuss the impact of diversifying the solver by using different restart- , branching- and clause database management heuristics. We show that these techniques can be used to tune the solver towards different problems. However, in a case study on formulas derived from Bounded Model Checking problems we see the best performance when using a rather simple clause exchange strategy. We show details of these tests and discuss possible explanations for this phenomenon.As computing times on massively-parallel clusters are expensive, we consider it especially interesting to share these kind of experimental results.

Download Full-text

Community Structure in Industrial SAT Instances

Journal of Artificial Intelligence Research ◽

10.1613/jair.1.11741 ◽

2019 ◽

Vol 66 ◽

pp. 443-472

Author(s):

Carlos Ansótegui ◽

Maria Luisa Bonet ◽

Jesús Giráldez-Cru ◽

Jordi Levy ◽

Laurent Simon

Keyword(s):

Community Structure ◽

Complex Networks ◽

Graph Model ◽

Underlying Structure ◽

Original Structure ◽

Sat Solving ◽

Random Graph Model ◽

Sat Solvers ◽

Sat Solver ◽

Remarkable Progress

Modern SAT solvers have experienced a remarkable progress on solving industrial instances. It is believed that most of these successful techniques exploit the underlying structure of industrial instances. Recently, there have been some attempts to analyze the structure of industrial SAT instances in terms of complex networks, with the aim of explaining the success of SAT solving techniques, and possibly improving them. In this paper, we study the community structure, or modularity, of industrial SAT instances. In a graph with clear community structure, or high modularity, we can find a partition of its nodes into communities such that most edges connect variables of the same community. Representing SAT instances as graphs, we show that most application benchmarks are characterized by a high modularity. On the contrary, random SAT instances are closer to the classical Erdös-Rényi random graph model, where no structure can be observed. We also analyze how this structure evolves by the effects of the execution of a CDCL SAT solver, and observe that new clauses learned by the solver during the search contribute to destroy the original structure of the formula. Motivated by this observation, we finally present an application that exploits the community structure to detect relevant learned clauses, and we show that detecting these clauses results in an improvement on the performance of the SAT solver. Empirically, we observe that this improves the performance of several SAT solvers on industrial SAT formulas, especially on satisfiable instances.

Download Full-text

Towards Improving the Resource Usage of SAT-solvers

10.29007/3vwv ◽

2018 ◽

Author(s):

Norbert Manthey ◽

Ari Saptawijaya

Keyword(s):

Data Structures ◽

Memory Access ◽

Resource Usage ◽

Sat Solving ◽

Sat Solvers ◽

L2 Cache ◽

Measurement Results ◽

Sat Solver ◽

Cache Analysis ◽

Runtime Performance

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.

Download Full-text

On speeding up factoring with quantum SAT solvers

Scientific Reports ◽

10.1038/s41598-020-71654-y ◽

2020 ◽

Vol 10 (1) ◽

Author(s):

Michele Mosca ◽

Joao Marcos Vensi Basso ◽

Sebastian R. Verschoor

Keyword(s):

Number Field ◽

Classical Method ◽

Sat Solving ◽

Smooth Numbers ◽

Sat Solvers ◽

Number Field Sieve ◽

Main Challenge ◽

Np Hard Problem ◽

Sat Solver ◽

Insight Into

Abstract There have been several efforts to apply quantum SAT solving methods to factor large integers. While these methods may provide insight into quantum SAT solving, to date they have not led to a convincing path to integer factorization that is competitive with the best known classical method, the Number Field Sieve. Many of the techniques tried involved directly encoding multiplication to SAT or an equivalent NP-hard problem and looking for satisfying assignments of the variables representing the prime factors. The main challenge in these cases is that, to compete with the Number Field Sieve, the quantum SAT solver would need to be superpolynomially faster than classical SAT solvers. In this paper the use of SAT solvers is restricted to a smaller task related to factoring: finding smooth numbers, which is an essential step of the Number Field Sieve. We present a SAT circuit that can be given to quantum SAT solvers such as annealers in order to perform this step of factoring. If quantum SAT solvers achieve any asymptotic speedup over classical brute-force search for smooth numbers, then our factoring algorithm is faster than the classical NFS.

Download Full-text

Duplicates of conflict clauses in CDCL derivation and their usage to invert some cryptographic functions

Numerical Methods and Programming (Vychislitel'nye Metody i Programmirovanie) ◽

10.26089/nummet.v20r106 ◽

2019 ◽

pp. 54-66

Author(s):

В.С. Кондратьев ◽

А.А. Семенов ◽

О.С. Заикин

Keyword(s):

Hash Functions ◽

Boolean Satisfiability ◽

Experimental Results ◽

Sat Solving ◽

New Approach ◽

Sat Solvers ◽

Satisfiability Problems ◽

Clause Learning ◽

Sat Solver ◽

Cryptographic Hash Functions

Изучен феномен повторного порождения конфликтных ограничений SAT-решателями в процессе работы с трудными экземплярами задачи о булевой выполнимости. Данный феномен является следствием применения эвристических механизмов чистки конфликтных баз, которые реализованы во всех современных SAT-решателях, основанных на алгоритме CDCL (Conflict Driven Clause Learning). Описана новая техника, которая позволяет отслеживать повторно порождаемые дизъюнкты и запрещать их последующее удаление. На базе предложенных технических решений построен новый многопоточный SAT-решатель (SAT, SATisfiability), который на ряде SAT-задач, кодирующих обращение криптографических хеш-функций, существенно превзошел по эффективности многопоточные решатели, занимавшие в последние годы высокие места на специализированных соревнованиях. A phenomenon of conflict clauses generated repeatedly by SAT solvers is studied. Such clauses may appear during solving hard Boolean satisfiability problems (SAT). This phenomenon is caused by the fact that the modern SAT solvers are based on the CDCL algorithm that generates conflict clauses. A database of such clauses is periodically and partially cleaned. A new approach for practical SAT solving is proposed. According to this approach, the repeatedly generated conflict clauses are tracked, whereas their further generation is prohibited. Based on this approach, a multithreaded SAT solver was developed. This solver was compared with the best multithreaded SAT solvers awarded during the last SAT competitions. According to the experimental results, the developed solver greatly outperforms its competitors on several SAT instances encoding the inversion of some cryptographic hash functions.

Download Full-text

Light-Weight Integration of SAT Solving into First-Order Reasoners – First Experiments

10.29007/89kc ◽

2018 ◽

Cited By ~ 1

Author(s):

Stephan Schulz

Keyword(s):

Search Space ◽

Light Weight ◽

Sat Solving ◽

First Order ◽

Proof Search ◽

Sat Solver

We describe a light-weight integration of the propositional SAT solver PicoSAT and the saturation-based superposition prover E. The proof search is driven by the saturation prover. Periodically, the saturation is interrupted, and all first-order clauses are grounded. The resulting ground problem is converted to a propositional format and handed to the SAT solver. If the SAT solver reports unsatisfiability, the proof is extracted and reported on the first-order level. First experiments demonstrate the viability of the approach and suggest future extensions. They also yield interesting information about the structure of the search space.

Download Full-text

A Theory of Satisfiability-Preserving Proofs in SAT Solving

10.29007/tc7q ◽

2018 ◽

Author(s):

Adrián Rebola-Pardo ◽

Martin Suda

Keyword(s):

Propositional Logic ◽

Logical Truth ◽

Point Of View ◽

Traditional View ◽

Satisfiability Problem ◽

Sat Solving ◽

Sat Solvers ◽

Proof Systems ◽

Meta Level

We study the semantics of propositional interference-based proof systems such as DRAT and DPR. These are characterized by modifying a CNF formula in ways that preserve satisfiability but not necessarily logical truth. We propose an extension of propositional logic called overwrite logic with a new construct which captures the meta-level reasoning behind interferences. We analyze this new logic from the point of view of expressivity and complexity, showing that while greater expressivity is achieved, the satisfiability problem for overwrite logic is essentially as hard as SAT, and can be reduced in a way that is well-behaved for modern SAT solvers. We also show that DRAT and DPR proofs can be seen as overwrite logic proofs which preserve logical truth. This much stronger invariant than the mere satisfiability preservation maintained by the traditional view gives us better understanding on these practically important proof systems. Finally, we showcase this better understanding by finding intrinsic limitations in interference-based proof systems.

Download Full-text