Minimum Unsatisfiable Core 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 &gt; z) \wedge (y = z)$$
The MUC would be $\{(x= z), (x &gt; z)\}$. However if we added another contradiction unrelated to this core:
$$(x = z) \wedge (x &gt; z) \wedge (y = z) \wedge (y &gt; 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 &quot;Minimizing Learned Clauses&quot;. 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.
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