3
$\begingroup$

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.

Has anyone heard about this algorithm? Does anyone have its implementation/demonstration?

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.

$\endgroup$

migrated from stackoverflow.com Sep 22 '17 at 3:29

This question came from our site for professional and enthusiast programmers.

  • 1
    $\begingroup$ 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.) $\endgroup$ – D.W. Sep 22 '17 at 4:19
  • 1
    $\begingroup$ @D.W. Unfortunately the paper is a bit sketchy on these details. $\endgroup$ – Yuval Filmus Sep 22 '17 at 10:11
  • $\begingroup$ 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. $\endgroup$ – Yuval Filmus Sep 22 '17 at 10:15
  • $\begingroup$ @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. $\endgroup$ – younes zeboudj Sep 30 '17 at 18:39
5
$\begingroup$

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 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 < 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]) > 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
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.