[YICES] Max-sat and unsat core

[Sanjai Narain]

  Hi Bruno: The specification is unsatisfiable even with max-sat because 
the weights are not specified, hence are assumed to be infinite. 
Correct? -- Sanjai


On 4/11/2011 1:03 PM, Bruno Dutertre wrote:
> Sanjai Narain wrote:
>>  The following spec is unsatisfiable but Yices does not print the 
>> unsat-core. Replacing (max-sat) with (check) does. Is there a way to 
>> get unsat-core with (max-sat)? Thanks -- Sanjai
>>
>>
>> (define-type node (scalar a b))
>> (define prop::(-> node int))
>> (assert+ (= (prop a) (prop b)))
>> (assert+ (= (prop a) 1))
>> (assert+ (= (prop b) 2))
>>
>> (max-sat)
>>
>
> I'm not sure what you mean by unsat core if you use max-sat.
> The whole point of max-sat is to search for a Boolean assignment
> that satisfies as many assertions as possible, so from a "max-sat"
> point-of-view, these assertions are satisfiable and there's no
> unsat core.
>
> Bruno