shaobo-he / sls

OL1V3R: Reimplementation of "Stochastic Local Search for Satisfiability Modulo Theories" in Racket (probably with support of FP)
Other
2 stars 0 forks source link

study griggio/fmcad12/newton.6.3.i.smt2 #17

Open shaobo-he opened 5 years ago

shaobo-he commented 5 years ago

This script consists of three assertions, two of them (a1, a2) constraining the input range and the other one (a3) constraining the computation result. Let's say we start at a point v where a1 a3 are satisfied while a2 is not. Assume neighbors of v violate a3 but satisfy a2. The general result will be better letting a2 keep unsatisfied because violating a3 actually leads to lower scores or no improvement.

One solution is to add weights which has effects where satisfying a2 yields higher score. This in turn makes sure the variable is within bound.

The other solution is to record the range and use it in generating neighbors/restarts.