For example, a statement in CNF might look like this:

$($a OR NOT b$)$ AND $($b OR c OR NOT d$)$ AND $($d OR NOT e$)$

In our project, a literal also includes two boolean constants TRUE and FALSE. Your program should return a list of variable assignments that make the CNF formula true. For instance, to make $($AND a b$)$ true, both $"$a$"$ and $"$b$"$ need to be TRUE. To make $($OR a b$)$ true, there are three possible solutions, both $"$a$"$ and $"$b$"$ are TRUE, or $"$a$"$ is TRUE, $"$b$"$ is FALSE, or $"$b$"$ is TRUE, $"$a$"$ is FALSE.

The context$-$free grammar for the CNF formula is straightforward and defined in our project as below:

$1.\backslash ($ ::$=()\backslash )$ AND $\backslash (\backslash$mid$()\backslash )$

$2.\backslash ($ ::$=$O R$\backslash$mid $\backslash )$

$3.\backslash ($ ::$=\backslash$mid N O T $\backslash )$

$4.\backslash ($ ::$=$a$|$b$|\backslash$ldots$|$z$|\backslash )$ TRUE $\backslash (\backslash$mid $\backslash )$ FALSE

$2$ Input and Output of the Program

The input to the program is a string list. An example is below:

$"($ a OR b OR NOT c $)$ AND $($NOT a $)$ AND TRUE"

The program's output is of the type $($string$,$ bool$)$ list, which gives the first possible boolean value assignment of the variables to satisfy the CNF formula. An example is below:

If such an assignment doesn't exist, please return a list of one tuple, as in

the example shown below:

$[("$error$",$ true$)]$

$3$ Basic Function Implementations

First, you need to break down the input string into a string list by eliminating

white spaces. This function is already provided to you in the "project$2\_$driver.ml$"$

file, called "tokensListFromString $($str : string$)".$

Next, you will need to implement a basic called "partition" in the code

package given to you. The purpose of the "partition" function is to break down

a string list with respect to a delimiter. It will help you get the input string list

represented in a way that facilitates further processing.

Table $1$: Required Functions

The input and output type of the "partition" function is given in Table $1.$

An example of the input and output of the "partition" function is below:

Name: partition

Input: $["("$; $"$a$"$; $"$OR$"$; "NOT"; $"$b$"$; $")"$; "AND"; $"("$; $"$b$"$; $")"]$ "AND"

Output: $[["("$; $"$a$"$; $"$OR$"$; "NOT"; $"$b$"$; $")"]$; $["("$; $"$b$"$; $")"]]$

There are a few other basic functions you have to implement, listed below:

The next function you will have to implement is called "getVariables". It

takes a string list and gets the list of the variable names from the CNF$.$ The

input and output types are specified in Table $1.$ It filters out the left$/$right

parenthesis, AND$/$OR$,$ TRUE$/$FALSE$,$ and NOT items out of the string list

representing the input. The output should not have duplicates. An example is

given below:

Name: getVariables

Input: $["("$; $"$a$"$; $"$OR$"$; "NOT"; $"$b$"$; $")"$; "AND"; $"("$; $"$b$"$; $")"]$

Output: $["$a$"$; $"$b$"]$

You will also have to implement the function called "generateDefaultAssign$-$

ments". It takes the list of variables, and outputs a list of tuples, each tuple

being a variable name and the boolean value "false". It is used to initialize the

set of variables to the "false" value. An example is given below:

Name: generateDefaultAssignments

Input: $["$a$"$;$"$b$"]$

Output: $[("$a$",$ false$)"$b$",$ false$)]$

You will also have to implement the function called "generateNextAssign$-$

ments". This function takes a list of string$-$boolean tuples, and returns an up$-$

dated list of string$-$boolean tuples as if the singular binary number represented

by the booleans is incremented by $1,$ as well as an additional boolean value carry

for when it overflows. Essentially, starting with the rightmost variable, if the

checked variable is assigned to false, it is set to true. If the checked variable

is true, it is set to false and the algorithm carries to next variable to the left.

The returned boolean value carry is true only if the resulting binary number

overflows the given space, i$.$e$.$ the algorithm reaches the leftmost variable and

still carries.

Name: generateNextAssignments

Input: $[("$a$",$ false$)"$b$",$ false$)]$

Output: $([("$a$",$ false$)"$b$",$ true$)],$ false$)$

Input: $[("$a$",$ false$)"$b$",$ true$)]$

Output: $([("$a$",$ true$)"$b$",$ false$)],$ false$)$

Input: $[("$a$",$ true$)"$b$",$ true$)]$

Output: $([("$a$",$ false$)"$b$",$ false$)],$ true$)$

You will also have to implement the function called "LookupVar". This

function takes a assignment list of string$-$boolean tuples as well as a string, and

returns the boolean value associated with the given string in the assignment

list. Behavior for string values not in the assignment list will not be tested.

Name: LookupVar

Input: $[("$a$",$ false$)"$b$",$ true$)]"$a$"$

Output: false

$4$ Advanced Function Implementations

Now, we will handle the boolean satisfiability evaluation function and data

structures to represent the satisfiability funct

$4\mathrm{.}1$ The buildCNF function

Thi

N