Return to 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$.

Call $F_{\phi|I}$, the induced formula by applying any partial assignment $I$ of the variables 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 ?

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 ?

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

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

Call $F_{\phi|I}$, the induced formula by applying any partial assignment $I$ of the variables 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 ?

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

Call $F_{\phi|I}$, the induced formula by applying any partial assignment $I$ of the variables 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 ?

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

The 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$. (see About Inverse 3-SAT for details).

Call $F_{\phi|I}$, the induced formula by applying any partial assignment $I$ of the variables 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 (all subsumed clauses are deleted from the formula).

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

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

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

Call $F_{\phi|I}$, the induced formula by applying any partial assignment $I$ of the variables 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 ?