[YICES] Max-sat and unsat core
narain at research.telcordia.com
Mon Apr 11 10:36:41 PDT 2011
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))
> 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.
More information about the YICES