<p>Umans proved that a problem that he calls &quot;succinct set cover&quot; is <span class="math-container">$\Sigma_2^p$</span>-complete [1]. In this problem we are given a DNF-formula with terms <span class="math-container">$T=\{t_1,\dots,t_m\}$</span> and a parameter <span class="math-container">$k$</span>, the question being whether <span class="math-container">$T$</span> has a subset <span class="math-container">$T'$</span> of size at most <span class="math-container">$k$</span> such that <span class="math-container">$\bigvee T'$</span> is a tautology. Your problem should be equivalent with this problem by duality, so both are <span class="math-container">$\Sigma_2^p$</span>-complete.</p>
<p>[1] C. Umans. Hardness of Approximating Σp 2 Minimization Problems. In IEEE Symposium on Foundations of Computer Science (FOCS), pages 465–474, 1999.</p>

CC BY-SA 4.0
2024-09-24T13:04:49.020Z
Thanks for your super quick and correct answer! I agree: asking for a minimum subset of clauses of a CNF which is unsat is equivalent to asking for a minimum subset of terms of the corresponding DNF which is tautological, so minimum unsatisfiable core is equivalent to that problem. Very nice. Out of curiosity do you happen to also know the complexity of computing a *minimal* unsatisfiable core?
Antoine Amarilli 'a3nm'
CC BY-SA 4.0
2024-09-24T13:31:50.913Z
@a3nm For this one I don't have a reference, but it should be complete for the class of search problems solvable in polynomial time with at most logarithmic number of calls to a $\Sigma_2^p$-witness oracle. Witness oracle means that the oracle not only gives you yes-no answer but also gives you the witness.
Reijo Jaakkola
CC BY-SA 4.0
2024-09-24T13:34:49.340Z
I see, good to know, thanks!
Antoine Amarilli 'a3nm'
CC BY-SA 4.0
2024-09-25T08:32:28.180Z
@a3nm Just noticed that I misread your comment. My comment concerns the search problem for finding a _minimum_ unsatisfiable core. I'm not sure what is the complexity of the search problem for finding a _minimal_ unsatisfiable core.
Reijo Jaakkola
CC BY-SA 4.0
2024-09-25T12:19:10.653Z
Oh I see. Indeed there are two dimensions: computation problem ("find a X") vs decision problem ("given k does there exist an X of size at most k"); and "minimum" vs "minimal". I think all 4 combinations make sense. I agree that your answer works for the decision problem phrasing of finding a minimum unsatisfiable core. I was also curious about the decision problem phrasing for finding a minimal unsatisfiable core.
Antoine Amarilli 'a3nm'
CC BY-SA 4.0
2024-09-24T11:39:08.520Z
2024-09-24T11:39:08.520Z
Reijo Jaakkola
<p>Given a Boolean formula <span class="math-container">$\phi$</span> in <a href="https://en.wikipedia.org/wiki/Conjunctive_normal_form" rel="noreferrer">conjunctive normal form</a> (CNF), an <em><a href="https://en.wikipedia.org/wiki/Unsatisfiable_core" rel="noreferrer">unsatisfiable core</a></em> of <span class="math-container">$\phi$</span> is a subset <span class="math-container">$\phi'$</span> of the clauses of <span class="math-container">$\phi$</span> which is unsatisfiable. We say that <span class="math-container">$\phi'$</span> is a <em>minimum unsatisfiable core</em> if its number of clauses <span class="math-container">$|\phi'|$</span> is minimum.</p>
<p>My question is about the complexity of computing a minimum unsatisfiable core, which I wasn't able to find in the literature. To make this a decision problem, say we receive as input a CNF <span class="math-container">$\phi$</span> and integer <span class="math-container">$k \in \mathbb{N}$</span>, and we must decide whether there exists an unsatisfiable core of <span class="math-container">$\phi$</span> containing at most <span class="math-container">$k$</span> clauses. <strong>What is the complexity of this problem?</strong> Is it known to be complete for some complexity class?</p>
<p>Of course this problem is at least coNP-hard, i.e., in the special case where <span class="math-container">$k = |\phi|$</span> the answer is true iff <span class="math-container">$\phi$</span> is unsatisfiable. The problem is even <a href="https://en.wikipedia.org/wiki/Boolean_hierarchy#Derived_classes" rel="noreferrer">DP</a>-hard because in the special case where <span class="math-container">$k = |\phi|-1$</span> we are asking whether <span class="math-container">$\phi$</span> is a so-called minimal unsatisfiable CNF, which is DP-complete by <a href="https://www.sciencedirect.com/science/article/pii/0022000088900426" rel="noreferrer">this paper</a>. My question is more to know what is a good upper bound. The naive algorithm would be to guess a subset <span class="math-container">$\phi'$</span>, and then check that it is unsatisfiable (i.e., there is no satisfying assignment), which I think is in <a href="https://en.wikipedia.org/wiki/Polynomial_hierarchy" rel="noreferrer"><span class="math-container">$\Sigma_2^P$</span></a>. But I don't know about hardness; for all I know the problem could be in DP for instance.</p>
<p>Some further notes about problem variants:</p>
<ul>
<li>Note that I am interested in <strong>minimum</strong> unsatisfiable cores. I am also unsure about the complexity of computing a <strong>minimal</strong> (for inclusion) unsatisfiable core but I think these can be found in <a href="https://en.wikipedia.org/wiki/Polynomial_hierarchy" rel="noreferrer"><span class="math-container">$\Delta_2^P$</span></a>, i.e., <span class="math-container">$\text{P}^{\text{NP}}$</span>, by iteratively removing clauses as long as the result is still unsatisfiable. I don't know about hardness. I'm also unsure about the problem of deciding, given <span class="math-container">$\phi$</span> and <span class="math-container">$\phi' \subseteq \phi$</span>, whether <span class="math-container">$\phi'$</span> is a minimum unsatisfiable core of <span class="math-container">$\phi$</span>. By contrast note that deciding if <span class="math-container">$\phi'$</span> is a <em>minimal</em> unsatisfiable core of <span class="math-container">$\phi$</span> is equivalent to checking whether <span class="math-container">$\phi'$</span> is minimal unsatisfiable, so it is DP-complete.</li>
<li>Alternatively I am also interested in other &quot;minimum violation&quot; type problems, e.g., given a graph <span class="math-container">$G$</span> and integer <span class="math-container">$k \in \mathbb{N}$</span>, does <span class="math-container">$G$</span> admit a subgraph of at most <span class="math-container">$k$</span> edges which is <em>not</em> <a href="https://en.wikipedia.org/wiki/Graph_coloring" rel="noreferrer">3-colorable</a>. Or, in the spirit of <a href="https://en.wikipedia.org/wiki/Constraint_satisfaction_problem" rel="noreferrer">constraint satisfaction problems</a>, fixing a right-hand-side structure <span class="math-container">$H$</span>, what is the complexity, given a structure <span class="math-container">$G$</span> and integer <span class="math-container">$k \in \mathbb{N}$</span>, of deciding whether there is a substructure of <span class="math-container">$G$</span> of size at most <span class="math-container">$k$</span> which does <em>not</em> map to <span class="math-container">$H$</span>. I also didn't find anything about the complexity of these problems.</li>
</ul>

<reference-request><sat><boolean-functions><boolean-formulas><minimization>
Complexity of computing minimum unsatisfiable core
Antoine Amarilli 'a3nm'
# Complexity of computing minimum unsatisfiable core

(Asked by: username_0 on 2024-09-24)

Given a Boolean formula $\phi$ in [conjunctive normal form](https://en.wikipedia.org/wiki/Conjunctive_normal_form) (CNF), an *[unsatisfiable core](https://en.wikipedia.org/wiki/Unsatisfiable_core)* of $\phi$ is a subset $\phi'$ of the clauses of $\phi$ which is unsatisfiable. We say that $\phi'$ is a *minimum unsatisfiable core* if its number of clauses $|\phi'|$ is minimum.

My question is about the complexity of computing a minimum unsatisfiable core, which I wasn't able to find in the literature. To make this a decision problem, say we receive as input a CNF $\phi$ and integer $k \in \mathbb{N}$, and we must decide whether there exists an unsatisfiable core of $\phi$ containing at most $k$ clauses. **What is the complexity of this problem?** Is it known to be complete for some complexity class?

Of course this problem is at least coNP-hard, i.e., in the special case where $k = |\phi|$ the answer is true iff $\phi$ is unsatisfiable. The problem is even [DP](https://en.wikipedia.org/wiki/Boolean_hierarchy#Derived_classes)-hard because in the special case where $k = |\phi|-1$ we are asking whether $\phi$ is a so-called minimal unsatisfiable CNF, which is DP-complete by [this paper](https://www.sciencedirect.com/science/article/pii/0022000088900426). My question is more to know what is a good upper bound. The naive algorithm would be to guess a subset $\phi'$, and then check that it is unsatisfiable (i.e., there is no satisfying assignment), which I think is in [$\Sigma\_2^P$](https://en.wikipedia.org/wiki/Polynomial_hierarchy). But I don't know about hardness; for all I know the problem could be in DP for instance.

Some further notes about problem variants:

* Note that I am interested in **minimum** unsatisfiable cores. I am also unsure about the complexity of computing a **minimal** (for inclusion) unsatisfiable core but I think these can be found in [$\Delta\_2^P$](https://en.wikipedia.org/wiki/Polynomial_hierarchy), i.e., $\text{P}^{\text{NP}}$, by iteratively removing clauses as long as the result is still unsatisfiable. I don't know about hardness. I'm also unsure about the problem of deciding, given $\phi$ and $\phi' \subseteq \phi$, whether $\phi'$ is a minimum unsatisfiable core of $\phi$. By contrast note that deciding if $\phi'$ is a *minimal* unsatisfiable core of $\phi$ is equivalent to checking whether $\phi'$ is minimal unsatisfiable, so it is DP-complete.
* Alternatively I am also interested in other "minimum violation" type problems, e.g., given a graph $G$ and integer $k \in \mathbb{N}$, does $G$ admit a subgraph of at most $k$ edges which is *not* [3-colorable](https://en.wikipedia.org/wiki/Graph_coloring). Or, in the spirit of [constraint satisfaction problems](https://en.wikipedia.org/wiki/Constraint_satisfaction_problem), fixing a right-hand-side structure $H$, what is the complexity, given a structure $G$ and integer $k \in \mathbb{N}$, of deciding whether there is a substructure of $G$ of size at most $k$ which does *not* map to $H$. I also didn't find anything about the complexity of these problems.

**Tags:** reference-request, sat, boolean-functions, boolean-formulas, minimization

---

## 1 answers

### Answer by username_1 on 2024-09-24. Score: 8 | Accepted answer

Umans proved that a problem that he calls "succinct set cover" is $\Sigma\_2^p$-complete [1]. In this problem we are given a DNF-formula with terms $T=\{t\_1,\dots,t\_m\}$ and a parameter $k$, the question being whether $T$ has a subset $T'$ of size at most $k$ such that $\bigvee T'$ is a tautology. Your problem should be equivalent with this problem by duality, so both are $\Sigma\_2^p$-complete.

[1] C. Umans. Hardness of Approximating Σp 2 Minimization Problems. In IEEE Symposium on Foundations of Computer Science (FOCS), pages 465–474, 1999.

> **Comments:**
> **username_0**: Thanks for your super quick and correct answer! I agree: asking for a minimum subset of clauses of a CNF which is unsat is equivalent to asking for a minimum subset of terms of the corresponding DNF which is tautological, so minimum unsatisfiable core is equivalent to that problem. Very nice. Out of curiosity do you happen to also know the complexity of computing a *minimal* unsatisfiable core?  
> **username_1**: @a3nm For this one I don't have a reference, but it should be complete for the class of search problems solvable in polynomial time with at most logarithmic number of calls to a $\Sigma_2^p$-witness oracle. Witness oracle means that the oracle not only gives you yes-no answer but also gives you the witness.  
> **username_0**: I see, good to know, thanks!  
> **username_1**: @a3nm Just noticed that I misread your comment. My comment concerns the search problem for finding a _minimum_ unsatisfiable core. I'm not sure what is the complexity of the search problem for finding a _minimal_ unsatisfiable core.  
> **username_0**: Oh I see. Indeed there are two dimensions: computation problem ("find a X") vs decision problem ("given k does there exist an X of size at most k"); and "minimum" vs "minimal". I think all 4 combinations make sense. I agree that your answer works for the decision problem phrasing of finding a minimum unsatisfiable core. I was also curious about the decision problem phrasing for finding a minimal unsatisfiable core.  

---

