Comment lines
The first line starts with a c, which provides a comment line. Comment lines can provide any information, and we can use 0 or more comment lines.

Problem Line
The second line starts with a p, denoting a problem line. The problem line follows the following pattern: p FORMAT VARIABLES CLAUSES.

• Format: This is the file format, useful for programs to detect the format the file uses. 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.

In the second line, we specified our problem file contains 4 clauses, so we must express these clauses as 4 distinct lines where each number represents 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. A value of 0 does not represent a variable.

Based on our problem file (which has 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 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 start with a c character as shown in the first line of our file.

Variables lines

Note that we then have a line starting with v, which denotes the variables from our problem with their 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 character, as shown 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 the 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 get extracted and added into a list. The function then returns a list where each element is a clause.

The function returns the following when applied to our problem file:

[[1, -5, 3], [-2, 4, 5], [4, -6], [3]]

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

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 their corresponding value.

The function returns the following when applied to 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 problem 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 their 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.

Our function iterates over all clauses, evaluating whether any variable in the clause evaluates to True, that serves as proof that it satisfies the clause.

Once all clauses evaluate, the program displays the summary on the console. 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)


if __name__ == "__main__":
    main()