Is there an Upper Bound on Number of Redundant Clauses in a satisfiable $3-SAT$?

Question

For a non-empty $3-SAT$ with $n\geq3$ variables and $T\geq1$ non-identical non-degenerate clauses $C_i$: $$S=C_1 \wedge \ldots \wedge C_T$$ where a non-degenerate clause is one containing $3$ unique literals (no clauses like $a\vee a\vee b$, etc.)

It is clear that there are $2^3 \cdot \binom{n}{3}\geq T$ possible $C_i$ to choose from. Additionally when $n=3$ there are no possible redundant clauses.

This is not true for $n=4$, here is an example: $$\begin{split} &(x_4\vee x_2\vee x_3)\wedge(\overline{x}_4\vee x_2\vee x_3)\wedge(x_1\vee x_4\vee x_3)\wedge(x_1\vee \overline{x}_4\vee x_3)\\ \wedge&(x_1\vee x_2\vee x_4)\wedge(x_1\vee x_2\vee \overline{x}_4)\wedge(x_1\vee x_2\vee x_3) \end{split} $$ The last clause here is redundant, since removing it from the $SAT$ instance would have no effect on the satisfying assignments.

For an unsatisfiable instance, clearly the upper bound on redundant clauses is: $T-2^3$

Given these constraints, does anyone see a path towards figuring out the maximum number of possible redundant clauses in a satisfiable instance, for a given $n$ and $T$?

Answer 1

I interpret the question as: given $n$ and $T$, what is the maximum number of redundant clauses a satisfiable $n$-variable formula on $T$ clauses can have? For the purposes of this question, I find it helpful to phrase this as: Find (lower bounds on) $f(n,m)$ such that an $n$-variable $m$-clause formula may imply $f(n,m)$ clauses (that may or may not be in the formula). I answer the question by giving, in two constructions, my "best attempt" formulas, which try to keep $m$ as small as possible, but make $f$ as large as possible. I find that $f(n,\mathcal O(n))=\Theta(n^3)$, i.e., only a linear number of clauses suffices to obtain the maximum possible number of implied clauses. A consequence is that, in the extreme case, all clauses except a $\mathcal O(\frac{1}{n^2})$ fraction is redundant. This non-redundant part that you are after, is usually called the unsatisfiable core when the formula is unsatisfiable, which will yield you many results if you search the literature.

1. $f(n,2(n-2))\geq 3\binom{n-1}{2}=\Omega(n^2)$. Construction: consider the formula with clauses $(x_1\vee x_2\vee x_i)$ and $(\neg x_1\vee x_2\vee x_i)$ for $i=3\ldots n$. This implies all clauses $(x_2\vee x_i)$, so it also implies the clause $(x_2\vee \pm x_i\vee \pm x_j)$, except not the clause $(x_2\vee \neg x_i\vee \neg x_j)$, for each $(i,j)$ with $1\leq i<j\leq n$. There are $3\binom{n-1}2$ such clauses.

2. $f(n, \frac{7}{3}n)= 7\binom n3=\Omega(n^3)$. Construction: consider the formula with the $7$ clauses $(\pm x_{i}\vee \pm x_{i+1}\vee \pm x_{i+2})$ except the all-negative clause $(\neg x_i\vee \neg x_{i+1}\vee \neg x_{i+2})$, for $i=1,4,7,\ldots,n-2$. This formula implies all literals $x_i=1$, so it has exactly one satisfying assignment, $x=(1,\ldots, 1)$. It therefeore also implies all clauses that have at least one positive literal in it, of which there are $7\binom n3$. A consequence: for $\alpha\leq \frac{7}{3}$, we have $f(n,\alpha n)=\Omega(n^{\frac{9}{7}\alpha})$, which is better than Construction 1, since we get $f(n,2n)=\Omega(n^{2\frac{4}{7}})$.

Does $f$ have a phase transition between $m=2n$ and $m=2\frac{1}{3}n$, where it goes from $f=\Omega(n^{2\frac{4}{7}})$ to $f=\Omega(n^3)$? Are these constructions optimal? I hope that someone can answer who is more familiar with the literature.

---

The flipside of your question (my previous interpretation): given a satisfiable formula on $n$ variables and $T$ clauses, when may I conclude, based only on $n$ and $T$, that at least some number of the clauses are redundant?

I find this a difficult combinatorial question. Perhaps the literature contains the answer; I hope somebody can add it here.

Here is a lower bound. Consider the formula with all $T=\binom n3$ all-positive clauses. This is a redundancy-free formula, since removing, e.g., the clause $(x_1\vee x_2\vee x_3)$ now allows the satisfying assignment $x=(0,0,0,1,\ldots, 1)$ (the definition of redundant was that removing it preserved the set of satisfying assignments). All the other clauses behave similarly. Is this the largest redundancy-free formula?

Answer 2

Theorem 1. For all $n\ge 6$ and $T$ with $n+14\le T \le 7{n\choose 3}$, there is a satisfiable 3-SAT formula on $n$ variables with $T$ clauses in which all clauses are redundant.

Before we give the proof, note that $7{n\choose 3}$ is an upper bound on the number of clauses in any satisfiable 3-CNF formula. In the case $T=7{n\choose 3}$ the theorem implies that the formula on $n$ variables obtained by anding together all 3-CNF clauses containing at least one positive literal is uniquely satisfied by setting all variables true, and all of its clauses are redundant.

Proof of Theorem 1.

1. Let $\mu(x_1, x_2, x_3)$ be the 3-CNF formula with 3 variables that contains all 3-CNF clauses except $\overline x_1 \vee \overline x_2 \vee \overline x_3$. Then $\mu(x_1, x_2, x_3)$ is uniquely satisfied by setting all variables true. The formula $\mu$ has seven clauses.

2. Now for $x=(x_1, x_2, x_3)$ and $z=(z_1, z_2, \ldots, z_{n'})$ define $$\alpha(x, z) = (z_1 \vee \overline{x_1} \vee \overline{x_2})\wedge (z_2 \vee \overline{x_1} \vee \overline{x_2}) \wedge \cdots \wedge (z_{n'} \vee \overline{x_1} \vee \overline{x_2})$$ and $$\beta(x, z) = \mu(x) \wedge \alpha(x, z).$$

3. Note that $\beta(x, z)$ is uniquely satisfied by setting all its variables true.

4. Case 1. First consider the case that $T \ge 14 + 2n$.

5. For $x=(x_1, x_2, x_3)$, $y=(y_1, y_2, y_3)$, and $z=(z_1, \ldots, z_{n'})$ where $n'=n-6$, define $$\phi(x, y, z) = \beta(x, y) \wedge \beta(y, x) \wedge \alpha(x, z) \wedge \alpha(y, z).$$

6. By inspection the clauses in $\phi(x, y, z)$ are all distinct. By Step 3 above $\phi(x, y, z)$ is uniquely satisfied by setting all variables true.

7. Every clause in $\phi(x, y, z)$ is redundant. (Indeed, for any three of the four subformulas in the definition of $\phi$ to be satisfied, all variables in $(x, y, z)$ must be true. This follows from the same reasoning as for Step 3.)

8. Then $\phi(x, y, z)$ has $6+n'=n$ variables and $14+2n \le T$ clauses.

9. Now pad $\phi$ by adding $T-14-2n$ clauses of the form $(u\vee v\vee w)$ where $u$, $v$, and $w$ are any of the $2n$ literals and at least one literal is positive. There are $7{n \choose 3}$ such clauses, $14+2n$ of which already occur in $\phi$ --- avoid those. All added clauses are redundant. This concludes the proof for Case 1.

10. Case 2. Now consider the remaining case: $n + 14\le T < 14+2n$.

11. For $x=(x_1, x_2, x_3)$, $y=(y_1, y_2, y_3)$, and $z=(z_1, \ldots, z_{n'})$ where $n'=n-6$, define $\psi(x, y, z)$ to be the "and" of the following two subformulae:

$$\beta(x, y) \wedge \beta(y, x)$$ $$(x_1 \vee z_1 \vee z_2) \wedge(x_1 \vee z_2 \vee z_3) \wedge \cdots \wedge (x_1 \vee z_{n'-1} \vee z_{n'}) \wedge (x_1 \vee z_{n'} \vee z_1).$$

12. By inspection the clauses in $\psi(x, y, z)$ are all distinct. The satisfying assignments to $\phi(x, y, z)$ are those that set variables in $x$ and $y$ true, and variables in $z$ arbitrarily.

13. Every clause in $\psi(x, y, z)$ is redundant. (The reasoning is as in Case 1, except that here the assignment to $z$ is unconstrained and remains unconstrained upon removal of any clause.)

14. And $\psi(x, y, z)$ has $6+n'=n$ variables and $14+n \le T$ clauses.

15. Now pad $\psi$ by adding $T-14-n < n$ new clauses of the form $(x_1 \vee \overline{z_i}\vee \overline{z_{i+1}})$ where $i<n$. All added clauses are redundant. This concludes the proof for Case 2. $~~~\Box$

Note that we could weaken the assumption $T \ge n+14$ to something like $T \ge n/2+14$ if we are allowed to use variables that occur only once. (But in that case the notion of redundancy is unclear, because deleting the sole clause that contains a given variable removes the variable from the formula.)