About Inverse 3-SAT

Question

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 ?

Answer 1

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