[YICES] Re: Question on Yices for Max-SAT

[Bruno Dutertre]

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.
>>>
>>> Regards,
>>> Marco
>>
>> 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
>> example.
>>
>> 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
>>
>>    (max-sat)
>>
>> 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,
>>
>>
>> Bruno
> 
> 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
> problems?
> 
> Thank you again.
> 
> Regards,
> Marco
> 

Hi Marco,

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
size problems.

Bruno