# Even, Itai & Shamir's limited backtracking algorithm for 2-SAT: is it really linear?

I have read in Wikipedia (and other sources) about the limited backtracking algorithm of Even, Itai & Shamir for solving 2-SAT problem in a linear time, but the approach doesn't seem to be linear, there is no demonstration nor algorithm implementation to check it.

Here is the algorithm description from Wikipedia: Even, Itai & Shamir - Limited backtracking.

PS: I am not searching for an algorithm to solve 2-SAT problem in a linear time since I have read about the Aspvall, Plass & Tarjan approach. I am just interested in the former algorithm.

• What research have you done? Wikipedia is not a primary source. You should read the original paper; I would imagine they probably give the running time analysis there. Wikipedia has a citation to the paper. (If for some reason you are unable to do that, you should edit the question to give a self-contained specification of the algorithm and show your running time analysis. Why do you think it isn't linear? Do you have a counterexample that you can show takes super-linear time? But really you should just read the paper.) – D.W. Sep 22 '17 at 4:19
• @D.W. Unfortunately the paper is a bit sketchy on these details. – Yuval Filmus Sep 22 '17 at 10:11
• The algorithm seems correct, and with a little bit of work it can be implemented in linear time on a RAM machine. It's an exercise in programming, so this question seems somewhat off-topic here. – Yuval Filmus Sep 22 '17 at 10:15
• @D.W. I couldn't find the original paper, it is paying. but I did my research and I found the same description elsewhere. anyway, YuvalFilmus's response helped me to understand it, thanks all. – younes zeboudj Sep 30 '17 at 18:39

Below you can find a (non-optimized) python implementation of the algorithm. First, I give some hints explaining why this implementation runs in linear time. These hints assume that you know what is roughly going on, and that you have read the code.

The algorithm runs up to two threads at any given time. Initially only one thread is run. Whenever reaching a decision point (a clause with two unassigned variables), it kills the other thread and "forks" the current thread into two. The current thread is killed if it reaches an unsatisfiable clause, and if both threads are dead then the algorithm returns "unsatisfiable".

The algorithm is careful to maintain the following properties:

• The two threads are run in lockstep, each step running in $O(1)$ (apart from forking).
• Forking takes time $O(t)$, where $t$ is the number of steps since the last fork (or since the start or the algorithm).
• The total running time of all non-killed threads is $O(n+m)$ (where $n$ is the number of variables and $m$ is the number of clauses).

These properties guarantee that the main body of the algorithm runs in time $O(n+m)$. The initialization step also runs in time $O(n+m)$, and so the entire algorithm runs in time $O(n+m)$.

There are two somewhat non-trivial implementation details:

1. Maintaining the partial assignments for the threads. Each thread needs to maintain a partial assignment. Upon reaching a decision point, this partial assignment needs to be forked. A naive implementation would take $O(n)$ to copy the partial assignment. The implementation below uses a two-tiered strategy to handle this: there is a reference assignment which is common to both threads, and there is a per-thread addition. The implementation also keeps track on which variables were set during each thread, and uses this to maintain this data structure.

2. Handling the repercussions of an assignment. Whenever a variable is assigned, we need to check on all other clauses containing this variable. This is done by precalculating all clauses containing each variable, and keeping a stack of "clauses to check" for each thread. Since a variable could appear in many clauses, we copy one clause to the stack in each iteration. This forces us to keep a state machine (with two states).

The code below accepts two parameters: n is the number of variables, and clauses is a list of pairs of instances of Literal. For example, to check whether the 2CNF $(x_0 \lor \lnot x_1) \land (\lnot x_0 \lor x_2)$ is satisfiable, run

EIS(3, [(Literal(0,True),Literal(1,False)), (Literal(0,False),Literal(2,True))])

Here is the complete code:

class Literal:
def __init__(self, var, value):
self.var = var
self.value = value
def __repr__(self):
if self.value:
return '+x%d' % (self.var,)
else:
return '-x%d' % (self.var,)

def EIS(n, clauses):
"""
Solve a 2SAT formula 'clauses' on 'n' variables.
The formula is given as a list of pairs of Literal.
Returns a satisfying assignment or None if formula is unsatisfiable."""
## construct for each variable a list of clauses it appears in
clauses_by_variable = [[] for _ in range(n)]
for index,clause in enumerate(clauses):
for literal in clause:
clauses_by_variable[literal.var].append(index)
## initialization
# reference assignment
reference_assignment = [None for _ in range(n)]
# thread is currently updating the stack (either (var,index) or None)
# new assignment (as partial assignment)
thread_assignment = [[None for _ in range(n)] for _ in range(2)]
# variables assigned in this thread
thread_assigned_variables = [[] for _ in range(2)]
# next unhandled clause
# stack of clauses to handle
## main loop
while True:
# check whether any threads are alive
return None
continue
# check whether thread is updating the stack
if index < len(clauses_by_variable[var]):
else:
continue
# determine next clause to handle
else:
# check whether we have finished handling all clauses
if next_clause == len(clauses):
assignment = []
for var in range(n):
if value is None:
value = reference_assignment[var]
if value is None:
value = True # arbitrary value
assignment.append(value)
return assignment
# otherwise, read clause and current assignment to variables
clause = clauses[next_clause]
ref_values = [reference_assignment[clause[i].var] for i in range(2)]
curr_values = [ref_values[i] if thr_values[i] is None else thr_values[i] for i in range(2)]
# check whether current clause is already satisfied
if any(clause[i].value == curr_values[i] for i in range(2)):
continue
# check whether current clause is unsatisfiable
if all(clause[i].value != curr_values[i] and curr_values[i] is not None for i in range(2)):
continue
# check whether there is a forced assignment
if curr_values is not None:
forced = clause
elif curr_values is not None:
forced = clause
elif clause == clause: # clause contains two identical literals
forced = clause
else:
forced = None
# handle forced assignment, if any
if forced is not None:
continue
## we have reached a decision point
# update reference assignment