scholarly journals RAT Elimination

10.29007/fccb ◽  
2020 ◽  
Author(s):  
Adrian Rebola Pardo ◽  
Georg Weissenbacher
Keyword(s):  
State Of The Art ◽  
Propositional Formula ◽  
Sat Solving ◽  
Proof Systems ◽  
Resolution Proofs

Inprocessing techniques have become one of the most promising advancements in SAT solving over the last decade. Some inprocessing techniques modify a propositional formula in non model-perserving ways. These operations are very problematic when Craig inter- polants must be extracted: existing methods take resolution proofs as an input, but these inferences require stronger proof systems; state-of-the-art solvers generate DRAT proofs. We present the first method to transform DRAT proofs into resolution-like proofs by elim- inating satisfiability-preserving RAT inferences. This solves the problem of extracting interpolants from DRAT proofs.

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

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.

scholarly journals SAT solving experiments in Vampire

10.29007/5l47 ◽  
2018 ◽  
Author(s):  
Armin Biere ◽  
Ioan Dragan ◽  
Laura Kovács ◽  
Andrei Voronkov
Keyword(s):  
State Of The Art ◽  
Theorem Prover ◽  
Sat Solving ◽  
First Order ◽  
Automated Theorem Prover ◽  
Sat Solver ◽  
Overall Performance

In order to better understand how well a state of the art SAT solver would behave in the framework of a first-order automated theorem prover we have decided to integrate Lingeling, best performing SAT solver, inside Vampire’s AVATAR framework. In this paper we propose two ways of integrating a SAT solver inside of Vampire and evaluate overall performance of this combination. Our experiments show that by using a state of the art SAT solver in Vampire we manage to solve more problems. Surprisingly though, there are cases where combination of the two solvers does not always prove to generate best results.

scholarly journals Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures

10.29007/73n4 ◽  
2018 ◽  
Author(s):  
Martin Aigner ◽  
Armin Biere ◽  
Christoph Kirsch ◽  
Aina Niemetz ◽  
Mathias Preiner
Keyword(s):  
Experimental Evaluation ◽  
State Of The Art ◽  
Memory System ◽  
Memory Access ◽  
Sat Solving ◽  
Running Time ◽  
Current State ◽  
The Individual

Effectively parallelizing SAT solving is an open andimportant issue. The current state-of-the-art isbased on parallel portfolios. This technique relieson running multiple solvers on the same instance inparallel. As soon one instance finishes the entirerun stops. Several succesful systems even use plainparallel portfolio (PPP), where the individual solversdo not exchange any information. This paper containsa thorough experimental evaluation which shows that PPPcan improve wall-clock running time because memory accessis still local, respectively the memory system can hidethe latency of memory access. In particular, there doesnot seem as much cache congestion as one might imagine.We also present some limits on the scalibility of PPP.Thus this paper gives one argument why PPP solvers are agood fit for todays multi-core architectures.

scholarly journals Solving #SAT and Bayesian Inference with Backtracking Search

2009 ◽  
Vol 34 ◽  
pp. 391-442 ◽  
Author(s):  
F. Bacchus ◽  
S. Dalmao ◽  
T. Pitassi
Keyword(s):  
Probabilistic Reasoning ◽  
State Of The Art ◽  
Exact Algorithm ◽  
Propositional Formula ◽  
Performance Gain ◽  
Bayes Nets ◽  
Backtracking Search ◽  
Time Space ◽  
Sum Of Products ◽  
Improved Performance

Inference in Bayes Nets (BAYES) is an important problem with numerous applications in probabilistic reasoning. Counting the number of satisfying assignments of a propositional formula (#SAT) is a closely related problem of fundamental theoretical importance. Both these problems, and others, are members of the class of sum-of-products (SUMPROD) problems. In this paper we show that standard backtracking search when augmented with a simple memoization scheme (caching) can solve any sum-of-products problem with time complexity that is at least as good any other state-of-the-art exact algorithm, and that it can also achieve the best known time-space tradeoff. Furthermore, backtracking’s ability to utilize more flexible variable orderings allows us to prove that it can achieve an exponential speedup over other standard algorithms for SUMPROD on some instances. The ideas presented here have been utilized in a number of solvers that have been applied to various types of sum-of-product problems. These system’s have exploited the fact that backtracking can naturally exploit more of the problem’s structure to achieve improved performance on a range of probleminstances. Empirical evidence of this performance gain has appeared in published works describing these solvers, and we provide references to these works.

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.

Chapter 15. Proofs of Unsatisfiability

2021 ◽  
Author(s):  
Marijn J.H. Heule
Keyword(s):  
State Of The Art ◽  
Sat Solvers ◽  
Proof Systems ◽  
Speed Up

Satisfiability (SAT) solvers have become complex tools, which raises the question of whether we can trust their results. This question is particularly important when the solvers are used to determine the correctness of hardware and software and when they are used to produce mathematical results. To deal with this issue, solvers can provide proofs of unsatisfiability to certify the correctness of their answers. This chapter presents the history and state-of-the-art of producing and validating proofs of unsatisfiability. The chapter covers the most popular proof formats with and without hints to speed up certification. Hints in proofs make validation easy, which resulted in several efficient formally-verified checkers. Various proof systems are discussed, ranging from resolution to the recent propagation redundancy system. The chapter also describes techniques to compress and optimize proofs.

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.

Sign in / Sign up

Export Citation Format

Share Document