<p>If I understand the question correctly, the answer is no.</p>
<p><strong>Theorem 1.</strong> <em>There is an infinite family <span class="math-container">$\{\phi'_n\}_n$</span> of unsatisfiable 3CNF formulas such that, for each instance <span class="math-container">$\phi'_n$</span>, any execution of the algorithm in the post constructs intermediate assignments whose total size is exponential in the size of <span class="math-container">$\phi'_n$</span>.</em></p>
<p><em>Proof sketch.</em>
Fix arbitrarily large integer <span class="math-container">$n\ge 1$</span>.
Define conjunctive Boolean formula
<span class="math-container">$\phi_n$</span> with <span class="math-container">$n+1$</span> &quot;iff&quot; clauses as follows:
<span class="math-container">$$\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).$$</span></p>
<p>(This formula is not in 3CNF form.  We'll correct that later.)
Note that <span class="math-container">$\phi_n$</span> is not satisfiable,
as it logically implies <span class="math-container">$z \iff \overline z$</span>.</p>
<p>Consider any proper subset <span class="math-container">$C$</span> of the &quot;iff&quot; clauses in <span class="math-container">$\phi_n$</span>.
We claim that <em>there are exponentially (in <span class="math-container">$|C|$</span>) many distinct assignments to the variables in <span class="math-container">$C$</span>
that satisfy all clauses in <span class="math-container">$C$</span>.</em>
(Indeed, let <span class="math-container">$I$</span> denote the set of indices <span class="math-container">$i$</span> such that
some variable <span class="math-container">$x_i$</span> or <span class="math-container">$y_i$</span> or its negation is mentioned in
a clause in <span class="math-container">$C$</span>.
Fix a <span class="math-container">$j$</span> such that the <span class="math-container">$j$</span>th clause is not in <span class="math-container">$C$</span>.
First consider the case that at least half of the clauses in <span class="math-container">$C$</span>
occur before clause <span class="math-container">$j$</span> in <span class="math-container">$\phi_n$</span>.
In this case, we can (i) assign <span class="math-container">$z$</span> true,
(ii) for each <span class="math-container">$i\le j$</span> (with <span class="math-container">$i\in I$</span>)
assign each <span class="math-container">$x_i$</span> arbitrarily true or false
and assign <span class="math-container">$y_i = \lnot x_i$</span>,
and (iii) for each <span class="math-container">$i&gt;j$</span> (with <span class="math-container">$i\in I$</span>)
assign <span class="math-container">$x_i$</span> and <span class="math-container">$y_i$</span> false.
This gives us at least <span class="math-container">$2^{|C|/2}$</span> distinct assignments
to the variables mentioned in <span class="math-container">$C$</span>
that satisfy all clauses in <span class="math-container">$C$</span>.
For the remaining case, reverse the order:
(i) assign <span class="math-container">$z$</span> false,
(ii) for each <span class="math-container">$i&gt;j$</span> (with <span class="math-container">$i\in I$</span>)
assign each <span class="math-container">$x_i$</span> arbitrarily true or false
and assign <span class="math-container">$y_i = \lnot x_i$</span>,
and (iii) for each <span class="math-container">$i\le j$</span> (with <span class="math-container">$i\in I$</span>)
assign <span class="math-container">$x_i$</span> and <span class="math-container">$y_i$</span> false.)</p>
<p>Next consider running the algorithm on input <span class="math-container">$\phi_n$</span>
(with the <span class="math-container">$n+1$</span> &quot;iff&quot; clauses as the initial solution sets,
ignoring for now that <span class="math-container">$\phi_n$</span> 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 <span class="math-container">$n/2$</span> clauses, but not all of the clauses.
Taking <span class="math-container">$C$</span> to be the set of those clauses,
we have <span class="math-container">$|C| \ge n/2$</span>,
and by the previous paragraph
exponentially many (at least <span class="math-container">$2^{n/4}$</span>) of the assignments
to the variables of <span class="math-container">$C$</span> satisfy all the clauses in <span class="math-container">$C$</span>,
as desired.</p>
<p>This does not complete the proof, because <span class="math-container">$\phi_n$</span> 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 <span class="math-container">$\phi'_n$</span> obtained by converting <span class="math-container">$\phi_n$</span>
into 3CNF form in the standard way. That is, we replace each &quot;iff&quot; clause by an equivalent group of up to four 3CNF clauses, as follows:</p>
<ol>
<li>Replace <span class="math-container">$z \iff (x_1\vee y_1)$</span> by the equivalent group of three clauses
<span class="math-container">$$(z \vee \overline{x_1})\wedge(z\vee\overline{y_1})
\wedge(\overline{z}\vee x_1\vee y_1),$$</span>
and likewise replace <span class="math-container">$(x_n\vee y_n) \iff \overline z$</span>
by
<span class="math-container">$(\overline z \vee \overline{x_1})\wedge(\overline z\vee\overline{y_1})
\wedge(z\vee x_1\vee y_1)$</span></li>
<li>For each <span class="math-container">$i\in[n-1]$</span>, replace
<span class="math-container">$(x_i\vee y_i)\iff (x_{i+1} \vee y_{i+1})$</span> by the equivalent group of four clauses
<span class="math-container">$$(\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}}).)$$</span></li>
</ol>
<p>Note that <span class="math-container">$\phi'_n$</span> has the same variables as <span class="math-container">$\phi_n$</span>, and that any assignment to those variables satisfies a given &quot;iff&quot; clause in <span class="math-container">$\phi'_n$</span> if and only if it satisfies the associated group of clauses in <span class="math-container">$\phi_n$</span>.</p>
<p>Now consider executing the algorithm in the post on <span class="math-container">$\phi'_n$</span>.  Consider the first iteration in which the algorithm has a &quot;solution set&quot; containing at least one clause from each of the <span class="math-container">$n+1$</span> &quot;clause groups&quot; in <span class="math-container">$\phi'_n$</span>.  This solution set was formed as the union of two solution sets. Let <span class="math-container">$S'$</span> be whichever has clauses from the most clause groups.  Then <span class="math-container">$S'$</span> has clauses from at least <span class="math-container">$n/2$</span> clause groups in <span class="math-container">$\phi'_n$</span>, but not from every clause group.  Note that each clause associated with the <span class="math-container">$j$</span>th clause group (<span class="math-container">$2\le j \le n$</span>) mentions <span class="math-container">$x$</span> and/or <span class="math-container">$y$</span> variables with indices <span class="math-container">$j-1$</span> and <span class="math-container">$j$</span>.
By the previous argument, there are at least <span class="math-container">$n/4$</span> indices <span class="math-container">$i$</span>
such that <span class="math-container">$x_i$</span> or <span class="math-container">$y_i$</span> is mentioned in <span class="math-container">$S'$</span>,
and we can assign <span class="math-container">$x_i$</span> arbitrarily and <span class="math-container">$y_i = \lnot x_i$</span>,
giving at least <span class="math-container">$2^{n/4}$</span> distinct assignments
that satisfy all clauses in <span class="math-container">$S'$</span>, as desired.
<span class="math-container">$~~~\Box$</span></p>

CC BY-SA 4.0
2021-12-13T01:21:37.103Z
2021-12-13T01:21:37.103Z
Neal Young
<p>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.</p>
<p>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.)</p>
<p>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.</p>
<p>As a first attempt at this, I have defined a datatype <code>SatisfactionSet</code> which contains the following:</p>
<ul>
<li>A list of the clauses that must be satisfied by every possible solution in the set</li>
<li>A set of the variables that are covered by the <code>SatisfactionSet</code>. 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.</li>
<li>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 <code>m</code> variables, this list would contain at most <code>2^m</code> assignments and every one of them must be able to satisfy all clauses</li>
</ul>
<p>Two <code>SatisfactionSets</code> 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 <code>SatisfactionSet</code> with as many compatible assignments from the second <code>SatisfactionSet</code> as possible. Every matching of assignments takes the union of the two assignments and makes it into an assignment in the joined <code>SatisfactionSet</code>.</p>
<p>The object produced by joining two <code>SatisfactionSets</code> always replaces the two objects being joined in the list of all <code>SatisfactionSets</code>.</p>
<p>Two <code>SatisfactionSets</code> are only eligible to be joined if their variable sets have at least one variable in common.</p>
<p>Our algorithm initializes by creating one <code>SatisfactionSet</code> for each clause in the input.</p>
<p>If a <code>SatisfactionSet</code> 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.</p>
<p>Our algorithm runs until it either rejects or there are no remaining pairs of <code>SatisfactionSets</code> that are eligible to be joined together. If there are no remaining pairs eligible to be joined and we haven't rejected, we accept.</p>
<p>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).</p>
<p>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 <code>SatisfactionSets</code> over the duration of the algorithm. Therefore, we will let a variable <code>C</code> represent this total.</p>
<p>This is where I would like assistance. I would like to perform a sanity check on this approach.</p>
<p>Suppose we have a polynomial time algorithm <code>A</code> 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 <code>C</code> will be minimal.</p>
<p>We will represent the value of <code>C</code> obtained when running our algorithm on input <code>x</code> using the ordering provided by <code>A</code> as <code>C_A(x)</code></p>
<p>The sanity check is thus:</p>
<p>I would like to prove or disprove that for any non-satisfiable input <code>x</code>, the value of <code>C_A(x)</code> is polynomial to the input size.</p>
<p>More formally:</p>
<p>I would like to prove or disprove that there exists a fixed polynomial function <code>f</code> of the input size, as well as a base input size n_0, such that, for all inputs <code>x</code> such that <code>|x|&gt;=n_0</code>, <code>x</code> not being satisfiable implies that <code>C_A(x)&lt;=f(|x|)</code>.</p>
<p>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:</p>
<ol>
<li>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.)</li>
<li>The variation can still be correctly solved using the algorithm described above.</li>
<li>The variation is still NP-complete.</li>
</ol>
<p>For instance, the 3-SAT variant where each literal can appear at most two times would be a valid variant to use instead.</p>

CC BY-SA 4.0
2021-12-11T20:17:31.470Z
*"polynomial with the input size and the number of accepting solutions"*... Just a quick note: Unambiguous-SAT (CNF-SAT with the promise that there is at most one satisfying solution) is hard for NP under randomized reductions ([https://en.wikipedia.org/wiki/Valiant–Vazirani_theorem](https://en.wikipedia.org/wiki/Valiant–Vazirani_theorem)).  So, in the worst case, SAT formulas with just one satisfying solution are not easier to solve.
Neal Young
CC BY-SA 4.0
2021-12-12T01:16:06.063Z
@Neal Young I am under no delusions that the problem I am looking at is any less hard than any other np-complete problem. I myself outlined a way to solve general 3-SAT in polynomial time if such a solution existed. Like I said, it is a mental exercise.
Timothy Schommer
CC BY-SA 4.0
2021-12-12T02:48:24.190Z
(i) To verify my understanding of your question, if the answer is yes, will that imply that co-3SAT (given a 3CNF formula, is it not satisfiable) is in NP?  (Because the execution path of your algorithm would give a poly-size, verifiable proof that the given formula is not satisfiable.)  Given that co-3SAT is co-NP-hard, this would imply NP = co-NP?  (ii) To disprove it, have you tried to find an infinite family of unsatisfiable 3CNF formula such that, for each formula of $n$ clauses, any subformula formed by, say, $\Theta(\log^2 n)$ of its clauses has super-poly$(n)$ satisfying assignments?
Neal Young
CC BY-SA 4.0
2021-12-12T13:17:20.700Z
(i) Yes. I suppose so.
(ii) Such a family is what I have been working on trying to find as a way of disproving it, but I have not had much success. To be fair though, I have been a bit distracted by school work and so haven't had a lot of time to put into the discovery of such a family.
Timothy Schommer
<optimization><time-complexity><sat><polynomial-time>
3-SAT runtime if an optimal order to eliminate possible solutions is known
Timothy Schommer
# 3-SAT runtime if an optimal order to eliminate possible solutions is known

(Asked by: username_0 on 2021-12-11)

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.

**Tags:** optimization, time-complexity, sat, polynomial-time

> **Comments:**
> **username_1**: *"polynomial with the input size and the number of accepting solutions"*... Just a quick note: Unambiguous-SAT (CNF-SAT with the promise that there is at most one satisfying solution) is hard for NP under randomized reductions ([https://en.wikipedia.org/wiki/Valiant–Vazirani_theorem](https://en.wikipedia.org/wiki/Valiant–Vazirani_theorem)).  So, in the worst case, SAT formulas with just one satisfying solution are not easier to solve.  
> **username_0**: @username_1 I am under no delusions that the problem I am looking at is any less hard than any other np-complete problem. I myself outlined a way to solve general 3-SAT in polynomial time if such a solution existed. Like I said, it is a mental exercise.  
> **username_1**: (i) To verify my understanding of your question, if the answer is yes, will that imply that co-3SAT (given a 3CNF formula, is it not satisfiable) is in NP?  (Because the execution path of your algorithm would give a poly-size, verifiable proof that the given formula is not satisfiable.)  Given that co-3SAT is co-NP-hard, this would imply NP = co-NP?  (ii) To disprove it, have you tried to find an infinite family of unsatisfiable 3CNF formula such that, for each formula of $n$ clauses, any subformula formed by, say, $\Theta(\log^2 n)$ of its clauses has super-poly$(n)$ satisfying assignments?  
> **username_0**: (i) Yes. I suppose so. (ii) Such a family is what I have been working on trying to find as a way of disproving it, but I have not had much success. To be fair though, I have been a bit distracted by school work and so haven't had a lot of time to put into the discovery of such a family.  

---

## 1 answers

### Answer by username_1 on 2021-12-13. Score: 2 | Accepted answer

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$


---

