3
$\begingroup$

Recently in a course I'm taking, we have been learning about the DPLL(T) algorithm for SMT solving. The basic outline goes like this:

DPLL_T(F)
  G = B(F) // where B is the boolean abstraction function
  while (true) do
    A,out = SAT-solver(G)
    if (out = UNSAT) then return UNSAT
    else
      out = T-solver(B'(A)) // where B' is the inverse of B and T is a theory solver
      if (out = SAT) then return SAT
      else G = G and !B(MinimalUnsatCore(B'(A))

This is all fine, but I struggle with the last line, MinimalUnsatCore(). Specifically, the Minimal Unsatisfiable Core was defined as:

An Unsatisfiable Core $C$ of $A$ contains a subset of atoms in $A$ such that $B'(C)$ is still unsatisfiable.

A Minimal Unsatisfiable Core (MUC) $C^*$ has the property that if you drop any single atom of $C^*$ from $A$, the result is satisfiable.

The description for finding the MUC was that you must drop each atom from $A$, one by one, if the result of dropping a particular atom is satisfiable, then that atom must be in the MUC. This is fine, say, if there were only one conflict, for example:

$$(x = z) \wedge (x > z) \wedge (y = z)$$

The MUC would be $\{(x= z), (x > z)\}$. However if we added another contradiction unrelated to this core:

$$(x = z) \wedge (x > z) \wedge (y = z) \wedge (y > z)$$

Then at any point if we drop one individual atom, then $A$ is still not satisfiable because removing any one atom will still leave a contradiction. How do we remedy this to see that there are multiple MUCs? Can we still do this in linear time w.r.t. the number of atoms in the boolean abstraction? If not, what's the time complexity of finding all the MUCs?

See page 43 here: https://web.stanford.edu/class/cs357/lectures/lec9.pdf MUCs are referred to as part of the concept of "Minimizing Learned Clauses". Specifically the method discussed on page 44.


If this isn't the correct place for this question (maybe better over at Math.SE or CS.SE?), please let me know.

$\endgroup$
  • 1
    $\begingroup$ Where did you get this definition of a MUC from? Typically, MUC refers to a minimal number of clauses, rather than atoms (in which case your example no longer has a problem). $\endgroup$ – Shaull Sep 13 '17 at 12:08
  • $\begingroup$ @Shaull, the definition was from lecture material. They aren't actually "atoms" but rather, atomic formula of a boolean abstraction of an SMT formula. The boolean abstraction is sometimes referred to as the boolean skeleton. $\endgroup$ – ryan Sep 13 '17 at 18:02
  • $\begingroup$ Can you give a link to the notes? (edit your post to include it, please). $\endgroup$ – Shaull Sep 13 '17 at 18:29
  • $\begingroup$ @Shaull, my professor's notes are not publicly available, so the link would be useless, but I have found lecture notes from Stanford that use the same methodology (starting page 43). $\endgroup$ – ryan Sep 13 '17 at 21:44
4
$\begingroup$

First thing to say that the minimality here is subset-minimality (as opposed to cardinality-minimality). Observe that minimality is not actually needed. The main objective is to block the assignment A, which led to the conflict. However minimality is beneficial because like this you block other "bad" assignments as well.

Similarly, multiple MUCs are not a problem. All we need is to block the assignment A so picking an arbitrary MUC is sufficient. Note also that the number of MUCs can be exponential, so going through all of them might not even be feasible and typically is not done in this context.

To compute an MUC there're various algorithms. The easiest is to go through each literal L in the set and remove it. If the set is still UNSAT, then move onto the next literal. If the set is SAT, put the literal L back (it's needed). If I may shamelessly plug in my paper, here's more algorithms [1].

[1] Minimal Sets over Monotone Predicates in Boolean Formulae. J Marques-Silva, M Janota, A Belov. CAV13

$\endgroup$
  • $\begingroup$ I am new to this, so bear with me, but you say "You could just block that one particular assignment that led to the conflict." My problem is that any assignment leads to a conflict. For $(x = y) \wedge (x \neq y)$, no assignment of $x$ and $y$ will satisfy this conflict. $\endgroup$ – ryan Sep 14 '17 at 3:33
  • $\begingroup$ Further, "The easiest is to drop literals as long there still [is] conflict." If we do this, which are being included in the MUC; the dropped literals? If we include the dropped literals in the MUC, this would not result in a Minimal Unsatisfiable Core. If there are multiple pairs of conflicts, we may end up removing all non-conflicts as well. $\endgroup$ – ryan Sep 14 '17 at 3:35
  • 1
    $\begingroup$ Hi @ryan. Not sure if I follow. If your problem has no solution, you'll eventually block all assignments and the SAT part gives UNSAT. You keep the literals that are not dropped. E.g. from x = y, x<y, x>y drop (remove) the first one and it's an MUC bcs removing anything further will make it satisisfiable. So you'll effectively add x>=y OR x<=y $\endgroup$ – Mikolas Sep 14 '17 at 12:54
  • $\begingroup$ @ryan You might want to check out Example 3.1 in Solving SAT and SAT Modulo Theories: From an Abstract Davis–Putnam–Logemann–Loveland Procedure to DPLL(T). That should be easy to understand. $\endgroup$ – Mikolas Sep 14 '17 at 18:38
  • 1
    $\begingroup$ @ryan Added some clarification. Hope it makes sense. I wanted to keep it smallish so am not putting any formulas. $\endgroup$ – Mikolas Sep 18 '17 at 8:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.