Author name cluster

Vadim Ryvchin

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

9 papers

1 author row

SAT Conference 2018 Conference Paper

Chronological Backtracking

Alexander Nadel
Vadim Ryvchin

Abstract Non-Chronological Backtracking (NCB) has been implemented in every modern CDCL SAT solver since the original CDCL solver GRASP. NCB’s importance has never been questioned. This paper argues that NCB is not always helpful. We show how one can implement the alternative to NCB–Chronological Backtracking (CB)–in a modern SAT solver. We demonstrate that CB improves the performance of the winner of the latest SAT Competition, Maple_LCM_Dist, and the winner of the latest MaxSAT Evaluation Open-WBO.

Details

SAT Conference 2015 Conference Paper

Hints Revealed

Jonathan Kalechstain
Vadim Ryvchin
Nachum Dershowitz

Abstract We propose a notion of hints, clauses that are not necessarily consistent with the input formula. The goal of adding hints is to speed up the SAT solving process. For this purpose, we provide an efficient general mechanism for hint addition and removal. When a hint is determined to be inconsistent, a hint-based partial resolution-graph of an unsatisfiable core is used to reduce the search space. The suggested mechanism is used to boost performance by adding generated hints to the input formula. We describe two specific hint-suggestion methods, one of which increases performance by 30% on satisfiable SAT ’13 competition instances and solves 9 instances not solved by the baseline solver.

Details

SAT Conference 2015 Conference Paper

Mining Backbone Literals in Incremental SAT - A New Kind of Incremental Data

Alexander Ivrii
Vadim Ryvchin
Ofer Strichman

Abstract In incremental SAT solving, information gained from previous similar instances has so far been limited to learned clauses that are still relevant, and heuristic information such as activity weights and scores. In most settings in which incremental satisfiability is applied, many of the instances along the sequence of formulas being solved are unsatisfiable. We show that in such cases, with a P-time analysis of the proof, we can compute a set of literals that are logically implied by the next instance. By adding those literals as assumptions, we accelerate the search.

Details

SAT Conference 2014 Conference Paper

Ultimately Incremental SAT

Alexander Nadel
Vadim Ryvchin
Ofer Strichman

Abstract Incremental SAT solving under assumptions, introduced in Minisat, is in wide use. However, Minisat’s algorithm for incremental SAT solving under assumptions has two main drawbacks which hinder performance considerably. First, it is not compliant with the highly effective and commonly used preprocessor SatELite. Second, all the assumptions are left in the formula, rather than being represented as unit clauses, propagated, and eliminated. Two previous attempts to overcome these problems solve either the first or the second of them, but not both. This paper remedies this situation by proposing a comprehensive solution for incremental SAT solving under assumptions, where SatELite is applied and all the assumptions are propagated. Our algorithm outperforms existing approaches over publicly available instances generated by a prominent industrial application in hardware validation.

Details

SAT Conference 2012 Conference Paper

Efficient SAT Solving under Assumptions

Alexander Nadel
Vadim Ryvchin

Abstract In incremental SAT solving, assumptions are propositions that hold solely for one specific invocation of the solver. Effective propagation of assumptions is vital for ensuring SAT solving efficiency in a variety of applications. We propose algorithms to handle assumptions. In our approach, assumptions are modeled as unit clauses, in contrast to the current state-of-the-art approach that models assumptions as first decision variables. We show that a notable advantage of our approach is that it can make preprocessing algorithms much more effective. However, our initial scheme renders assumption-dependent (or temporary) conflict clauses unusable in subsequent invocations. To resolve the resulting problem of reduced learning power, we introduce an algorithm that transforms such temporary clauses into assumption-independent pervasive clauses. In addition, we show that our approach can be enhanced further when a limited form of look-ahead information is available. We demonstrate that our approach results in a considerable performance boost of the SAT solver on instances generated by a prominent industrial application in hardware validation.

Details

SAT Conference 2012 Conference Paper

Preprocessing in Incremental SAT

Alexander Nadel
Vadim Ryvchin
Ofer Strichman

Abstract Preprocessing of CNF formulas is an invaluable technique when attempting to solve large formulas, such as those that model industrial verification problems. Unfortunately, the best combination of preprocessing techniques, which involve variable elimination combined with subsumption, is incompatible with incremental satisfiability. The reason is that soundness is lost if a variable is eliminated and later reintroduced. Look-ahead is a known technique to solve this problem, which simply blocks elimination of variables that are expected to be part of future instances. The problem with this technique is that it relies on knowing the future instances, which is impossible in several prominent domains. We show a technique for this realm, which is empirically far better than the known alternatives: running without preprocessing at all or applying preprocessing separately at each step.

Details

SAT Conference 2011 Conference Paper

Faster Extraction of High-Level Minimal Unsatisfiable Cores

Vadim Ryvchin
Ofer Strichman

Abstract Various verification techniques are based on SAT’s capability to identify a small, or even minimal, unsatisfiable core in case the formula is unsatisfiable, i. e. , a small subset of the clauses that are unsatisfiable regardless of the rest of the formula. In most cases it is not the core itself that is being used, rather it is processed further in order to check which clauses from a preknown set of Interesting Constraints (where each constraint is modeled with a conjunction of clauses) participate in the proof. The problem of minimizing the participation of interesting constraints was recently coined high-level minimal unsatisfiable core by Nadel [15]. Two prominent examples of verification techniques that need such small cores are 1) abstraction-refinement model-checking techniques, which use the core in order to identify the state variables that will be used for refinement (smaller number of such variables in the core implies that more state variables can be replaced with free inputs in the abstract model), and 2) assumption minimization, where the goal is to minimize the usage of environment assumptions in the proof, because these assumptions have to be proved separately. We propose seven improvements to the recent solution given in [15], which together result in an overall reduction of 55% in run time and 73% in the size of the resulting core, based on our experiments with hundreds of industrial test cases. The optimized procedure is also better empirically than the assumptions-based minimization technique.

Details

SAT Conference 2010 Conference Paper

Assignment Stack Shrinking

Alexander Nadel
Vadim Ryvchin

Abstract Assignment stack shrinking is a technique that is intended to speed up the performance of modern complete SAT solvers. Shrinking was shown to be efficient in SAT’04 competition winners Jerusat and Chaff. However, existing studies lack the details of the shrinking algorithm. In addition, shrinking’s performance was not tested in conjunction with the most modern techniques. This paper provides a detailed description of the shrinking algorithm and proposes two new heursitics for it. We show that using shrinking is critical for solving well-known industrial benchmark families with the latest versions of Minisat and Eureka.

Details

SAT Conference 2008 Conference Paper

Local Restarts

Vadim Ryvchin
Ofer Strichman

Abstract Most or even all competitive DPLL-based SAT solvers have a “restart” policy, by which the solver is forced to backtrack to decision level 0 according to some criterion. Although not a sophisticated technique, there is mounting evidence that this technique has crucial impact on performance. The common explanation is that restarts help the solver avoid spending too much time in branches in which there is neither an easy-to-find satisfying assignment nor opportunities for fast learning of strong clauses. All existing techniques rely on a global criterion such as the number of conflicts learned as of the previous restart, and differ in the method of calculating the threshold after which the solver is forced to restart. This approach disregards, in some sense, the original motivation of focusing on ‘bad’ branches. It is possible that a restart is activated right after going into a good branch, or that it spends all of its time in a single bad branch. We suggest instead to localize restarts, i. e. , apply restarts according to measures local to each branch. This adds a dimension to the restart policy, namely the decision level in which the solver is currently in. Our experiments with both Minisat and Eureka show that with certain parameters this improves the run time by 15% - 30% on average (when applied to the 100 test benchmarks of SAT-race’06), and reduces the number of time-outs.

Details