getConflictClause() and minizeUnsatCore() always return empty results

[xieyangxu]

running monoSAT with Python bindings, the getConflictClause() function following the Solve() always returns empty list, nomatter SAT or UNSAT result. Is this an expected result?

[sambayless]

Hi! Yes, that is expected. getConflictClause() only considers assumption literals (this is the same as MiniSAT).

Specifically, when calling solve(), you can optionally pass in a list of assumption literals, which will be treated as temporary unit clauses for the duration of that solve call. For example, if you have added clause (a & ~b) to the solver, and then you call solve(~a), then during that solve call, a unit clause (~a) will be temporarily applied. (So the only satisfying solution in that case is ~a & ~b). But in subsequent call to solve(), that unit clause will be removed and 'a' will again be free.

The unsat core and conflict clause that monosat considers only take into account the assumption literals, so if you haven't set any assumption literals during the most recent solve call, the conflict clause will always be empty.

Similarly, minimizeUnsatCore() only produces a (locally) minimal unsat core of assumption literals, not of all clauses.