Even, Itai & Shamir's limited backtracking algorithm for 2-SAT: is it really linear?
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:


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.
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 variables:
    # thread is alive
    thread_live = [True, False]
    # thread is currently updating the stack (either (var,index) or None)
    thread_stack_update = [None, 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
    thread_next_clause = [0, 0]
    # stack of clauses to handle
    thread_stack = [[], []]
    ## main loop
    while True:
        # check whether any threads are alive
        if all(not thread_live[thread] for thread in range(2)):
            return None
        # advance all live threads
        for thread in range(2):
            if not thread_live[thread]:
                continue
            # check whether thread is updating the stack
            if thread_stack_update[thread] is not None:
                var, index = thread_stack_update[thread]
                if index &lt; len(clauses_by_variable[var]):
                    thread_stack[thread].append(clauses_by_variable[var][index])
                    thread_stack_update[thread] = var, index+1
                else:
                    thread_stack_update[thread] = None
                continue
            # determine next clause to handle
            if len(thread_stack[thread]) &gt; 0:
                next_clause = thread_stack[thread].pop()
            else:
                next_clause = thread_next_clause[thread]
                thread_next_clause[thread] += 1
            # check whether we have finished handling all clauses
            if next_clause == len(clauses):
                assignment = []
                for var in range(n):
                    value = thread_assignment[thread][var]
                    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)]
            thr_values = [thread_assignment[thread][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)):
                # kill current thread
                thread_live[thread] = False
                continue
            # check whether there is a forced assignment
            if curr_values[0] is not None:
                forced = clause[1]
            elif curr_values[1] is not None:
                forced = clause[0]
            elif clause[0] == clause[1]: # clause contains two identical literals
                forced = clause[0]
            else:
                forced = None
            # handle forced assignment, if any
            if forced is not None:
                thread_assigned_variables[thread].append(forced.var)
                thread_assignment[thread][forced.var] = forced.value
                thread_stack_update[thread] = (forced.var,0)
                continue
            ## we have reached a decision point
            # update reference assignment
            for var in thread_assigned_variables[thread]:
                reference_assignment[var] = thread_assignment[thread][var]
            # undo assignments in threads
            for thr in range(2):
                for var in thread_assigned_variables[thr]:
                    thread_assignment[thr][var] = None
            # initialize threads
            for thr in range(2):
                thread_live[thr] = True
                thread_assigned_variables[thr] = [clause[0].var]
                thread_assignment[thr][clause[0].var] = [False,True][thr]
                thread_stack[thr] = []
                thread_stack_update[thr] = (clause[0].var,0)
                thread_next_clause[thr] = next_clause