<p>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 <em>A</em>, which led to the conflict. However minimality is beneficial because like this you block other "bad" assignments as well. </p>

<p>Similarly, multiple MUCs are not a problem. All we need is to block the  assignment <em>A</em> 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.</p>

<p>To compute <strong>an</strong> MUC there're various algorithms. The easiest is to go through each literal <em>L</em> 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 <em>L</em> back (it's needed).  If I may shamelessly plug in my paper, here's more algorithms [1].</p>

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

CC BY-SA 3.0
2017-09-14T03:33:10.807Z
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.
ryan
CC BY-SA 3.0
2017-09-14T03:35:35.150Z
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.
ryan
CC BY-SA 3.0
2017-09-14T12:54:02.763Z
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
Mikolas
CC BY-SA 3.0
2017-09-14T18:38:03.293Z
@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.
Mikolas
CC BY-SA 3.0
2017-09-16T00:07:11.177Z
I believe your second comment answers my question, by dropping literals until it is SAT, we can figure out which ones must be included in a MUC. We may have to repeat this with the subset left over in case there are multiple MUCs.
ryan
CC BY-SA 3.0
2017-09-16T10:31:32.377Z
@ryan You remove a literal, it it's still UNSAT, good, otherwise put it back. Move onto the next literal. In theory you could enumerate multiple MUCs but typically it's not done in this context. You just pick one. In general the number of MUCs can be exponential. One MUC is enough because you really just need to block the assignment A from occurring again.
Mikolas
CC BY-SA 3.0
2017-09-16T19:17:41.210Z
yes that is a good point, we only need one MUC to prevent A from occurring again. This answers my question, if you add the info from your first* and third comments to the answer I'll go ahead an accept.
ryan
CC BY-SA 3.0
2017-09-18T08:56:39.480Z
@ryan Added some  clarification. Hope it makes sense. I wanted to keep it smallish so am not putting any formulas.
Mikolas
CC BY-SA 3.0
2017-09-13T22:19:15.387Z
2017-09-18T08:55:26.540Z
2017-09-18T08:55:26.540Z
Mikolas
<p>Recently in a course I'm taking, we have been learning about the <a href="https://en.wikipedia.org/wiki/Satisfiability_modulo_theories#SMT_solver_approaches" rel="nofollow noreferrer">DPLL(T) algorithm for SMT solving</a>. The basic outline goes like this:</p>
<pre><code>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))
</code></pre>
<p>This is all fine, but I struggle with the last line, <code>MinimalUnsatCore()</code>. Specifically, the  Minimal Unsatisfiable Core was defined as:</p>
<blockquote>
<p>An <em>Unsatisfiable Core</em> <span class="math-container">$C$</span> of <span class="math-container">$A$</span> contains a subset of atoms in <span class="math-container">$A$</span> such that <span class="math-container">$B'(C)$</span> is still unsatisfiable.</p>
<p>A <em>Minimal Unsatisfiable Core (MUC)</em> <span class="math-container">$C^*$</span> has the property that if you drop any single atom of <span class="math-container">$C^*$</span> from <span class="math-container">$A$</span>, the result is satisfiable.</p>
</blockquote>
<p>The description for finding the MUC was that you must drop each atom from <span class="math-container">$A$</span>, 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:</p>
<p><span class="math-container">$$(x = z) \wedge (x &gt; z) \wedge (y = z)$$</span></p>
<p>The MUC would be <span class="math-container">$\{(x= z), (x &gt; z)\}$</span>. However if we added another contradiction unrelated to this core:</p>
<p><span class="math-container">$$(x = z) \wedge (x &gt; z) \wedge (y = z) \wedge (y &gt; z)$$</span></p>
<p>Then at any point if we drop one individual atom, then <span class="math-container">$A$</span> 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?</p>
<p>See page 43 here: <a href="https://web.stanford.edu/class/cs357/lectures/lec9.pdf" rel="nofollow noreferrer">https://web.stanford.edu/class/cs357/lectures/lec9.pdf</a>
MUCs are referred to as part of the concept of &quot;Minimizing Learned Clauses&quot;. Specifically the method discussed on page 44.</p>
<hr />
<p>If this isn't the correct place for this question (maybe better over at Math.SE or CS.SE?), please let me know.</p>

CC BY-SA 3.0
2017-09-13T12:08:03.653Z
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).
Shaull
CC BY-SA 3.0
2017-09-13T18:02:55.080Z
@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.
ryan
CC BY-SA 3.0
2017-09-13T18:29:23.710Z
Can you give a link to the notes? (edit your post to include it, please).
Shaull
CC BY-SA 3.0
2017-09-13T21:44:38.267Z
@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).
ryan
<sat><boolean-formulas>
Minimum Unsatisfiable Core
ryan
# Minimum Unsatisfiable Core

(Asked by: username_0 on 2017-09-13)

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.

**Tags:** sat, boolean-formulas

> **Comments:**
> **username_1**: 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).  
> **username_0**: @username_1, 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.  
> **username_1**: Can you give a link to the notes? (edit your post to include it, please).  
> **username_0**: @username_1, 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).  

---

## 1 answers

### Answer by username_2 on 2017-09-13. Score: 5 | Accepted answer

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

> **Comments:**
> **username_0**: 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.  
> **username_0**: 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.  
> **username_2**: Hi @username_0. 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  
> **username_2**: @username_0 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.  
> **username_0**: I believe your second comment answers my question, by dropping literals until it is SAT, we can figure out which ones must be included in a MUC. We may have to repeat this with the subset left over in case there are multiple MUCs.  
> **username_2**: @username_0 You remove a literal, it it's still UNSAT, good, otherwise put it back. Move onto the next literal. In theory you could enumerate multiple MUCs but typically it's not done in this context. You just pick one. In general the number of MUCs can be exponential. One MUC is enough because you really just need to block the assignment A from occurring again.  
> **username_0**: yes that is a good point, we only need one MUC to prevent A from occurring again. This answers my question, if you add the info from your first* and third comments to the answer I'll go ahead an accept.  
> **username_2**: @username_0 Added some  clarification. Hope it makes sense. I wanted to keep it smallish so am not putting any formulas.  

---

