2 SAT Problem

Python Algorithm Kosaraju's Algorithm
Python
Publish Date:   2022-06-07
Update Date:   2023-03-28
Word Count:   1.9k
Read Times:   11 Min
Read Count:  

2 SAT Problem

1. What is SAT Problem

Boolean Satisfiability or simply SAT is the problem of determining if a Boolean formula is satisfiable or unsatisfiable.

  • Satisfiable : If the Boolean variables can be assigned values such that the formula turns out to be TRUE, then we say that the formula is satisfiable.
  • Unsatisfiable : If it is not possible to assign such values, then we say that the formula is unsatisfiable.

Examples:

  • $F=A\land \bar{B}$ is satisfiable, because A = TRUE and B = FALSE makes F = TRUE.
  • $F = A \land \bar{A}$ is unsatisfiable, because
    • if A = True, $\bar{A}$ = False, they and together, F = False
    • if A = False, $\bar{A}$ = True, they and together, F = False

Symbol explanation:

  • A is one term, it can be True or False
  • $\bar{A}$ is not A, it is opposite to A’s Boolean value
  • $\land$ is and gate
  • $\lor$ is or gate

2. What is Conjunctive Normal Form (CNF)

To understand Problem of 2-Satisfiability better, first let us see what is Conjunctive Normal Form (CNF)

CNF : CNF is a conjunction (AND) of clauses, where every clause is a disjunction (OR).

Example:
$$
F= (A_1 \lor B_1 \lor C_1 \lor …) \land (A_2 \lor B_2\lor C_2 \lor …) \land (A_3 \lor B_3\lor C_3 \lor …) \land …… \land (A_m \lor B_m\lor C_m \lor …)
$$

3. What is 2-SAT problem

Thus, Problem of 2-Satisfiability can be stated as:
Given CNF with each clause having only 2 terms, is it possible to assign such values to the variables so that the CNF is TRUE?

Example:

  • $$
    F= (x_1 \lor x_2 ) \land (x_2 \lor \bar{x}_1) \land (\bar{x}_1 \lor \bar{x}_2)
    $$

    The given expression is satisfiable.

    for x1 = FALSE, x2 = TRUE

  • $$
    F= (x_1 \lor x_2 ) \land (x_2 \lor \bar{x}_1)\land (x_1 \lor \bar{x}_2) \land (\bar{x}_1 \lor \bar{x}_2)
    $$

    The given expression is unsatisfiable.

    for all possible combinations of x1 and x2

4. How to solve the 2-SAT problem4

Prepare:

For the CNF value to come TRUE, value of every clause should be TRUE.

Let one of the clause be ($A\lor B$) = True

  • if A=0, B must be 1, ($\bar{A} \Rightarrow B $)
  • if B=0, A must be 1, ($\bar{B} \Rightarrow A $)

Then we create an Implication Graph which has 2 edges for every clause of the CNF.

($A\lor B$) expressed in Graph as $edge(\bar{A} \Rightarrow B )$ , $edge(\bar{B} \Rightarrow A )$

So for a Boolean formula with m clauses, we have 2 edges for every clause in Graph. So 2m edges in total.

Case:

Case 1: If $edge(X\rightarrow \bar{X})$ exists in the graph

It means if X=True, $\bar{X}$ = True

But if X = False, can not decide $\bar{X}$

Case 2: If $edge(\bar{X}\rightarrow X)$ exists in the graph

It means if $\bar{X}$ =True, X = True

But if $\bar{X}$ = False, can not decide X

Case 3: If $edge(\bar{X}\rightarrow X) \space and \space edge(X\rightarrow \bar{X})$ exists in the graph at same time

One edge requires X to be TRUE and the other one requires X to be FALSE.

Thus, there is no possible assignment in such a case.

CONCLUSION: If any two variables $X$ and $\bar{X}$ are on a cycle i.e. $edge(\bar{X}\rightarrow X) \space and \space edge(X\rightarrow \bar{X})$ both exists, then the CNF is unsatisfiable. Otherwise, there is a possible assignment and the CNF is satisfiable.

CONCLUSION FROM IMPLEMENTATION POINT OF VIEW:
If both $X$ and $\bar{X}$ lie in the same SCC (Strongly Connected Component), the CNF is unsatisfiable.

Strongly Connected Component:

A Strongly Connected Component of a directed graph has nodes such that every node can be reach from every another node in that SCC.

3 SCCs here

image-20220607145236240

5. Code for solve 2-SAT problem implement by Python

Total code

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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
import time

test_data = [ ]
with open('2satBIG.cnf', 'r') as f:
    for line in f.readlines():
        test_data.append(line.strip())  # 把末尾的'\n'删掉

A = []
B = []
n = 0
m = 0
for rec in test_data:
    rec=rec.strip()
    junk_list = []
    substrs = rec.split()
    if substrs[0] == 'p' and  substrs[1] == 'cnf':
        n=int(substrs[2])
        m=int(substrs[3])
    ## record has to start with a number or a minus sign
    if (rec[0].isdigit()) or (rec[0].startswith("-")):
        substrs = rec.split()
        try:
            if len(substrs) == 3:
                for num in range(len(substrs)):
                    num_int = int(substrs[num])
                    if num == 0:
                        A.append(num_int)
                    elif num ==1:
                        B.append(num_int)
            elif len(substrs) == 2:
                for num in range(len(substrs)):
                    num_int = int(substrs[num])
                    if num == 0:
                        A.append(num_int)
                        B.append(num_int)
        except:
            print("error converting", rec)



MAX = 1000000

adj = []
adjInv = []
for i in range(0, MAX + 1):
    adj.append([])
    adjInv.append([])
visited = [False] * MAX
visitedInv = [False] * MAX
s = []

scc = [0] * MAX

count = 1


def add_edge(a, b):
    adj[a].append(b)


def add_edge_inv(a, b):
    adjInv[b].append(a)


def dfs_first(u):
    if visited[u]:
        return
    visited[u] = True
    for i in range(0, len(adj[u])):
        dfs_first(adj[u][i])
    s.append(u)
    # print("stack: " + str(s))


def dfs_second(u):
    if visitedInv[u]:
        return
    visitedInv[u] = True
    for i in range(0, len(adjInv[u])):
        dfs_second(adjInv[u][i])
    scc[u] = count


def is_2_sat(n, m, a, b):
    global count
    for i in range(0, m):
        if a[i] > 0 and b[i] > 0:
            add_edge(a[i] + n, b[i])
            add_edge_inv(a[i] + n, b[i])
            add_edge(b[i] + n, a[i])
            add_edge_inv(b[i] + n, a[i])

        elif a[i] > 0 > b[i]:
            add_edge(a[i] + n, n - b[i])
            add_edge_inv(a[i] + n, n - b[i])
            add_edge(-b[i], a[i])
            add_edge_inv(-b[i], a[i])

        elif a[i] < 0 < b[i]:
            add_edge(-a[i], b[i])
            add_edge_inv(-a[i], b[i])
            add_edge(b[i] + n, n - a[i])
            add_edge_inv(b[i] + n, n - a[i])

        else:
            add_edge(-a[i], n - b[i])
            add_edge_inv(-a[i], n - b[i])
            add_edge(-b[i], n - a[i])
            add_edge_inv(-b[i], n - a[i])


    for i in range(1, 2 * n + 1):
        if not visited[i]:
            dfs_first(i)

    while len(s) != 0:
        top = s.pop()

        if not visitedInv[top]:
            dfs_second(top)
            count += 1

        # print("scc: " + str(scc[0:20]))

    for i in range(1, n + 1):
        if scc[i] == scc[i + n]:
            print("The given expression is unsatisfiable")
            return

    print("The given expression is satisfiable")
    for i in range(1, n + 1):
        if scc[i] > scc[i + n]:
            pass
            # print("x" + str(i) + ": True")
        else:
            pass
            # print("x" + str(i) + ": False")


if __name__ == '__main__':
    start = time.time()
    # for i in range(100):
    is_2_sat(n, m, A, B)
    end = time.time()
    print(end-start)

Part 1, read CNF file

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
test_data = [ ]
with open('2satBIG.cnf', 'r') as f:
    for line in f.readlines():
        test_data.append(line.strip())  # 把末尾的'\n'删掉

A = []
B = []
n = 0
m = 0
for rec in test_data:
    rec=rec.strip()
    junk_list = []
    substrs = rec.split()
    if substrs[0] == 'p' and  substrs[1] == 'cnf':
        n=int(substrs[2])
        m=int(substrs[3])
    ## record has to start with a number or a minus sign
    if (rec[0].isdigit()) or (rec[0].startswith("-")):
        substrs = rec.split()
        try:
            if len(substrs) == 3:
                for num in range(len(substrs)):
                    num_int = int(substrs[num])
                    if num == 0:
                        A.append(num_int)
                    elif num ==1:
                        B.append(num_int)
            elif len(substrs) == 2:
                for num in range(len(substrs)):
                    num_int = int(substrs[num])
                    if num == 0:
                        A.append(num_int)
                        B.append(num_int)
        except:
            print("error converting", rec)

Part 2, check 2 SAT-Problem

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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
MAX = 1000000

adj = []
adjInv = []
for i in range(0, MAX + 1):
    adj.append([])
    adjInv.append([])
visited = [False] * MAX
visitedInv = [False] * MAX
s = []

scc = [0] * MAX

count = 1


def add_edge(a, b):
    adj[a].append(b)


def add_edge_inv(a, b):
    adjInv[b].append(a)


def dfs_first(u):
    if visited[u]:
        return
    visited[u] = True
    for i in range(0, len(adj[u])):
        dfs_first(adj[u][i])
    s.append(u)


def dfs_second(u):
    if visitedInv[u]:
        return
    visitedInv[u] = True
    for i in range(0, len(adjInv[u])):
        dfs_second(adjInv[u][i])
    scc[u] = count

# m number of clauses
# n number of terms
# A all terms in first position
# B all terms in second position
def is_2_sat(n, m, a, b):
    global count
    for i in range(0, m):
        if a[i] > 0 and b[i] > 0:
            add_edge(a[i] + n, b[i])
            add_edge_inv(a[i] + n, b[i])
            add_edge(b[i] + n, a[i])
            add_edge_inv(b[i] + n, a[i])

        elif a[i] > 0 > b[i]:
            add_edge(a[i] + n, n - b[i])
            add_edge_inv(a[i] + n, n - b[i])
            add_edge(-b[i], a[i])
            add_edge_inv(-b[i], a[i])

        elif a[i] < 0 < b[i]:
            add_edge(-a[i], b[i])
            add_edge_inv(-a[i], b[i])
            add_edge(b[i] + n, n - a[i])
            add_edge_inv(b[i] + n, n - a[i])

        else:
            add_edge(-a[i], n - b[i])
            add_edge_inv(-a[i], n - b[i])
            add_edge(-b[i], n - a[i])
            add_edge_inv(-b[i], n - a[i])


    for i in range(1, 2 * n + 1):
        if not visited[i]:
            dfs_first(i)

    while len(s) != 0:
        top = s.pop()
        if not visitedInv[top]:
            dfs_second(top)
            count += 1



    for i in range(1, n + 1):
        if scc[i] == scc[i + n]:
            print("The given expression is unsatisfiable")
            return

    print("The given expression is satisfiable")



if __name__ == '__main__':
    start = time.time()
    # for i in range(100):
    is_2_sat(n, m, A, B)
    end = time.time()
    print(end-start)

6. Explanation for Algo

Step 1:

The after reading the CNF file it will return us four parameters

  • m number of clauses
  • n number of terms
  • A all terms in first position
  • B all terms in second position

Step 2:

1
scc = [0] * MAX

This is used for checking the SCC problem.

Store the count number in the corresponding position in SCC.

Step 3:

Based on the input terms’ sign, we will decide how we set up the edges.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
for i in range(0, m):
        if a[i] > 0 and b[i] > 0:
            add_edge(a[i] + n, b[i])
            add_edge_inv(a[i] + n, b[i])
            add_edge(b[i] + n, a[i])
            add_edge_inv(b[i] + n, a[i])

        elif a[i] > 0 > b[i]:
            add_edge(a[i] + n, n - b[i])
            add_edge_inv(a[i] + n, n - b[i])
            add_edge(-b[i], a[i])
            add_edge_inv(-b[i], a[i])

        elif a[i] < 0 < b[i]:
            add_edge(-a[i], b[i])
            add_edge_inv(-a[i], b[i])
            add_edge(b[i] + n, n - a[i])
            add_edge_inv(b[i] + n, n - a[i])

        else:
            add_edge(-a[i], n - b[i])
            add_edge_inv(-a[i], n - b[i])
            add_edge(-b[i], n - a[i])
            add_edge_inv(-b[i], n - a[i])

Step 4:

execute the DFS

changing the count number

1
2
3
4
5
6
7
8
9
for i in range(1, 2 * n + 1):
    if not visited[i]:
        dfs_first(i)

while len(s) != 0:
    top = s.pop()
    if not visitedInv[top]:
        dfs_second(top)
        count += 1

Step 5:

Whether there is both $X$ and $\bar{X}$ lie in the same SCC condition. Return results.

1
2
3
4
5
6
for i in range(1, n + 1):
    if scc[i] == scc[i + n]:
        print("The given expression is unsatisfiable")
        return

print("The given expression is satisfiable")
Author: Liang Junyi
Link: https://liangjunyi010.github.io/liangjunyi.github.io/2022/06/07/project-2-sat-problem/
Reprint policy: All articles in this blog are used except for special statements CC BY 4.0 reprint policy. If reproduced, please indicate source Liang Junyi !
Python Algorithm Kosaraju's Algorithm
  TOC