Author name cluster

Ofer Strichman

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

2 author rows

JAIR Journal 2020 Journal Article

Learning the Language of Software Errors

Hana Chockler
Pascal Kesseli
Daniel Kroening
Ofer Strichman

We propose to use algorithms for learning deterministic finite automata (DFA), such as Angluin’s L* algorithm, for learning a DFA that describes the possible scenarios under which a given program error occurs. The alphabet of this automaton is given by the user (for instance, a subset of the function call sites or branches), and hence the automaton describes a user-defined abstraction of those scenarios. More generally, the same technique can be used for visualising the behavior of a program or parts thereof. It can also be used for visually comparing different versions of a program (by presenting an automaton for the behavior in the symmetric difference between them), and for assisting in merging several development branches. We present experiments that demonstrate the power of an abstract visual representation of errors and of program segments, accessible via the project’s web page. In addition, our experiments in this paper demonstrate that such automata can be learned efficiently over real-world programs. We also present lazy learning, which is a method for reducing the number of membership queries while using L *, and demonstrate its effectiveness on standard benchmarks.

PDF Details DOI

AIJ Journal 2016 Journal Article

Learning general constraints in CSP

Michael Veksler
Ofer Strichman

We present a new learning scheme for solvers of the Constraint Satisfaction Problem (CSP), which is based on learning (general) constraints rather than the generalized no-goods or signed-clauses that were used in the past. The new scheme is integrated in a conflict-analysis algorithm reminiscent of a modern systematic propositional satisfiability (SAT) solver: it traverses the conflict graph backwards and gradually builds an asserting conflict constraint. This construction is based on new inference rules that are tailored for various pairs of constraints types, e. g. , x ≤ y 1 + k 1 and x ≥ y 2 + k 2, or y 1 ≤ x and [ x, y 2 ] ⊈ [ a, b ]. The learned constraint is stronger than what can be learned via signed resolution. Our experiments show that our solver HCSP backtracks orders of magnitude less than other state-of-the-art solvers, and is overall on par with the winner of this year's MiniZinc challenge.

Details DOI

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

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

AAAI Conference 2010 Conference Paper

A Proof-Producing CSP Solver

Michael Veksler
Ofer Strichman

PCS is a CSP solver that can produce a machine-checkable deductive proof in case it decides that the input problem is unsatisfiable. The roots of the proof may be nonclausal constraints, whereas the rest of the proof is based on resolution of signed clauses, ending with the empty clause. PCS uses parameterized, constraint-specific inference rules in order to bridge between the nonclausal and the clausal parts of the proof. The consequent of each such rule is a signed clause that is 1) logically implied by the nonclausal premise, and 2) strong enough to be the premise of the consecutive proof steps. The resolution process itself is integrated in the learning mechanism, and can be seen as a generalization to CSP of a similar solution that is adopted by competitive SAT solvers.

PDF 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

SAT Conference 2005 Conference Paper

Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas

Roman Gershman
Ofer Strichman

Abstract We present an improvement to the Hyper preprocessing algorithm that was suggested by Bacchus and Winter in SAT 2003 [1]. Given the power of modern SAT solvers, Hyper is currently one of the only cost-effective preprocessors, at least when combined with some modern SAT solvers and on certain classes of problems. Our algorithm, although it produces less information than Hyper, is much more efficient. Experiments on a large set of industrial Benchmark sets from previous SAT competitions show that HyperBinFast is always faster than Hyper (sometimes an order of magnitude faster on some of the bigger CNF formulas), and achieves faster total run times, including the SAT solver’s time. The experiments also show that HyperBinFast is cost-effective when combined with three state-of-the-art SAT solvers.

Details