Kelson Martins Blog

Introduction

Recently I have had the opportunity to work with Boolean Satisfiability Problems and techniques on how to efficiently solve them. I personally found the topic extremely interesting so I decided to produce this article as the first of a series on how to solve SAT problems with a few different meta-heuristic techniques.
All SAT solver algorithms have something in common: they need some sort of procedure to evaluate whether the generated solution satisfies all clauses of an SAT problem or not.
Given this information, this article presents the implementation of a python SAT checker, which has the goal of reading SAT Problem File in the CNF DIMACS file format, and evaluate how many clauses are satisfied given a solution file.

The SAT Problem File

An SAT problem consists of 2 components: variables and clauses.
CNF DIMACS format was then created as a way of defining Boolean expressions, written in conjunctive normal form.
An example of a CNF DIMACS format file is:
c cnf comment line
p cnf 6 4
1 -5 3 0
-2 4 5 0
4 -6 0
3 0
Problem File Breakdown
Comment lines
The first line is starting with a c, which indicates the line as a comment line. Comment lines can be used to point any information. 0 or more comment lines can be used.
Problem Line
The second is being started with a p,  indicating that it is a problem line.  The problem line follows the following pattern: p FORMAT VARIABLES CLAUSES.
Format: Is the file format, useful for programs to detect which format the file is expected to be. For our scenario, the format is cnf.
Variables: The number of unique variables our SAT problem contains.
Clauses: The total number of clauses our problem contains.
Clauses Lines
Subsequent Lines in our file are the Clauses lines.
As in the Problem line, we defined that our problem file contains 4 clauses, these clauses are then expressed as 4 distinct lines where each number represent a variable.
Having a positive number represents the variable having the value of True.
Having a negative number represents the variable having the value of False.
The value 0, at the end of the line, represents the end of the clause representation. A value of 0 does not represent a variable.
Based on our problem file with 6 vars and 4 clauses, our Boolean expression is:
( (x1) OR NOT(x5) OR (x3) OR (x4) )
AND 
( NOT(x2) OR (x4) OR (x5) )
AND
( (x4) OR NOT(x6) )
AND
(x3)

The SAT Solution File

Having the problem file available is the first step in producing our SAT checker. But this is just the first component, as we also require the solution file.
An example of a solution file for the problem file previously detailed is:
c cnf solution file comment
v  -1 2 3 4 -5 -6
v  0
Solution File Breakdown
Comment lines
Similar to the Problem file, solution files can also contain comments, which also starts with a c as shown in the first line of our file.
Variables lines
Note that we then have a line starting with v, which determines the variables from our problem with its respective values.
Again:
Having a positive number represents the variable having a value of True.
Having a negative number represents the variable having a value of False.
Variables lines end with a line containing an individual 0, as demonstrated in the third line of our solution file.

Show Me the Code

Now that we have the details about SAT Problem and Solution files, we can then develop a python parser to check whether the solution file completely satisfies all the clauses of the problem.
First, here is the function that reads Problem file to break it down and extract all of its clauses.
def read_clauses(path):

    clauses = []

    try:
        file = open(path,"r")

        clauses_lines = False

        for line in file:
            if line.startswith("p"):
                clauses_lines = True
                continue

            if line.startswith("%"):
                clauses_lines = False

            if clauses_lines:                    
                # removing trailing spaces, removing last 0 items and converting to number
                clause = [int(s) for s in re.split('[\s]+',line.strip())][:-1] 

                clauses.append(clause)            

        file.close()       

    except IOError:
        print("Can not find input file or read data")
        exit()

    return clauses
This function is key since it reads the problem file, and parses it so all the clauses are extracted and added into a list.
The function then returns a list where each element is a clause.
The function returns the following if reading our problem file:
[[1, -5, 3], [-2, 4, 5], [4, -6], [3]]

Similarly, the function to read and parse the solution file is presented:

def read_solution(path):

    solution = []

    try:
        file = open(path,"r")

        for line in file:
            if line.startswith("v"):
                
                split_solution = line[3:].split(" ")

                for i in range(len(split_solution)):
                    solution.append(split_solution[i])

        # converting list to int and removing last item "0"
        solution = list(map(int, solution))[:-1]

        file.close()       

    except IOError:
        print("Can not find input file or read data")
        exit()

    return solution
The read_solution function has similar functionality to the read_clauses function previously shown, the difference being that the read_solution parses the solution file and returns a list with all variables with its corresponding value.
The function returns the following if parsing our solution file:
[-1, 2, 3, 4, -5, -6]
Having read and parsed our Problem and Solution files, we have now all the tools required to write a checker that will evaluate whether all clauses from the problem are satisfied.
The following function does the job:
def check_satisfation(clauses, solution):

    total_clauses = len(clauses)
    total_satistied = 0
    total_non_satisfied = 0

    # iterating over all clauses
    for i in range(len(clauses)):
        
        satistied = False

        for j in range(len(clauses[i])):
                
            if clauses[i][j] in solution:
                satistied = True
        
        if satistied:
            total_satistied += 1
        else:
            total_non_satisfied += 1    
    
    print("Total Clauses: " + str(total_clauses))
    print("Satisfied Clauses: " + str(total_satistied))
    print("Non Satisfied Clauses: " + str(total_non_satisfied))
First, note that our function expects 2 parameters: [clauses, solution].
The clauses parameter is a list of clauses and its variables, which is what the read_solution() function returns.
The solution parameter is a list of variables that represents an attempt to solve the problem. This is what the read_solution() function returns.
Saying that our function iterates over all clauses, evaluating whether any variable in the clause evaluates to True, which would indicate that the clause is satisfied.
Once all clauses are evaluated, the summary is displayed.
Quite simple, is it not?

Putting it all together

Having the 3 functions that are the core of our project ready, we can just put it all together with something like:
def main():
    
    clauses = read_clauses(PROBLEM_FILEPATH)
    solution = read_solution(SOLUTION_FILEPATH)

    check_satisfation(clauses,solution)
Note that the entry point of our script expects 2 files, one for the problem and one for the solution files.
We then pass the appropriate file to its respective function, before calling the main check_satisfaction() function, which provides our results.

Testing the Code

Let’s now perform some tests.
Let’s assume the following Problem and Solution files:
problem_1.cnf
c cnf comment line
p cnf 6 4
1 -5 3 0
-2 4 5 0
4 -6 0
3 0
solution_1.cnf
c cnf solution file comment
v  -1 2 3 4 -5 -6
v  0

By Calling our checker with the files as parameters, the following is expected:

python sat_checker.py problem_1.cnf solution_1.cnf

Total Clauses: 4
Satisfied Clauses: 4
Non Satisfied Clauses: 0
If we analyze the problem and the solution presented, indeed we can confirm that all clauses are satisfied.
Shall we perform another test?
problem_2.cnf
c cnf comment line
p cnf 6 5
1 -2 6 0
-1 4 -3 0
4 -2 0
3 -5 2 0
-6 3 4 0
solution_2.cnf
c cnf solution file comment
v  -1 2 3 4 -5 -6
v  0

By testing the new problem files, we expect the following:

python sat_checker.py problem_2.cnf solution_2.cnf

Total Clauses: 5
Satisfied Clauses: 4
Non Satisfied Clauses: 1
Analyzing the output, we can identify that there is one clause not being satisfied.
By performing a further analysis, we can identify that the first clause [1, -2, 6] is the clause that can not be satisfied given the presented solution.

Conclusion

Boolean Satisfiability Problem (SAT) is a popular topic in Computer Science. SAT problem is also the first problem that was proven to be NP-Complete.
Before going through techniques of how to develop solutions for SAT Problems, this article presented the implementation of an SAT checker that determines whether a given Solution satisfies all clauses of a given Problem.
This article used Problem files in the CNF DIMACS format. These files can be generated by a few different tools, with cnfgen being a popular one.
You can also find the complete code presented in this article in Github.
Finally, as previously mentioned, this article is the first of a series of planned articles on the SAT topic. Future articles on this topic will start to approach techniques for the creation of solutions that satisfies all clauses, not just checking them.
Stay Tuned!

Software engineer, geek, traveler, wannabe athlete and a lifelong learner. Works at @IBM

Next Post