Author name cluster

Michael Veksler

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.

2 papers

1 author row

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

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