getConflictClause returns the negation of assumption literals

[amnore]

Hello, I'm using monosat to solve some problems of graphs, and I am a little confused by the behavior of getConflictClause because the returned value is the negation of those literals:

from monosat import *
g = Graph()
a = g.addNode()
b = g.addNode()
e1 = g.addEdge(a, b)
e2 = g.addEdge(b, a)
x = g.acyclic()
Solve(e1, e2, x)

print(getConflictClause())
# [7, 5, 3]
print([e1, e2, x])
# [2, 4, 6]
print(list(map(Not, [e1, e2, x])))
# [3, 5, 7]

I assume it should return exactly the passed literals? Or is this the intended behavior?

[amnore]

It looks like I'm looking fore minimizeUnsatCore... Sorry for that.

[sambayless]

No problem at all!

getConflictClause and minimizeUnsatCore are closely related. getConflictClauses behaviour shouldn't change depending on which theories are used (and it sounds like you confirmed that it does not change after all - that would have been a bug if it did).

getConflictClause will return a (negated) subset of the assumption literals, such that at least one of those (negated) literals must be true or else the formula will remain unsatisfiable; this clause is produced on a best effort basis by the solver as part of proving the original formula UNSAT (in conjunction with the assumption literals). This behaviour of returning the negated literals matches MiniSATs, but I agree its a bit counter-intuitive. I always have to double check, personally.

minimizeUnsatCore will make repeated SAT calls to find a (locally) minimal subset of the assumption literals that are mutually UNSAT. So that is going to be a lot more expensive.

If you dont need actually a minimal unsat core, and you simply want the assumption literals back in their original polarity, my recommendation is use getConflictClause, and just negate the literals back to positive to get the original literals used.