3-SAT runtime if an optimal order to eliminate possible solutions is known

Question

As a mental exercise I have been playing around with the 3-SAT problem, but I am having difficulty proving or disproving the usefulness of a current idea that I am playing around with.

My current exploration of the problem was based off of the question: Would it be possible to create an algorithm for 3-SAT that has a runtime which is polynomial with the input size and the number of accepting solutions? (Probably not, but it makes for an interesting exercise.)

It is obvious that, if such an algorithm existed, then 3-SAT could be solvable by using the input size to compute the maximum number of steps the algorithm would run assuming that the input was not satisfiable (guaranteed to be polynomial with the input size, because the number of accepting solutions would be 0) and running the algorithm for that many steps. If the algorithm had not rejected by that point, then the input can be accepted because we know the algorithm will not reject at all.

As a first attempt at this, I have defined a datatype SatisfactionSet which contains the following:

• A list of the clauses that must be satisfied by every possible solution in the set
• A set of the variables that are covered by the SatisfactionSet. Every variable must appear in at least one of the clauses listed and if a variable appears in one of the clauses it must appear here.
• A list containing all possible assignments of the variables in the above set that would satisfy the listed clauses. In other words, if the above set contains m variables, this list would contain at most 2^m assignments and every one of them must be able to satisfy all clauses

Two SatisfactionSets can be joined by concatenating their lists of clauses, taking the union of their variable sets, and iterating through to match each assignment from the first SatisfactionSet with as many compatible assignments from the second SatisfactionSet as possible. Every matching of assignments takes the union of the two assignments and makes it into an assignment in the joined SatisfactionSet.

The object produced by joining two SatisfactionSets always replaces the two objects being joined in the list of all SatisfactionSets.

Two SatisfactionSets are only eligible to be joined if their variable sets have at least one variable in common.

Our algorithm initializes by creating one SatisfactionSet for each clause in the input.

If a SatisfactionSet is ever created (either initially or by joining) that has an empty list of satisfying assignments, then our algorithm rejects the input, saying that it is not satisfiable.

Our algorithm runs until it either rejects or there are no remaining pairs of SatisfactionSets that are eligible to be joined together. If there are no remaining pairs eligible to be joined and we haven't rejected, we accept.

I will not go into a proof of correctness here, but it is not too hard to show that this will correctly solve the 3-SAT problem. So now we begin work on trying to bring the runtime into a polynomial bound based on the input size and the number of satisfying solutions (or at least polynomial if there is no satisfying assignment).

Setting aside the issue of maintaining a list of valid join operations (since that can be done in polynomial time per join with just a little tweaking to the setup), it is readily apparent that the runtime of the algorithm can be encapsulated by observing the total number of unique assignments/assignment parts discovered by all of the SatisfactionSets over the duration of the algorithm. Therefore, we will let a variable C represent this total.

This is where I would like assistance. I would like to perform a sanity check on this approach.

Suppose we have a polynomial time algorithm A which, for any input, will produce an optimal ordering of join operations such that following them will take our algorithm from initialization to termination and C will be minimal.

We will represent the value of C obtained when running our algorithm on input x using the ordering provided by A as C_A(x)

The sanity check is thus:

I would like to prove or disprove that for any non-satisfiable input x, the value of C_A(x) is polynomial to the input size.

More formally:

I would like to prove or disprove that there exists a fixed polynomial function f of the input size, as well as a base input size n_0, such that, for all inputs x such that |x|>=n_0, x not being satisfiable implies that C_A(x)<=f(|x|).

Any help or insight that could be provided on this would be greatly appreciated. Additionally, if it would simplify the proof, I do not mind if variations of 3-SAT are used instead so long as following conditions hold for the variations used:

1. The variation is still a recognizable and valid variation of 3-SAT (i.e. You can't use SAT with a single really large clause that covers most variables right at the start as a disproof. It would not be recognized as a valid instance of 3-SAT.)
2. The variation can still be correctly solved using the algorithm described above.
3. The variation is still NP-complete.

For instance, the 3-SAT variant where each literal can appear at most two times would be a valid variant to use instead.

Answer 1

If I understand the question correctly, the answer is no.

Theorem 1. There is an infinite family $\{\phi'_n\}_n$ of unsatisfiable 3CNF formulas such that, for each instance $\phi'_n$, any execution of the algorithm in the post constructs intermediate assignments whose total size is exponential in the size of $\phi'_n$.

Proof sketch. Fix arbitrarily large integer $n\ge 1$. Define conjunctive Boolean formula $\phi_n$ with $n+1$ "iff" clauses as follows: $$\phi_n \,=\, \big(z \iff (x_1 \vee y_1)\big) \wedge \big(\forall_{i\in [n-1]}(x_i\vee y_i) \iff (x_{i+1}\vee y_{i+1}) \big) \wedge \big((x_n \vee y_n) \iff \overline {z}\big).$$

(This formula is not in 3CNF form. We'll correct that later.) Note that $\phi_n$ is not satisfiable, as it logically implies $z \iff \overline z$.

Consider any proper subset $C$ of the "iff" clauses in $\phi_n$. We claim that there are exponentially (in $|C|$) many distinct assignments to the variables in $C$ that satisfy all clauses in $C$. (Indeed, let $I$ denote the set of indices $i$ such that some variable $x_i$ or $y_i$ or its negation is mentioned in a clause in $C$. Fix a $j$ such that the $j$th clause is not in $C$. First consider the case that at least half of the clauses in $C$ occur before clause $j$ in $\phi_n$. In this case, we can (i) assign $z$ true, (ii) for each $i\le j$ (with $i\in I$) assign each $x_i$ arbitrarily true or false and assign $y_i = \lnot x_i$, and (iii) for each $i>j$ (with $i\in I$) assign $x_i$ and $y_i$ false. This gives us at least $2^{|C|/2}$ distinct assignments to the variables mentioned in $C$ that satisfy all clauses in $C$. For the remaining case, reverse the order: (i) assign $z$ false, (ii) for each $i>j$ (with $i\in I$) assign each $x_i$ arbitrarily true or false and assign $y_i = \lnot x_i$, and (iii) for each $i\le j$ (with $i\in I$) assign $x_i$ and $y_i$ false.)

Next consider running the algorithm on input $\phi_n$ (with the $n+1$ "iff" clauses as the initial solution sets, ignoring for now that $\phi_n$ is not in 3CNF form). Each iteration chooses some two solution sets and replaces them by their union. It follows that (just before termination) the algorithm would have to have a solution set containing at least $n/2$ clauses, but not all of the clauses. Taking $C$ to be the set of those clauses, we have $|C| \ge n/2$, and by the previous paragraph exponentially many (at least $2^{n/4}$) of the assignments to the variables of $C$ satisfy all the clauses in $C$, as desired.

This does not complete the proof, because $\phi_n$ is not in 3CNF form, so is not in fact a valid input for the algorithm. To finish the proof, we show that essentially the same argument works for the 3CNF formula $\phi'_n$ obtained by converting $\phi_n$ into 3CNF form in the standard way. That is, we replace each "iff" clause by an equivalent group of up to four 3CNF clauses, as follows:

1. Replace $z \iff (x_1\vee y_1)$ by the equivalent group of three clauses $$(z \vee \overline{x_1})\wedge(z\vee\overline{y_1}) \wedge(\overline{z}\vee x_1\vee y_1),$$ and likewise replace $(x_n\vee y_n) \iff \overline z$ by $(\overline z \vee \overline{x_1})\wedge(\overline z\vee\overline{y_1}) \wedge(z\vee x_1\vee y_1)$
2. For each $i\in[n-1]$, replace $(x_i\vee y_i)\iff (x_{i+1} \vee y_{i+1})$ by the equivalent group of four clauses $$(\overline x_i \vee x_{i+1} \vee y_{i+1}) \wedge (\overline y_i \vee x_{i+1} \vee y_{i+1}) \wedge (x_{i} \vee y_i \vee \overline{x_{i+1}}) \wedge (x_{i} \vee y_i \vee \overline{y_{i+1}}).)$$

Note that $\phi'_n$ has the same variables as $\phi_n$, and that any assignment to those variables satisfies a given "iff" clause in $\phi'_n$ if and only if it satisfies the associated group of clauses in $\phi_n$.

Now consider executing the algorithm in the post on $\phi'_n$. Consider the first iteration in which the algorithm has a "solution set" containing at least one clause from each of the $n+1$ "clause groups" in $\phi'_n$. This solution set was formed as the union of two solution sets. Let $S'$ be whichever has clauses from the most clause groups. Then $S'$ has clauses from at least $n/2$ clause groups in $\phi'_n$, but not from every clause group. Note that each clause associated with the $j$th clause group ($2\le j \le n$) mentions $x$ and/or $y$ variables with indices $j-1$ and $j$. By the previous argument, there are at least $n/4$ indices $i$ such that $x_i$ or $y_i$ is mentioned in $S'$, and we can assign $x_i$ arbitrarily and $y_i = \lnot x_i$, giving at least $2^{n/4}$ distinct assignments that satisfy all clauses in $S'$, as desired. $~~~\Box$