Context: Kavvadias and Sideri have shown that the Inverse 3-SAT problem is coNP Complete: Given $\phi$ a set of models on $n$ variables, is there a 3-CNF formula such that $\phi$ is its exact set of models ? An immediate candidate formula arises which is the conjunction of all 3-clauses satisfied by all models in $\phi$.

Since it contains all 3-clauses it implies, this candidate formula can easily be transformed into an equivalent formula $F_{\phi}$ which is 3-closed under resolution - The 3-closure of a formula is the subset of its closure under resolution containing only clauses of size 3 or less. A CNF formula is closed under resolution if all possible resolvents are subsumed by a clause of the formula - a clause $c_1$ is subsumed by a clause $c_2$ if all literals of $c_2$ are in $c_1$.

Given $I$, a partial assignment of the variables such that $I$ is not a subset of any model of $\phi$.

Call $F_{\phi|I}$, the induced formula by applying $I$ to $F_{\phi}$: Any clause that contains a literal which evaluates to $true$ under $I$ is deleted from the formula and any literals that evaluate to $false$ under $I$ are deleted from all clauses.

Call $G_{\phi|I}$, the formula that derived from $F_{\phi|I}$ by all possible 3-limited resolutions (in which the resolvent and the operands have at most 3 literals) and subsumptions.

Question: Is $G_{\phi|I}$ 3-closed under resolution ?

• "P=NP"? from K&S fig1, "models" are analogous to bitvectors. the question needs to clearly determine how those models are represented (and maybe if restated in terms of satisfying bitvectors, the answer would be more obvious?). if solutions are represented as bitvectors then for some 3SAT formulas there are exponentially many satisfying bitvectors wrt the size of the formula. that is the expected "explosion in size". right? some other papers eg natural proofs also refer to the "truth table" of the formula which can be helpful in relating it to satisfying bitvectors.... – vzn Mar 19 '13 at 15:00
• Is it obvious that the third step can be computed efficiently? (Ie, deciding whether there exists a partial assignment $I$ not in $\phi$ such that $F_{\phi |I}$ does not contain the empty clause.) I must be missing something, but this isn't obvious to me. – Daniel Apon Mar 20 '13 at 15:09
• correction it is maybe more related to coNP=P? or possibly coNP=NP? not exactly sure. by the way this also reminds me a lot of dualization where models can be "represented" with DNF. see eg this ref on dualization by Bioch/Ibaraki – vzn Mar 20 '13 at 15:50
• @Daniel, IMHO yes, the third step can be computed efficiently as long as Step 1 and 2 can : as the set of partial assignments not in $\phi$ is bounded in size, it is easy to compute $F_{\phi|I}$ (for every $I$ not in $\phi$) and check whether the empty clause is in it. The possible bug would come about step 1 (I saw a bug which I am trying to fix it). – Xavier Labouze Mar 20 '13 at 16:11
• @XavierLabouze: a gave a quick look at the paper, just a note: the proof that $F_\phi$ can be calculated in polynomial time is not too clear (to me) – Marzio De Biasi Mar 20 '13 at 16:46

Answer : Yes (even if $I$ is a subset of some model of $\phi$)

Let $R_{|I}$ the set of clauses that derive from $F_{\phi} \cup F_{\phi|I}$ by all possible 3-limited resolutions and subsumptions ($R_{|I}$ is the 3-limited closure of $F_{\phi}\cup F_{\phi|I}$). Given $c$ a clause implied by $F_{\phi}$, it exists at least one subset of $R_{|I}$ whose clauses imply $c$. Name $R_c$ such a subset.

Let $P(k)$ the following property: For all $c$ implied by $F_{\phi}$ such that $|c_{|I}| \le 3$,

$[\exists R_c \subseteq R_{|I}$ such that $|R_c|\le k \Rightarrow c_{|I}$ is subsumed by some clause $\in G_{\phi|I}]$

Here does the recurrence begin. Given $c$ implied by $F_{\phi}$ such that $|c_{|I}|\le 3$, i.e. $c_{|I} \in$ the 3-closure of $F_{\phi|I}$.

1. $k=1$. If $\exists R_c \subseteq R_{|I} / |R_c|=1$ then $R_c=\{d\}$ ($d \in F_{\phi}\cup F_{\phi|I}$ subsumes $c$) and $c_{|I}$ is subsumed by $d_{|I} \in F_{\phi|I}$ (note that any clause of $F_{\phi|I}$ is subsumed by some clause of $G_{\phi|I}$). Thus $P(1)$.

2. Suppose $P(k)$ for $k\ge1$. If $\exists R_{c}\subseteq R_{|I}$ such that $|R_{c}|\le k+1$ (and no other $R_{c}$ of size 1 such that $c\notin F_{\phi}$ and $|c|>3$) then suppose $c=(\alpha \beta \gamma L_{I})$ where $\alpha ,\beta ,\gamma$ are literals not set by $I$ and $L_{I}$ is a subset of literals all evaluate to 0 under $I (L_I \neq \varnothing)$, i.e $c_{|I}=(\alpha \beta \gamma)$, with $\alpha ,\beta ,\gamma$ not necessarily different.

3. Remove a clause $d_{i}$ from $R_{c}$ such that $|d_{i|I}|<|d_{i}|\le3$, in other words, such that $d_{i}$ contains some literal from $L_{I}$ (there is at least one such clause in $R_{c}$ since $L_I \neq \varnothing$ ) and $|d_{i|I}|\leq 2$.

4. The size of the remaining set $R_{c}\setminus d_{i}$ is $\le k$. If a certain clause $c'=(\alpha \beta \gamma L'_{I})$ is implied by $R_{c}\setminus d_{i}$ (where $L'_{I}$ is a subset of literals all evaluate to 0 under $I$) then $|c'_{|I}|=3$ and $\exists R_{c'}=R_{c}\setminus d_{i}\subseteq R_{|I}$ such that $|R_{c'}|\le k$. By $P(k)$, $c'_{|I}=(\alpha \beta \gamma)$ is then subsumed by some clause $\in G_{\phi|I}$, inducing $P(k+1)$ for $c$.

5. If $d_{i|I}$ contains $\bar \alpha$ or $\bar \beta$ or $\bar \gamma$ then $d_{i|I}$ is useless to imply [some clause subsuming] $c$. Then $R_{c}\setminus d_{i}$ implies $c$, inducing $P(k+1)$ as shown previously.

6. If $d_{i|I}\in F_{\phi|I}$ subsumes $c_{|I}$ then $P(k+1)$ is satisfied for $c$.

7. If $d_{i|I}$ does not subsume $c_{|I}$ and does not contain $\bar \alpha$ or $\bar \beta$ or $\bar \gamma$ then either $d_{i|I}=(x)$ or $d_{i|I}=(ax)$ or $d_{i|I}=(xy)$, where $x$ and $y$ $\notin\{\alpha \beta \gamma \}$ and are not set by $I$, and $a \in\{\alpha \beta \gamma \}$.

• If $d_{i|I}=(x)$ then $R_{c}\setminus d_{i}$ implies $(\bar{x}\alpha \beta \gamma L_{I})$ (recall that implying a certain clause $C$ means implying a clause which subsumes $C$). Since any resolution with $d_{i|I}=(x)$ as operand removes $\bar{x}$ from the other operand then no clause of $R_{c}\setminus d_{i}$ contains $\bar x$ (since $R_{c}\setminus d_{i} \subseteq R_{|I}$ which is the 3-limited closure of $F_{\phi}\cup F_{\phi|I}$). Then $R_{c}\setminus d_{i}$ implies $(\alpha \beta \gamma L_{I})$, inducing $P(k+1)$ as shown in Point (4).
• If $d_{i|I}=(ax)$ then $R_{c}\setminus d_{i}$ implies $(\bar{x}\alpha \beta \gamma L_{I})$. Replace $\bar{x}$ by $a$ in each possible clause of $R_{c}\setminus d_{i}$ (if the new clause is subsumed by some clause in $R_{|I}$, keep the subsuming clause instead. Anyway, the replacing clause is in $R_{|I}$). Name $R_{c,d_{i}}$ the resulting set ($R_{c,d_{i}}\subseteq R_{|I}$). Then $R_{c,d_{i}}$ implies $(\alpha \beta \gamma L_{I})$, inducing $P(k+1)$ as above.

• If $d_{i|I}=(xy)$ then $R_{c}\setminus d_{i}$ implies $(\bar{x}\alpha \beta \gamma L_{I})$ and $(\bar{y}\alpha \beta \gamma L_{I})$. Replace $\bar{x}$ by $y$ in each possible clause of $R_{c}\setminus d_{i}$ (as above, if the new clause is subsumed by some clause in $R_{|I}$, keep the subsuming clause instead). Name $R_{c,d_{i}}$ the resulting set ($R_{c,d_{i}}\subseteq R_{|I}$). Then $R_{c,d_{i}}$ implies $({y}\alpha \beta \gamma L_{I})$. Since it implies also $(\bar{y}\alpha \beta \gamma L_{I})$ then it implies the resolvent $(\alpha \beta \gamma L_{I})$, inducing $P(k+1)$.

By this recurrence, any clause $\in$ the 3-closure of $F_{\phi |I}$ is subsumed by some clause $\in G_{\phi|I}$ (the other way holds as well). Then $G_{\phi|I}$ corresponds to the 3-closure of $F_{\phi |I}$.

I don't see how $F_\phi$ can be computed it in polynomial time becuase doing resolution itself takes exponential time (in the worst case). For example, let's say your candidate 3-CNF formula $F_1$ is as below: $$F_1 := \{ \{a, b, c\}, \{d, e, \neg c\}, \{a, \neg b, f\}, \{d, e, \neg f\}\}$$ Then, the result of resolution on $F_1$ is the formula $F_2$ below: $$F_2 := \{ \{a, b, c\}, \{d, e, \neg c\}, \{a, \neg b, f\}, \{d, e, \neg f\}, \{a,b,d,e\}, \{a,\neg b, d, e\}, \{a,d,e\}\}$$ Thus, the formula $F_\phi$ is as below: $$F_\phi :=\{\{a, b, c\}, \{d, e, \neg c\}, \{a, \neg b, f\}, \{d, e, \neg f\}, \{a,d,e\}\}$$

However, as you can see, in order to get the final clause in $F_\phi$ you should first get all four-literal clauses. So, I do not see any way to get rid of exponentially many steps for resolution. Indeed, for some problems such as the pigeonhole principle, we know that resolution cannot solve it in less than exponentially many steps (but, to be fair, as far as I know, these examples are not in 3-CNF form and some intelligent resolution might exist when the input is guaranteed to be in 3-CNF form).

• Thank you for your answer - $F_1$ cannot be a candidate formula as defined : since the candidate formula is the conjunction of all 3-clauses satisfied by all models in $\phi$, it must contain all 3-clauses it implies. – Xavier Labouze May 4 '13 at 10:14