scholarly journals Analysis of comparative effectiveness of state-of-the-art heuristics for CDCL SAT solvers

2021 ◽  
Author(s):  
S. Kochemazov
Keyword(s):  
Comparative Effectiveness ◽  
Major Part ◽  
State Of The Art ◽  
Learning Algorithms ◽  
Boolean Satisfiability ◽  
Satisfiability Problem ◽  
Sat Solvers ◽  
Boolean Satisfiability Problem ◽  
Clause Learning ◽  
Good For

The Conflict-Driven Clause Learning algorithms for solving the Boolean satisfiability problem comprise the major part of the methods used to solve various instances of the problems that arise in industry and science. In recent years there have been proposed several major heuristics for these algorithms which are assumed to be de facto good for the solvers’ performance over diverse sets of benchmarks. The goal of this paper is to evaluate the contribution of each separate heuristic to the performance of a state-of-the-art solver, see the extent to which they are beneficial, and figure out if the heuristics have any particular features that need to be taken into account.

scholarly journals Problems of search for collisions of cryptographic hash functions of the MD family as variants of Boolean satisfiability problem

2015 ◽  
pp. 61-77
Author(s):  
И.А. Богачкова ◽  
О.С. Заикин ◽  
С.Е. Кочемазов ◽  
И.В. Отпущенников ◽  
А.А. Семенов ◽  
...  
Keyword(s):  
Numerical Experiments ◽  
Hash Functions ◽  
Boolean Satisfiability ◽  
Satisfiability Problem ◽  
Sat Solvers ◽  
Boolean Satisfiability Problem ◽  
Single Block ◽  
Message Digest ◽  
Differential Attacks ◽  
Cryptographic Hash Functions

Рассмотрена реализация разностной атаки на криптографические хеш-функции MD4 (Message Digest 4) и MD5 (Message Digest 5) через сведение задачи поиска коллизий для этих хеш-функций к задаче о булевой выполнимости (SAT, SATisfiability). Новизна полученных результатов заключается в том, что предложены существенно более экономные (в сравнении с известными) SAT-кодировки рассматриваемых алгоритмов, а также в использовании для решения полученных SAT-задач современных многопоточных и параллельных SAT-решателей. Задачи поиска одноблоковых коллизий для MD4 в данной постановке оказались чрезвычайно простыми. Кроме того, найдены несколько десятков двухблоковых коллизий для MD5. В процессе соответствующих вычислительных экспериментов определен некоторый класс сообщений, дающих коллизии: построено множество пар дающих коллизии сообщений, у которых первые 10 байтов нулевые. An implementation of the differential attacks on cryptographic hash functions MD4 (Message Digest 4) and MD5 (Message Digest 5) by reducing the problems of search for collisions of these hash functions to the Boolean satisfiability problem (SAT) is considered. The novelty of the results obtained consists in a more compact (compared to already known) SAT encodings for the algorithms considered and in the use of modern parallel and distributed SAT solvers in applications to the formulated SAT problems. Searching for single block collisions of MD4 in this approach turned out to be very simple. In addition, several dozens of double block collisions of MD5 are found. In the process of the corresponding numerical experiments, a certain class of messages that produce the collisions is found: in particular, a set of pairs of such messages with first 10 zero bytes is constructed.

scholarly journals Seeking Practical CDCL Insights from Theoretical SAT Benchmarks

2018 ◽  
Author(s):  
Jan Elffers ◽  
Jesús Giráldez-Cru ◽  
Stephan Gocht ◽  
Jakob Nordström ◽  
Laurent Simon
Keyword(s):  
Systematic Study ◽  
Boolean Satisfiability ◽  
Proof System ◽  
Sat Solvers ◽  
Proof Search ◽  
Wide Range ◽  
Clause Learning ◽  
Resolution Proof ◽  
Shed Light

Over the last decades Boolean satisfiability (SAT) solvers based on conflict-driven clause learning (CDCL) have developed to the point where they can handle formulas with millions of variables. Yet a deeper understanding of how these solvers can be so successful has remained elusive. In this work we shed light on CDCL performance by using theoretical benchmarks, which have the attractive features of being a) scalable, b) extremal with respect to different proof search parameters, and c) theoretically easy in the sense of having short proofs in the resolution proof system underlying CDCL. This allows for a systematic study of solver heuristics and how efficiently they search for proofs. We report results from extensive experiments on a wide range of benchmarks. Our findings include several examples where theory predicts and explains CDCL behaviour, but also raise a number of intriguing questions for further study.

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 Divide and Conquer: Towards Faster Pseudo-Boolean Solving

2018 ◽  
Author(s):  
Jan Elffers ◽  
Jakob Nordström
Keyword(s):  
Boolean Satisfiability ◽  
Conflict Analysis ◽  
Divide And Conquer ◽  
Theoretical Strength ◽  
Integer Coefficient ◽  
Sat Solvers ◽  
Wide Range ◽  
Clause Learning

The last 20 years have seen dramatic improvements in the performance of algorithms for Boolean satisfiability---so-called SAT solvers---and today conflict-driven clause learning (CDCL) solvers are routinely used in a wide range of application areas. One serious short-coming of CDCL, however, is that the underlying method of reasoning is quite weak. A tantalizing solution is to instead use stronger pseudo-Boolean (PB) reasoning, but so far the promise of exponential gains in performance has failed to materialize---the increased theoretical strength seems hard to harness algorithmically, and in many applications CDCL-based methods are still superior. We propose a modified approach to pseudo-Boolean solving based on division instead of the saturation rule used in [Chai and Kuehlmann '05] and other PB solvers. In addition to resulting in a stronger conflict analysis, this also improves performance by keeping integer coefficient sizes down, and yields a very competitive solver as shown by the results in the Pseudo-Boolean Competitions 2015 and 2016.

Sign in / Sign up

Export Citation Format

Share Document