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

<p>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.</p>

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

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

<p>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}$.</p>

<ol>
<li><p>$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)$.</p></li>
<li><p>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|&gt;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.  </p></li>
<li><p>Remove a clause $d_{i}$ from $R_{c}$ such that $|d_{i|I}|&lt;|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$. </p></li>
<li><p>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$.</p></li>
<li><p>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.</p></li>
<li><p>If $d_{i|I}\in F_{\phi|I}$ subsumes $c_{|I}$ then $P(k+1)$ is satisfied for $c$. </p></li>
<li><p>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 \}$.</p>

<ul>
<li>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). </li>
<li><p>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.</p></li>
<li><p>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)$.</p></li>
</ul></li>
</ol>

<p>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}$.</p>

CC BY-SA 3.0
2013-08-18T13:43:53.980Z
2013-08-27T16:04:33.950Z
2013-08-27T16:04:33.950Z
Xavier Labouze
<p>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\}\}
$$</p>

<p>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).</p>

CC BY-SA 3.0
2013-05-04T10:14:23.120Z
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
CC BY-SA 3.0
2013-05-04T09:16:21.930Z
2013-05-04T09:16:21.930Z
Shahab
<p><strong>Context</strong>: <a href="http://lca.ceid.upatras.gr/courses/sttcc/papers/Inverse_SAT.pdf" rel="nofollow">Kavvadias and Sideri</a> 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$. </p>

<p>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$.</p>

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

<p>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.</p>

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

<p><strong>Question</strong>: Is $G_{\phi|I}$ 3-closed under resolution ?</p>

CC BY-SA 3.0
2013-03-19T15:00:11.097Z
"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
CC BY-SA 3.0
2013-03-20T15:09:20.893Z
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
CC BY-SA 3.0
2013-03-20T15:50:09.413Z
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](http://www.sciencedirect.com/science/article/pii/S0890540185711571) on dualization by Bioch/Ibaraki
vzn
CC BY-SA 3.0
2013-03-20T16:11:33.197Z
@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
CC BY-SA 3.0
2013-03-20T16:46:06.350Z
@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
CC BY-SA 3.0
2013-03-20T17:58:44.820Z
@MarzioDeBiasi , another way of thinking the proof is to consider a resolvent of size 2 comes from two clauses $(abx)$ and $(ab\bar x)$, easy to compute (all resolvents of size 3 are already in the formula, no need to compute them).
Xavier Labouze
CC BY-SA 3.0
2013-05-14T00:58:58.797Z
@Xavier, making too many insignificant edits is not nice. If you want to draw attention to your question you can offer a bounty.
Kaveh
CC BY-SA 3.0
2013-05-14T04:55:57.873Z
@Kaveh, Tks for the idea of bounty, I haven't thought of it -
Xavier Labouze
<cc.complexity-theory><lo.logic><complexity-classes><computability><sat>
About Inverse 3-SAT
Xavier Labouze
# About Inverse 3-SAT

(Asked by: username_0 on 2013-03-19)

**Context**: [Kavvadias and Sideri](http://lca.ceid.upatras.gr/courses/sttcc/papers/Inverse_SAT.pdf) 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 ?

**Tags:** cc.complexity-theory, lo.logic, complexity-classes, computability, sat

> **Comments:**
> **username_1**: "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....  
> **username_2**: 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.  
> **username_1**: 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](http://www.sciencedirect.com/science/article/pii/S0890540185711571) on dualization by Bioch/Ibaraki  
> **username_0**: @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).  
> **username_3**: @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)  
> **username_0**: @MarzioDeBiasi , another way of thinking the proof is to consider a resolvent of size 2 comes from two clauses $(abx)$ and $(ab\bar x)$, easy to compute (all resolvents of size 3 are already in the formula, no need to compute them).  
> **username_4**: @Xavier, making too many insignificant edits is not nice. If you want to draw attention to your question you can offer a bounty.  
> **username_0**: @username_4, Tks for the idea of bounty, I haven't thought of it -  

---

## 2 answers

### Answer by username_0 on 2013-08-18. Score: 3

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}$.


---

### Answer by username_5 on 2013-05-04. Score: -2

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).

> **Comments:**
> **username_0**: 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.  

---

