scholarly journals Decision levels are stable: towards better SAT heuristics

10.29007/cz1f ◽  
2020 ◽  
Author(s):  
Robert Nieuwenhuis ◽  
Adrià Lozano ◽  
Albert Oliveras ◽  
Enric Rodríguez-Carbonell
Keyword(s):  
Information Sharing ◽  
Experimental Setup ◽  
Cardinality Constraints ◽  
Sat Solvers ◽  
Parallel Solvers ◽  
Decision Level ◽  
Sat Solver ◽  
Real Value ◽  
Surprising Fact

We shed new light on the Literal Block Distance (LBD) and glue-based heuristics used in current SAT solvers. For this, we first introduce the concept of stickiness: given a run of a CDCL SAT solver, for each pair of literals we define, by a real value between 0 and 1, how sticky they are, basically, how frequently they are set at the same decision level.By means of a careful and detailed experimental setup and analysis, we confirm the following quite surprising fact: given a SAT instance, when running different CDCL SAT solvers on it, no matter their settings or random seeds, the stickiness relation between literals is always very similar, in a precisely defined sense.We analyze how quickly stickiness stabilizes in a run (quite quickly), and show that it is stable even under different encodings of cardinality constraints. We then describe how and why these solid new insights lead to heuristics refinements for SAT (and extensions, such as SMT) and improved information sharing in parallel solvers.

scholarly journals FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints

2020 ◽  
Vol 34 (02) ◽  
pp. 1552-1560
Author(s):  
Anastasios Kyrillidis ◽  
Anshumali Shrivastava ◽  
Moshe Vardi ◽  
Zhiwei Zhang
Keyword(s):  
Boolean Functions ◽  
Continuous Optimization ◽  
Conjunctive Normal Form ◽  
Cardinality Constraints ◽  
Sat Solvers ◽  
Boolean Satisfiability Problem ◽  
Algebraic Framework ◽  
Clause Learning ◽  
Sat Solver ◽  
Analysis Of Boolean Functions

The Boolean SATisfiability problem (SAT) is of central importance in computer science. Although SAT is known to be NP-complete, progress on the engineering side—especially that of Conflict-Driven Clause Learning (CDCL) and Local Search SAT solvers—has been remarkable. Yet, while SAT solvers, aimed at solving industrial-scale benchmarks in Conjunctive Normal Form (CNF), have become quite mature, SAT solvers that are effective on other types of constraints (e.g., cardinality constraints and XORs) are less well-studied; a general approach to handling non-CNF constraints is still lacking. In addition, previous work indicated that for specific classes of benchmarks, the running time of extant SAT solvers depends heavily on properties of the formula and details of encoding, instead of the scale of the benchmarks, which adds uncertainty to expectations of running time.To address the issues above, we design FourierSAT, an incomplete SAT solver based on Fourier analysis of Boolean functions, a technique to represent Boolean functions by multilinear polynomials. By such a reduction to continuous optimization, we propose an algebraic framework for solving systems consisting of different types of constraints. The idea is to leverage gradient information to guide the search process in the direction of local improvements. Empirical results demonstrate that FourierSAT is more robust than other solvers on certain classes of benchmarks.

scholarly journals Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers

10.29007/6vwg ◽  
2018 ◽  
Author(s):  
Marijn Heule ◽  
Norbert Manthey ◽  
Tobias Philipp
Keyword(s):  
Clock Time ◽  
Parallel Solver ◽  
Sat Solvers ◽  
Parallel Solvers ◽  
Cpu Time ◽  
Sat Solver ◽  
Solver Performance

As satisfiability (SAT) solver performance has improved, so has their complexity, which make it more likely that SAT solvers contain bugs. One important source of increased complexity is clause sharing in parallel SAT solvers. SAT solvers can emit a proof of unsatisfiability to gain confidence that the their results are correct. Such proofs must contain deletion information in order to check them efficiently. Computing deletion information is easy and cheap for parallel solvers without clause sharing, but tricky for parallel solvers with clause sharing.We present a method to generate unsatisfiability proofs from clause sharing parallel SAT solvers. We show that the overhead of our method is small and that the produced proofs can be validated in a time similar to the solving (CPU) time. However, proofs produced by parallel solvers without clause sharing can be checked in a similar to the solving (wall-clock) time. This raises the question whether our method can be improved such that the checking time of proofs from parallel solvers without clause sharing is comparable to the time to check proofs from parallel solver with clause sharing.

scholarly journals 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.

scholarly journals Framework for Generating Configurable SAT Solvers

2011 ◽  
Vol 6 (1) ◽  
pp. 50-59
Author(s):  
Bernardo C. Vieira ◽  
Fabrício V. Andrade ◽  
Antônio O. Fernandes
Keyword(s):  
State Of The Art ◽  
The State ◽  
Equivalence Checking ◽  
Decision Heuristics ◽  
Sat Solvers ◽  
The Third ◽  
Sat Solver ◽  
Run Time

The state-of-the-art SAT solvers usually share the same core techniques, for instance: the watched literals structure, conflict clause recording and non-chronological backtracking. Nevertheless, they might differ in the elimination of learnt clauses, as well as in the decision heuristic. This article presents a framework for generating configurable SAT solvers. The proposed framework is composed of the following components: a Base SAT Solver, a Perl Preprocessor, XML files (Solver Description and Heuristics Description files) to describe each heuristic as well as the set of heuristics that the generated solver uses. This solvers may use several techniques and heuristics such as those implemented in BerkMin, and in Equivalence Checking of Dissimilar Circuits, and also in Minisat. In order to demonstrate the effectiveness of the proposed framework, this article also presents three distinct SAT solver instances generated by the framework to address a complex and challenging industry problem: the Combinational Equivalence Checking problem (CEC).The first instance is a SAT solver that uses BerkMin and Dissimilar Circuits core techniques except the learnt clause elimination heuristic that has been adapted from Minisat; the second is another solver that combines BerkMin and Minisat decision heuristics at run-time; and the third is yet another SAT solver that changes the database reducing heuristic at run-time. The experiments demonstrate that the first SAT solver generated is a faster solver than state-of-the-art SAT solver BerkMin for several instances as well as for Minisat in almost every instance.

scholarly journals Exploring Practicability for Solving a Task Based on the Generalized Cellular Automata via SAT Solvers

2019 ◽  
pp. 11-22
Author(s):  
P. G. Klyucharev
Keyword(s):  
Positive Integer ◽  
Cellular Automata ◽  
Operation Time ◽  
Computational Experiments ◽  
Key Recovery ◽  
Sat Solvers ◽  
Initial Values ◽  
Sat Solver ◽  
Key Length ◽  
Exhaustive Method

The paper deals with exploring practicability to solve a task of the recovery key of generalized cellular automata via SAT solvers.The problem, which we call a task of the key recovery of generalized cellular automata, is under consideration. This task is formulated as follows. The generalized cellular automata, the positive integer s, the initial values of some cells, and the values of some cells after the s steps of the automata are given. It is required to find the initial values of the remaining cells (their number will be called the key length).To solve the task, were tested Picosat, MiniSat, Glucose, Lingeling, and CryptoMiniSat SAT solvers. In further computational experiments, was used the MiniSat, which was the best.The key recovery task was solved for the generalized cellular automata of a small size via the MiniSat SAT solver. Pizer's graphs were used as graphs of the automata. The key length was approximately half the number of the cells in the automata. As a result of the study, it turned out that operation time of a SAT solver quite significantly (several orders of magnitude) exceeds the estimated time of solution using the FPGA exhaustive method, and the empirical dependencies of the SAT-solver operation time on the key length are exponential.The obtained results confirm that SAT solvers disable effective solving a task under consideration. This allows giving the better reasons for the cryptographic security of the crypto-algorithms based on the generalized cellular automata with regard to the cryptanalysis methods using SAT solvers.

scholarly journals 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.

scholarly journals 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.

scholarly journals Community Structure in Industrial SAT Instances

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.

scholarly journals On speeding up factoring with quantum SAT solvers

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.

scholarly journals Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution

2011 ◽  
Vol 40 ◽  
pp. 353-373 ◽  
Author(s):  
A. Atserias ◽  
J. K. Fichte ◽  
M. Thurley
Keyword(s):  
High Probability ◽  
Learning Algorithms ◽  
Sat Solvers ◽  
Unit Clause ◽  
Resolution Rule ◽  
Clause Learning ◽  
Bounded Width ◽  
Unit Resolution ◽  
Surprising Fact ◽  
Do So

We offer a new understanding of some aspects of practical SAT-solvers that are based on DPLL with unit-clause propagation, clause-learning, and restarts. We do so by analyzing a concrete algorithm which we claim is faithful to what practical solvers do. In particular, before making any new decision or restart, the solver repeatedly applies the unit-resolution rule until saturation, and leaves no component to the mercy of non-determinism except for some internal randomness. We prove the perhaps surprising fact that, although the solver is not explicitly designed for it, with high probability it ends up behaving as width-k resolution after no more than O(n^{2k+2}) conflicts and restarts, where n is the number of variables. In other words, width-k resolution can be thought of as O(n^{2k+2}) restarts of the unit-resolution rule with learning.

Sign in / Sign up

Export Citation Format

Share Document