Algorithms-In-Python/12a) 2SAT - Papadimitrou's algorithm.py at master · codeyangjun/Algorithms-In-Python · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
import math
import random
import gc

def papadimitrou(clauses):

    n = len(clauses)

    for j in xrange(int(math.log(n, 2))):
        assignment = random_assignment(n)
        i = 2*n*n
        while i > 0:
            i -= 1
            clause_index = unsatisfied_clause(clauses, assignment)
            if clause_index is None:
                return 'satisfiable'
            else:
                var_index = abs(clauses[clause_index][random.randint(0, 1)]) - 1
                assignment[var_index] = 1 - assignment[var_index]

    return 'unsatisfiable'


def random_assignment(n):
    return [random.randint(0, 1) for _ in xrange(n)]


def unsatisfied_clause(clauses, assignment):
    for i in xrange(len(clauses)):
        if ((clauses[i][0] < 0 and assignment[abs(clauses[i][0])-1] == 1) or     \
            (clauses[i][0] > 0 and assignment[abs(clauses[i][0])-1] == 0)) and   \
            ((clauses[i][1] < 0 and assignment[abs(clauses[i][1])-1] == 1) or    \
            (clauses[i][1] > 0 and assignment[abs(clauses[i][1])-1] == 0)):
            return i
    return None


def main():
    for i in xrange(1, 7):
        print 'file %i' % i
        f = open('two-sat%i.txt' % i)
        n = int(f.readline())
        clauses = [[int(x) for x in line.split()] for line in f]

        print 'result: %s\n' % papadimitrou(clauses)

        gc.collect()


main()