[YICES] Re: Question on Yices for Max-SAT
bruno at csl.sri.com
Fri Oct 14 09:36:00 PDT 2011
Marco Maratea wrote:
> On Fri, 2011-04-22 at 15:16 -0700, Bruno Dutertre wrote:
>> Marco Maratea wrote:
>>> Hi Bruno,
>>> I Marco Maratea, one of the authors of TSAT++ as you may remember.
>>> I am working again on TSAT++: a student of mine is extending TSAT++
>>> to handle quantitative weights associated to DTP constraints
>>> (disjunction of difference constraints). A formula is a conjunction of
>>> DTP constraints.
>>> I would like now to evaluate such formulas with yices v.1
>>> The idea for applying weights to DTP constraints is to use a sort of
>>> "constraint boolean selectors" (the s* variables) to each DTP
>>> constraint, then applying the optimization on such variables (with a
>>> further constraint which forbids a naive solution where all s* variables
>>> are set to false)
>>> Is the attached formula correctly formulated for solving such problem?
>>> (where 26 is the reward for satisfying the first DTP constraint
>>> (x0 - x3 <= -8) v ( x4 - x1 <= -14), 21 for second DTP constraint, and
>>> so on).
>>> Thank you for your attention.
>> Hi Marco,
>> This encoding does not work. It is syntactically correct but
>> Yices does not interpret any of the (assert+ ...) as weighted
>> assertions. So (max-sat) is the same as (check) on this
>> The auxiliary variables s1 ... s30 and the 'min' assertion
>> are probably not useful.
>> You have to attach the weight to the assertions as in
>> (assert+ (or (<= (- x0 x3) -8) (<= (- x4 x1) -14)) 26)
>> (assert+ (or (<= (- x4 x1) 25) (<= (- x4 x2) 95)) 21)
>> Then you can just use
>> Yices is going to search for a satisfying assignment of maximal weight.
>> If you really want to keep s1 ... s30, then you can do this
>> in two steps. First assert a hard constraint (don't use assert+)
>> (assert (or (not s1) (or (<= (- x0 x3) -8) (<= (- x4 x1) -14) )))
>> then assert that s1 must be true with the relevant weight
>> (assert+ s1 26)
>> Then use (max-sat) as above,
> Hi again Bruno,
> I herewith acknowledge that Yices performs very well on Max-DTPs
> problems as I defined above.
> Hope this is a good news for you.
> I would like now to test Yices on mathematical formulations of some
> problems from transportation and logistics expressed as linear
> programming problems whose variables are boolean, or mixed boolean/real:
> does Yices support solving ILP (or better, Boolean LP) and MILP
> Thank you again.
Thanks for the feedback.
Yices can solve MILP/ILP feasibility problems. It does not
directly support optimization problems (if that's what you
care about). It's still possible to solve optimization problems
with Yices by converting them into a series of feasibility problems.
Also, don't expect Yices to be competitive with specialized MILP/
ILP solvers on large problems. But it should work fine on medium
More information about the YICES