How often can a learned clause cause this solver to backtrack?

Question

The is an improvement to the X3SAT solver I described in What is wrong with this simple proof of P=NP? I have fixed the flaw found in that solver. Now, I want to know how often the solver described below will backtrack because of a particular learned clause.

Exactly 1 in 3 SAT ($X3SAT$) is a variation of the Boolean Satisfiability problem. Given an instance of clauses where each clause has three literals, is there a set of literals such that each clause contains exactly one literal from the set. $X3SAT$ is NP-Complete even when the instance is monotone and linear. Monotone means all literals are positive. Linear means no two clauses share more than one variable in common.

The algorithm I describe is a clause based lexicographical satisfiability ($LexSAT$) solver. A $LexSAT$ solver finds the lowest or highest "numbered" satisfying assignment based on a given ordering of the variables or clauses.

Davis, Putnam, Logeman, Loveland ($DPLL$) with fixed variable order is an example of a LexSAT solver. If we agree 0 means a variable is false and 1 means a variable is true then any satisfying assignment of an $N$ variable instance can be represented by an $N$-bit binary number.

Assume all variables are unset. Choose the highest order unset variable and set it to 0 (false). If there is no conflict then repeat. If there is a conflict then backtrack and set the variable to 1 (true). If this also causes a conflict then backtrack to the lowest order variable that is set to 0. Set this variable to 1, unset all lower order variables, and repeat. This procedure will find the smallest binary number that represents a satisfying assignment.

The solver I describe below orders the $M$ clauses and represents a satisfying assignments with an $M$-trit ternary number.

Order the literals in each clause lexicographically, highest to lowest. Let $2$ represent the highest order literal, $0$ represent the lowest, and $1$ the middle literal. Then, order the clauses lexicographically, highest to lowest.

$\quad(t,r,h)(t,p,o)(t,n,l)(s,o,a)(s,m,l)(s,j,c)(r,q,j)(q,l,g)(o,j,e)(n,m,e)(l,k,e)(i,h,c)(g,f,e)(e,d,c)(c,b,a)$

This linear, monotone instance has two satisfying assignments:

a,d,g,i,j,k,m,t are true and all other variables are false.

b,e,i,q,s,t are true and all other variables are false.

Algorithm description:

1. Choose the highest order unsatisfied X3SAT clause.

2. Choose the lowest order unassigned variable in this clause and set it true.

3. Process all X3SAT clauses with this newly set true variable and set all other variables in these clauses to false.

4. Reduce learned clauses. Set to false all variables that appear in a unit learned clause.

5. If no conflict go to step 1.

6. Create a learned clause from the true variables that caused the conflict. Do not create a learned clause if one or more of the variables in the conflict clause wasn't set false in an assigned X3SAT clause.

7. Increment the lowest order satisfied clause that can be incremented.

8. Unset all variables set by clause assignments below the newly incremented clause.

9. Go to step 3.

Example (variables set to true are capitalized):

set clause-processed clauses / true / false

$\quad(t,r,H)-(i,H,c) / H / t,r,i,c$

$\quad(t,p,O)-(s,O,a)(O,j,e) / O,H / t,s,r,p,j,i,e,c,a$

$(s,j,c)$ is a conflict

There can never be more than three true variables involved in a conflict:

$s$ was set false when $O$ was set true in $(s,O,a)$

$j$ was set false when $O$ was set true in $(O,j,e)$

$c$ was set false when H was set true in $(i,H,c)$

$\quad(s,j,c)-(s,O,a)(O,j,e)(i,H,c)$

$H$ and $O$ cause the conflict. Add $(\bar o \lor \bar h)$ to the learned clauses.

Increment $(t,p,o)$, setting $P$ true, and go to step 3.

Repeating this process eventually creates the following learned clauses;

$\quad(\bar o \lor \bar h), (\bar l), (\bar n \lor \bar a), (\bar s \lor \bar n), (\bar o \lor \bar n)$

It is possible for more than one clause to cause a conflict. There can also be more than one true variable that forces a variable to be set false in the conflict clause. When these things happen simply create multiple learned clauses. There will still never be more than three literals in a learned clause.

The lowest numbered satisfying assignment is $t, m, k, j, i, g, d, a$ true and all other variables false: $\quad(T,r,h)(T,p,o)(T,n,l)(s,o,A)(s,M,l)(s,J,c)(r,q,J)(q,l,G)(o,J,e)(n,M,e)(l,K,e)(I,h,c)(G,f,e)(e,D,c)(c,b,A)$

This corresponds to the base 3 number $222011001112210$.

The other satisfying assignment would correspond to $222222120002021$.

$\quad(T,r,h)(T,p,o)(T,n,l)(S,o,a)(S,m,l)(S,j,c)(r,Q,j)(Q,l,g)(o,j,E)(n,m,E)(l,k,E)(I,h,c)(g,f,E)(E,d,c)(c,B,a)$

Since there can't be more than $O(n^3)$ learned clauses it is tempting to claim this proves $P=NP$. It appears this solver will only backtrack a polynomial number of times before finding a satisfying assignment or proving the instance unsatisfiable.

Unfortunately, a given learned clause can cause the solver to backtrack multiple times. For example, $(\bar l)$ prevents $l$ from being set true in $(t,n,l)$ when $(t,r,h)$ gets incremented.

My question is how often can a learned clause cause this solver to backtrack?

It is obvious there are upper bounds. Take $(\bar l)$ as an example. $l$ appears in the third highest order clause, $(t,n,l)$. We can ignore all lower order clauses because $l$ will always be false when these clauses get processed. Since there are only two higher order clauses than $(t,n,l)$, $(\bar l)$ can't cause more than $3^2$ increments.

The learned clause $(\bar o \lor \bar h)$ can't cause more than one backtrack. $o$ is in the second highest order clause and $h$ must be true in the highest order clause before $(\bar o \lor \bar h)$ can force a backtrack.