SAT Part 4 — Solving 3CNF with C++ templates

~ afish

This is the fourth part of the SAT series. For your convenience you can find other parts in the table of contents in Part 1 — Boolean logic

Let’s use C++ templates to solve 3CNF SAT in compile-time.

The solution

First, let’s start with the code:

Problem definition

Let’s start with the main function which shows how to calculate exclusive or (XOR) using this approach:

We will create an instance of FullModel template that will encapsulate our parameters.

As a first parameter, we are going to pass a list of variables. Each variable can be either fixed (Variable<0> is false, Variable<1> is true) or free (Variable<2>). Fixed variables represent clauses for which we know the value. Free variables need to be solved by the solver. We’ll later refer to this list as list of variables and we’ll get its elements by the 0-based indices.

The second parameter is a list of constraints. Each constraint represents a disjunction of three variables. Each variable is either negated or left intact. Let’s take this line as an example:

This creates a constraint in which we take variables with numbers 0, 1, and 2. The first variable (with index 0) is negated, other ones are left intact. This constraint represents the following formula:

    \[\neg A \vee B \vee C\]

Helpers

We need some helper structures to represent concepts.

This represents a null type. It’s basically a sentinel to indicate end of list or missing values.

Next, we need a definition of linked list. We build it the typical way, with head and tail:

We need some helpers to operate on this list. We start with indexing:

We also need a way to reverse the list:

We assume that each list will end with a null type and will not have any null type in the middle.

Now, we need a literal that represents a number used for indexing inside the list:

In a similar way, we need two literals to represent true and false. They are used to represent the actual variable values:

Finally, we need to have a way to negate the variable value or leave it intact.

Representing variables

Let’s now define actual variables used in the model. They represent logical clauses that can be either true or false.

Let’s now sketch the general idea for how we’re going to solve the model. We’ll try to substitute each clause with the allowed values. For fixed variables, only one value is allowed (either 0 or 1). For free variables, we need to consider both values (0 and 1). Therefore, each variable will have two fields to store the available values. For fixed variables, both fields will have the same value. For free variables, the fields will have two different values.

Constraints

When solving the model, we’ll effectively examine each possible valuation. Therefore, constraints need to be resolved after valuating variables. Therefore, we’ll have a two-stage process: first, we’ll define constraints as which variables they should incorporate. In the second stage, the constraints will be bound with valuated variables.

To do that, we will need to calculate the CNF. Therefore, we’ll need to calculate the conjunction of all constraints, and disjunction of possible valuations. We define these as follows:

Conceptually, we’ll use them as following:

For each valuation, we’ll calculate the following:

This will effectively create a tree of valuations (thanks to disjunctions), and for each specific valuation we’ll verify if all 3CNF clauses are met (thanks to conjunction).

Notice that both conjunction and disjunction return a set of bound variables. We use that to retrieve the particular result. If a given valuation doesn’t meet the constraints, then the null type is returned.

Now, we need to actually be able to check if a particular 3CNF is solved. We do it like this:

This is quite straightforward. We take the 3CNF and check if any variable is true.

Now, we need to bound the constraints with the variables. To do that, we take the variable by its index, negate it if needed, and use in the 3CNF:

I imagine this part can be simplified somehow (with even more templates and higher-kinded templates).

Model

We now have everything to define the model. A model is a structure with 4 elements: list of variables, list of bound variables (variables with valuation), list of constraints, and a list of bound constraints:

We don’t want the user to provide all the values, as we just need the variables and constraints. Therefore, we have the following wrapper:

Now, the plan of action. For the exclusive or example, we start with something like this:

First, we add two more empty parameters. We also reverse the list of variables because we’ll reverse it later when evaluating:

Now, we want to iterate over variables until the list is empty. For each iteration, we want to use disjunction to split into two subtrees:

So, the very first step of evaluation will take first variable and generate this first subtree:

You can see that we removed one unbound variable (from the first list) and added one bound variable (to the second list). We also need to do the same for the other possible value of the variable, so we generate another subtree:

Next steps are similar, but both generated subtrees will be the same (as variables are fixed). Ultimately, we end up with something like this:

We bound all the variables. Now, we need to do the same for constraints:

In the first step, we take the first constraint and bound it with the variables to get something like this:

We do the same for all the constraints, and finally end up with this:

We repeat a lot, but that’s not a problem.

Finally, we can start evaluating the constraints:

We unwrap the first constraint and turn it into a conjunction. Effectively, we’ll build a structure of this:

And now we can calculate the conjunctions. If the second parameter is empty model, then we simply return bound variables:

Now, we need to refer back to the definition of conjunction we already saw:

You can see that we’ll get some variables as a second parameter, and we’ll need to evaluate the first parameter which is BoundConstraint. We already saw how it’s done:

And here is where the magic happens. We extract variables from the list, we negate them accordingly, and then use the 3CNF logic:

And we can see this constraint isn’t met. We’ll therefore return LiteralFalse back to Conjunction above and this will in turn return NullType up the tree. You can trace the recursive calls further to figure out what happens next.

Printing

Last thing is printing. It’s rather straighforward:

This simply prints the structure. The solution to SAT is calculated in the compilation time. Printing happens in runtime, so you need to run the application to get the precalculated result.

Summary

We already saw how to reduce ILP to 0-1 ILP, then to 3CNF SAT, and now we can calculate that using C++ templates. Therefore, we can solve our ILP problems using C++ compiler.