scholarly journals Guiding CDCL SAT Search via Random Exploration amid Conflict Depression

2020 ◽  
Vol 34 (02) ◽  
pp. 1428-1435
Author(s):  
Md Solimul Chowdhury ◽  
Martin Müller ◽  
Jia You
Keyword(s):  
Variable Selection ◽  
State Of The Art ◽  
Fast Rate ◽  
Empirical Evaluation ◽  
Sat Solving ◽  
Sat Solvers ◽  
Exploration Strategy ◽  
Clause Learning ◽  
Strong Performance ◽  
Performance Gains

The efficiency of Conflict Driven Clause Learning (CDCL) SAT solving depends crucially on finding conflicts at a fast rate. State-of-the-art CDCL branching heuristics such as VSIDS, CHB and LRB conform to this goal. We take a closer look at the way in which conflicts are generated over the course of a CDCL SAT search. Our study of the VSIDS branching heuristic shows that conflicts are typically generated in short bursts, followed by what we call a conflict depression phase in which the search fails to generate any conflicts in a span of decisions. The lack of conflict indicates that the variables that are currently ranked highest by the branching heuristic fail to generate conflicts. Based on this analysis, we propose an exploration strategy, called expSAT, which randomly samples variable selection sequences in order to learn an updated heuristic from the generated conflicts. The goal is to escape from conflict depressions expeditiously. The branching heuristic deployed in expSAT combines these updates with the standard VSIDS activity scores. An extensive empirical evaluation with four state-of-the-art CDCL SAT solvers demonstrates good-to-strong performance gains with the expSAT approach.

scholarly journals Evaluating CDCL Restart Schemes

10.29007/89dw ◽  
2019 ◽  
Author(s):  
Armin Biere ◽  
Andreas Fröhlich
Keyword(s):  
Specific Problem ◽  
State Of The Art ◽  
Empirical Evaluation ◽  
Sat Solving ◽  
Practical Applications ◽  
Problem Class ◽  
New Variant ◽  
Clause Learning ◽  
Restart Strategy ◽  
The Given

Modern CDCL (conflict-driven clause learning) SAT solvers are used for many practical applications. One of the key ingredients of state-of-the-art CDCL solvers are efficient restart schemes. The main contribution of this work is an extensive empirical evaluation of various restart strategies. We show that optimal static restart intervals are not only correlated with the satisfiability status of a certain instance, but also with the more specific problem class of the given benchmark. We further compare uniform restart intervals with the performance of non-uniform restart schemes, such as Luby restarts. Finally, we revisit the dynamic restart strategy used in Glucose and propose a new variant thereof, which is based on the concept of exponential moving averages. The resulting implementation in Lingeling improves state-of-the-art performance in SAT solving.

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.

Chapter 3. Complete Algorithms

2021 ◽  
Author(s):  
Adnan Darwiche ◽  
Knot Pipatsrisawat
Keyword(s):  
Real World ◽  
Theoretical Perspective ◽  
Point Of View ◽  
Sat Solving ◽  
Practical Point ◽  
Sat Solvers ◽  
Proof Systems ◽  
Real World Applications ◽  
Clause Learning

Complete SAT algorithms form an important part of the SAT literature. From a theoretical perspective, complete algorithms can be used as tools for studying the complexities of different proof systems. From a practical point of view, these algorithms form the basis for tackling SAT problems arising from real-world applications. The practicality of modern, complete SAT solvers undoubtedly contributes to the growing interest in the class of complete SAT algorithms. We review these algorithms in this chapter, including Davis-Putnum resolution, Stalmarck’s algorithm, symbolic SAT solving, the DPLL algorithm, and modern clause-learning SAT solvers. We also discuss the issue of certifying the answers of modern complete SAT solvers.

Chapter 12. Automated Configuration and Selection of SAT Solvers

2021 ◽  
Author(s):  
Holger H. Hoos ◽  
Frank Hutter ◽  
Kevin Leyton-Brown
Keyword(s):  
Research And Development ◽  
State Of The Art ◽  
Sat Solving ◽  
Sat Solvers ◽  
Effective Application ◽  
Automated Algorithm ◽  
Fertile Ground ◽  
Algorithm Configuration ◽  
Algorithmic Approaches ◽  
Selection Of

This chapter provides an introduction to the automated configuration and selection of SAT algorithms and gives an overview of the most prominent approaches. Since the early 2000s, these so-called meta-algorithmic approaches have played a major role in advancing the state of the art in SAT solving, giving rise to new ways of using and evaluating SAT solvers. At the same time, SAT has proven to be particularly fertile ground for research and development in the area of automated configuration and selection, and methods developed there have meanwhile achieved impact far beyond SAT, across a broad range of computationally challenging problems. Conceptually more complex approaches that go beyond “pure” algorithm configuration and selection are also discussed, along with some open challenges related to meta-algorithmic approaches, such as automated algorithm configuration and selection, to the tools based on these approaches, and to their effective application.

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

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.

scholarly journals Combining Conflict-Driven Clause Learning and Chronological Backtracking for Propositional Model Counting

10.29007/vgg4 ◽  
2019 ◽  
Author(s):  
Sibylle Möhle ◽  
Armin Biere
Keyword(s):  
State Of The Art ◽  
Search Space ◽  
Formal Proof ◽  
Propositional Formula ◽  
Sat Solvers ◽  
Model Counting ◽  
Clause Learning ◽  
Solver Performance

In propositional model counting, also named #SAT, the search space needs to be explored exhaustively, in contrast to SAT, where the task is to determine whether a propositional formula is satisfiable. While state-of-the-art SAT solvers are based on non- chronological backtracking, it has also been shown that backtracking chronologically does not significantly degrade solver performance. Hence investigating the combination of chronological backtracking with conflict-driven clause learning (CDCL) for #SAT seems evident. We present a calculus for #SAT combining chronological backtracking with CDCL and provide a formal proof of its correctness.

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.

Approximate Mining of Frequent -Subgraph Patterns in Evolving Graphs

2021 ◽  
Vol 15 (3) ◽  
pp. 1-35
Author(s):  
Muhammad Anis Uddin Nasir ◽  
Cigdem Aslay ◽  
Gianmarco De Francisci Morales ◽  
Matteo Riondato
Keyword(s):  
Sample Size ◽  
State Of The Art ◽  
Empirical Evaluation ◽  
Connected Subgraph ◽  
Dynamic Graphs ◽  
High Quality ◽  
Complexity Bounds ◽  
Approximation Quality ◽  
Uniform Sample ◽  
Waiting For Godot

“Perhaps he could dance first and think afterwards, if it isn’t too much to ask him.” S. Beckett, Waiting for Godot Given a labeled graph, the collection of -vertex induced connected subgraph patterns that appear in the graph more frequently than a user-specified minimum threshold provides a compact summary of the characteristics of the graph, and finds applications ranging from biology to network science. However, finding these patterns is challenging, even more so for dynamic graphs that evolve over time, due to the streaming nature of the input and the exponential time complexity of the problem. We study this task in both incremental and fully-dynamic streaming settings, where arbitrary edges can be added or removed from the graph. We present TipTap , a suite of algorithms to compute high-quality approximations of the frequent -vertex subgraphs w.r.t. a given threshold, at any time (i.e., point of the stream), with high probability. In contrast to existing state-of-the-art solutions that require iterating over the entire set of subgraphs in the vicinity of the updated edge, TipTap operates by efficiently maintaining a uniform sample of connected -vertex subgraphs, thanks to an optimized neighborhood-exploration procedure. We provide a theoretical analysis of the proposed algorithms in terms of their unbiasedness and of the sample size needed to obtain a desired approximation quality. Our analysis relies on sample-complexity bounds that use Vapnik–Chervonenkis dimension, a key concept from statistical learning theory, which allows us to derive a sufficient sample size that is independent from the size of the graph. The results of our empirical evaluation demonstrates that TipTap returns high-quality results more efficiently and accurately than existing baselines.

scholarly journals Video Frame Interpolation via Deformable Separable Convolution

2020 ◽  
Vol 34 (07) ◽  
pp. 10607-10614 ◽  
Author(s):  
Xianhang Cheng ◽  
Zhenzhong Chen
Keyword(s):  
State Of The Art ◽  
Video Frame ◽  
Kernel Size ◽  
Frame Interpolation ◽  
Interpolation Methods ◽  
Video Frames ◽  
Convolution Process ◽  
Strong Performance ◽  
Existing Frames ◽  
Better Than

Learning to synthesize non-existing frames from the original consecutive video frames is a challenging task. Recent kernel-based interpolation methods predict pixels with a single convolution process to replace the dependency of optical flow. However, when scene motion is larger than the pre-defined kernel size, these methods yield poor results even though they take thousands of neighboring pixels into account. To solve this problem in this paper, we propose to use deformable separable convolution (DSepConv) to adaptively estimate kernels, offsets and masks to allow the network to obtain information with much fewer but more relevant pixels. In addition, we show that the kernel-based methods and conventional flow-based methods are specific instances of the proposed DSepConv. Experimental results demonstrate that our method significantly outperforms the other kernel-based interpolation methods and shows strong performance on par or even better than the state-of-the-art algorithms both qualitatively and quantitatively.

scholarly journals Scaling Up AND/OR Abstraction Sampling

2020 ◽  
Author(s):  
Kalev Kask ◽  
Bobak Pezeshki ◽  
Filjor Broka ◽  
Alexander Ihler ◽  
Rina Dechter
Keyword(s):  
Importance Sampling ◽  
State Of The Art ◽  
Empirical Evaluation ◽  
Search Space ◽  
Scaling Up ◽  
Sampling Scheme ◽  
Search Spaces

Abstraction Sampling (AS) is a recently introduced enhancement of Importance Sampling that exploits stratification by using a notion of abstractions: groupings of similar nodes into abstract states. It was previously shown that AS performs particularly well when sampling over an AND/OR search space; however, existing schemes were limited to ``proper'' abstractions in order to ensure unbiasedness, severely hindering scalability. In this paper, we introduce AOAS, a new Abstraction Sampling scheme on AND/OR search spaces that allow more flexible use of abstractions by circumventing the properness requirement. We analyze the properties of this new algorithm and, in an extensive empirical evaluation on five benchmarks, over 480 problems, and comparing against other state of the art algorithms, illustrate AOAS's properties and show that it provides a far more powerful and competitive Abstraction Sampling framework.

Sign in / Sign up

Export Citation Format

Share Document