A Logical Deduction Based Clause Learning Algorithm for Boolean Satisfiability Problems

Изучен феномен повторного порождения конфликтных ограничений 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

Using Grover's search quantum algorithm to solve Boolean satisfiability problems, part 2

XRDS Crossroads The ACM Magazine for Students ◽

10.1145/3368085 ◽

2019 ◽

Vol 26 (2) ◽

pp. 68-71

Author(s):

Diogo Fernandes ◽

Carla Silva ◽

Inês Dutra

Keyword(s):

Quantum Algorithm ◽

Boolean Satisfiability ◽

Satisfiability Problems

Download Full-text

Seeking Practical CDCL Insights from Theoretical SAT Benchmarks

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence ◽

10.24963/ijcai.2018/181 ◽

2018 ◽

Cited By ~ 5

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.

Download Full-text

Detecting data store access conflict in Simulink by solving Boolean satisfiability problems

Proceedings of the 2010 American Control Conference ◽

10.1109/acc.2010.5531137 ◽

2010 ◽

Author(s):

Zhi Han ◽

Pieter J Mosterman

Keyword(s):

Boolean Satisfiability ◽

Satisfiability Problems ◽

Data Store

Download Full-text

Divide and Conquer: Towards Faster Pseudo-Boolean Solving

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence ◽

10.24963/ijcai.2018/180 ◽

2018 ◽

Cited By ~ 10

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.

Download Full-text