2 SAT Problem

Algorithm Python 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

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

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

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:

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.

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

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.

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://LiangJunyi-010.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 !
Algorithm Python Kosaraju's Algorithm
  TOC