Produced unsat-core is not subset-minimal

[Tomaqa]

In the following benchmark, the produced unsat-core is not subset-minimal although the solver was asked to:

(set-option :produce-unsat-cores true)
(set-option :minimal-unsat-cores true)
(set-logic QF_LRA)
(declare-fun x1 () Real)
(declare-fun x2 () Real)
(declare-fun x3 () Real)
(declare-fun l1y1 () Real)
(declare-fun l1y2 () Real)
(declare-fun l1x1 () Real)
(declare-fun l1x2 () Real)
(declare-fun c1 () Real)
(declare-fun c2 () Real)

(assert (and (>= x1 0) (<= x1 4)))
(assert (and (>= x2 0) (<= x2 4)))
(assert (and (>= x3 0) (<= x3 4)))

(assert (= l1y1 (+ (* 2 x1) x3)) )
(assert (= l1y2 (+ (- x1) x2 (- x3))) )
(assert (= l1x1 (ite (> l1y1 0) l1y1 0)) )
(assert (= l1x2 (ite (> l1y2 0) l1y2 0)) )
(assert (= c1 (+ l1x1 (* (- 4) l1x2))) )
(assert (= c2 (+ (- l1x1) (* 4 l1x2))) )

(assert (< c1 c2))

(assert (! (= x1 1) :named s1))
(assert (! (= x2 1) :named s2))
(assert (! (= x3 3) :named s3))

(check-sat)
(get-unsat-core)
(exit)

Output:

unsat
(
s1
s2
s3
)

Correct cores: one of (s2 s3), (s1 s3), (s1 s2).

One can easily check that commenting out one of the named assertions leaves the formula still unsatisfiable and produces one of the cores above.

I tried the latest release and pre-release of CVC5 on Linux 6.6.28-1-lts.

I believe that the configuration and parameters do not matter here.

[HanielB]

This is an interesting case. Looking in more detail at what is going on, note that the full unsat core (you can see it with --print-cores-full and removing the minimization option) you have

(
(= l1y1 (+ (* 2.0 x1) x3))
(= l1y2 (+ (- x1) x2 (- x3)))
(= l1x1 (ite (> l1y1 0.0) l1y1 0.0))
(= l1x2 (ite (> l1y2 0.0) l1y2 0.0))
(= c1 (+ l1x1 (* (- 4.0) l1x2)))
(= c2 (+ (- l1x1) (* 4.0 l1x2)))
(< c1 c2)
(= x1 1.0)
(= x2 1.0)
(= x3 3.0)
)

where note that the first three assertions are not in the core. That is the starting point from which cvc5 tries to minimize, to which it gets to

(
(= l1y2 (+ (- x1) x2 (- x3)))
(= l1x1 (ite (> l1y1 0.0) l1y1 0.0))
(= l1x2 (ite (> l1y2 0.0) l1y2 0.0))
(= c1 (+ l1x1 (* (- 4.0) l1x2)))
(= c2 (+ (- l1x1) (* 4.0 l1x2)))
(< c1 c2)
(= x1 1.0)
(= x2 1.0)
(= x3 3.0)
)

since it only manages to remove the first formula from the core. It is not the case that you can remove any of the three assertions you have named from the core from which you have already removed those first three assertions. This is not the functionality you want though, since you want to minimize just the named assertions, reported in the unsat core. That is not something we currently support though.

[blishko]

Hi @HanielB,

are you saying that cvc5 does not support minimization of just the named assertions?

We have gone through a similar reasoning process recently in OpenSMT with @Tomaqa (based on this example he has discovered). What is interesting here is indeed that some assertions are named and some are not. If you start from an unsat core that excludes the first three (unnamed) assertions, then it is true that you cannot remove any of the named ones anymore. Yet, the unsat core (restricted to the named assertions) is not locally minimal. Based on the description in this blog post we thought cvc5 is supposed to guarantee minimality with this option.

[Tomaqa]

I have found yet another, even simpler example:

(set-option :produce-unsat-cores true)
(set-option :minimal-unsat-cores true)

(set-logic QF_UF)

(declare-const b1 Bool)
(declare-const b2 Bool)

(assert (! b1 :named a1))
(assert (! b2 :named a2))
(assert (! (not b1) :named a3))
(assert (and b1 b2))
(assert (or b1 b2))
(assert (xor b1 b2))

(check-sat)
(get-unsat-core)

CVC5 outputs:

unsat
(
a1
a3
)

But the subset-minimal unsat core should be empty, based on our understanding of your definition of minimal unsat cores. The definition should be probably concretized because it allows multiple interpretations.

Also, compare the example above with the following:

(set-option :produce-unsat-cores true)
(set-option :minimal-unsat-cores true)

(set-logic QF_UF)

(declare-const b1 Bool)
(declare-const b2 Bool)

(assert b1)
(assert b2)
(assert (not b1))
(assert (! (and b1 b2) :named a1))
(assert (! (or b1 b2) :named a2))
(assert (! (xor b1 b2) :named a3))

(check-sat)
(get-unsat-core)

.. where we changed the named terms to the other inconsistent group of constraints. Now CVC5 returns empty unsat-core. This seems a bit inconsistent. Furthermore, if we change just the order of the formulas above to

(set-option :produce-unsat-cores true)
(set-option :minimal-unsat-cores true)

(set-logic QF_UF)

(declare-const b1 Bool)
(declare-const b2 Bool)

(assert (! (and b1 b2) :named a1))
(assert (! (or b1 b2) :named a2))
(assert (! (xor b1 b2) :named a3))
(assert b1)
(assert b2)
(assert (not b1))

(check-sat)
(get-unsat-core)

then CVC5 again outputs:

unsat
(
a1
a3
)

[HanielB]

Thanks for the further comments. The behavior of both get-unsat-core and the cvc5-specific minimal-unsat-cores option are in line with how SMT-LIB defines (see page 68 of the standard) what should be the result of get-unsat-core w.r.t. named assertions:

"The solver selects from the unsatisfiable core only those formulas that have been asserted with a command of the form (assert (! t :named f )), and returns a sequence ( f1 · · · fn) of those labels".

The functionality that you want would require not selecting named assertions from the unsat core, but computing an unsat core differently, where you'd consider unsatisfiability of subsets of the named assertions vs all other assertions. You can sort of reproduce this functionality (for the original example) by putting all unnamed assertions under a single assert, i.e.:

(set-option :produce-unsat-cores true)
(set-option :minimal-unsat-cores true)
(set-logic QF_LRA)
(declare-fun x1 () Real)
(declare-fun x2 () Real)
(declare-fun x3 () Real)
(declare-fun l1y1 () Real)
(declare-fun l1y2 () Real)
(declare-fun l1x1 () Real)
(declare-fun l1x2 () Real)
(declare-fun c1 () Real)
(declare-fun c2 () Real)

(assert
    (and
        (and (>= x1 0) (<= x1 4))
        (and (>= x2 0) (<= x2 4))
        (and (>= x3 0) (<= x3 4))
        (= l1y1 (+ (* 2 x1) x3))
        (= l1y2 (+ (- x1) x2 (- x3)))
        (= l1x1 (ite (> l1y1 0) l1y1 0))
        (= l1x2 (ite (> l1y2 0) l1y2 0))
        (= c1 (+ l1x1 (* (- 4) l1x2)))
        (= c2 (+ (- l1x1) (* 4 l1x2)))
        (< c1 c2)))

(assert (! (= x1 1) :named s1))
(assert (! (= x2 1) :named s2))
(assert (! (= x3 3) :named s3))
(check-sat)
(get-unsat-core)
(exit)

to which cvc5 produces the unsat core (s1 s2 s3) and minimized unsat core (s2 s3).