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:

#include <iostream>

using namespace std;

// ============================

class NullType {};

// ============================

template <class T, class U>
struct Typelist
{
	typedef T Head;
	typedef U Tail;
};

// ============================

template <class TList, unsigned int index> struct TypeAt;
template <class Head, class Tail>
struct TypeAt<Typelist<Head, Tail>, 0>
{
	typedef Head Result;
};
template <class Head, class Tail, unsigned int i>
struct TypeAt<Typelist<Head, Tail>, i>
{
	typedef typename TypeAt<Tail, i - 1>::Result Result;
};

// ============================

template <class TList, class TAggregated> struct ReversedTypelist;
template<class TAggregated>
struct ReversedTypelist<NullType, TAggregated>{
	typedef TAggregated Result;
};
template <class Head, class Tail, class TAggregated>
struct ReversedTypelist<Typelist<Head, Tail>, TAggregated>
{
	typedef typename ReversedTypelist<Tail, Typelist<Head, TAggregated> >::Result Result;
};

// ============================

template<int v> struct Literal {
	enum {
		value = v
	};
};

struct LiteralTrue {
	enum {
		value = 1
	};
};

struct LiteralFalse {
	enum {
		value = 0
	};
};

// ============================


template<typename T> struct Id { typedef T Result; };
template<typename T> struct Negated {};
template<> struct Negated<LiteralTrue> { typedef LiteralFalse Result; };
template<> struct Negated<LiteralFalse> { typedef LiteralTrue Result; };




// ============================

template<int i>
struct Variable {};

template<>
struct Variable<0> {
	typedef LiteralFalse value1;
	typedef LiteralFalse value2;
};

template<>
struct Variable<1> {
	typedef LiteralTrue value1;
	typedef LiteralTrue value2;
};

template<>
struct Variable<2> {
	typedef LiteralFalse value1;
	typedef LiteralTrue value2;
};

// ============================

template<typename Constraint, typename BoundVariables> struct Conjunction { };
template<typename BoundVariables> struct Conjunction<LiteralFalse, BoundVariables> { typedef NullType Result; };
template<typename BoundVariables> struct Conjunction<LiteralTrue, BoundVariables> { typedef BoundVariables Result; };

template<typename BoundVariables1, typename BoundVariables2> struct Disjunction { typedef BoundVariables1 Result; };
template<> struct Disjunction<NullType, NullType> { typedef NullType Result; };
template<typename BoundVariables1> struct Disjunction<BoundVariables1, NullType> { typedef BoundVariables1 Result; };
template<typename BoundVariables2> struct Disjunction<NullType, BoundVariables2> { typedef BoundVariables2 Result; };

// ============================


// ============================
// Constraints with actual calculation
// This is where we check if SAT clauses (Variables) really satisfy a particular constraint
template<typename AOrNegated, typename BOrNegated, typename COrNegated> struct Constraint {};

template<typename A, typename B, typename C> struct ThreeClause { };
template<> struct ThreeClause<LiteralFalse, LiteralFalse, LiteralFalse> { typedef LiteralFalse value; };
template<> struct ThreeClause<LiteralFalse, LiteralFalse, LiteralTrue> { typedef LiteralTrue value; };
template<> struct ThreeClause<LiteralFalse, LiteralTrue, LiteralFalse> { typedef LiteralTrue value; };
template<> struct ThreeClause<LiteralFalse, LiteralTrue, LiteralTrue> { typedef LiteralTrue value; };
template<> struct ThreeClause<LiteralTrue, LiteralFalse, LiteralFalse> { typedef LiteralTrue value; };
template<> struct ThreeClause<LiteralTrue, LiteralFalse, LiteralTrue> { typedef LiteralTrue value; };
template<> struct ThreeClause<LiteralTrue, LiteralTrue, LiteralFalse> { typedef LiteralTrue value; };
template<> struct ThreeClause<LiteralTrue, LiteralTrue, LiteralTrue> { typedef LiteralTrue value; };

// ============================




// ============================


// ============================
// BoundConstraints
// Extracts referenced Variables and calculates literal representing the result of logical operation


template<typename ConstraintType, typename BoundVariables> struct BoundConstraint {};
template<int A, int B, int C, typename BoundVariables>
struct BoundConstraint<Constraint<Id<Literal<A> >, Id<Literal<B> >, Id<Literal<C> > >, BoundVariables> {
	typedef typename ThreeClause<
		typename Id<typename TypeAt<BoundVariables, A>::Result>::Result,
		typename Id<typename TypeAt<BoundVariables, B>::Result>::Result,
		typename Id<typename TypeAt<BoundVariables, C>::Result>::Result
	>::value value;
};
template<int A, int B, int C, typename BoundVariables>
struct BoundConstraint<Constraint<Id<Literal<A> >, Id<Literal<B> >, Negated<Literal<C> > >, BoundVariables> {
	typedef typename ThreeClause<
		typename Id<typename TypeAt<BoundVariables, A>::Result>::Result,
		typename Id<typename TypeAt<BoundVariables, B>::Result>::Result,
		typename Negated<typename TypeAt<BoundVariables, C>::Result>::Result
	>::value value;
};
template<int A, int B, int C, typename BoundVariables>
struct BoundConstraint<Constraint<Id<Literal<A> >, Negated<Literal<B> >, Id<Literal<C> > >, BoundVariables> {
	typedef typename ThreeClause<
		typename Id<typename TypeAt<BoundVariables, A>::Result>::Result,
		typename Negated<typename TypeAt<BoundVariables, B>::Result>::Result,
		typename Id<typename TypeAt<BoundVariables, C>::Result>::Result
	>::value value;
};
template<int A, int B, int C, typename BoundVariables>
struct BoundConstraint<Constraint<Id<Literal<A> >, Negated<Literal<B> >, Negated<Literal<C> > >, BoundVariables> {
	typedef typename ThreeClause<
		typename Id<typename TypeAt<BoundVariables, A>::Result>::Result,
		typename Negated<typename TypeAt<BoundVariables, B>::Result>::Result,
		typename Negated<typename TypeAt<BoundVariables, C>::Result>::Result
	>::value value;
};
template<int A, int B, int C, typename BoundVariables>
struct BoundConstraint<Constraint<Negated<Literal<A> >, Id<Literal<B> >, Id<Literal<C> > >, BoundVariables> {
	typedef typename ThreeClause<
		typename Negated<typename TypeAt<BoundVariables, A>::Result>::Result,
		typename Id<typename TypeAt<BoundVariables, B>::Result>::Result,
		typename Id<typename TypeAt<BoundVariables, C>::Result>::Result
	>::value value;
};
template<int A, int B, int C, typename BoundVariables>
struct BoundConstraint<Constraint<Negated<Literal<A> >, Id<Literal<B> >, Negated<Literal<C> > >, BoundVariables> {
	typedef typename ThreeClause<
		typename Negated<typename TypeAt<BoundVariables, A>::Result>::Result,
		typename Id<typename TypeAt<BoundVariables, B>::Result>::Result,
		typename Negated<typename TypeAt<BoundVariables, C>::Result>::Result
	>::value value;
};
template<int A, int B, int C, typename BoundVariables>
struct BoundConstraint<Constraint<Negated<Literal<A> >, Negated<Literal<B> >, Id<Literal<C> > >, BoundVariables> {
	typedef typename ThreeClause<
		typename Negated<typename TypeAt<BoundVariables, A>::Result>::Result,
		typename Negated<typename TypeAt<BoundVariables, B>::Result>::Result,
		typename Id<typename TypeAt<BoundVariables, C>::Result>::Result
	>::value value;
};
template<int A, int B, int C, typename BoundVariables>
struct BoundConstraint<Constraint<Negated<Literal<A> >, Negated<Literal<B> >, Negated<Literal<C> > >, BoundVariables> {
	typedef typename ThreeClause<
		typename Negated<typename TypeAt<BoundVariables, A>::Result>::Result,
		typename Negated<typename TypeAt<BoundVariables, B>::Result>::Result,
		typename Negated<typename TypeAt<BoundVariables, C>::Result>::Result
	>::value value;
};

// ============================


// ============================
// Model

template<typename Variables, typename BoundVariables, typename Constraints, typename BoundConstraints> struct Model {};

// Model with no BoundConstraints just returns the bound variables
template<typename BoundVariables>
struct Model<NullType, BoundVariables, NullType, NullType>{
	typedef BoundVariables Result;
};

// Recursively calculates AND between current BoundConstraint and the rest of BoundConstraints
// Effectively removes one element from BoundConstraints, and returns Conjunction of the removed BoundConstraint and the rest
template<typename BoundVariables, typename Head, typename Tail>
struct Model<NullType, BoundVariables, NullType, Typelist<Head, Tail> > {
	typedef typename Conjunction<
		typename Head::value,
		typename Model<NullType, BoundVariables, NullType, Tail>::Result
	>::Result Result;
};

// Recursively bounds Constraint with BoundVariables
// Effectively removes one element from Constraints, and adds one element to BoundConstraints
template<typename BoundVariables, typename Head, typename Tail, typename BoundConstraints>
struct Model<NullType, BoundVariables, Typelist<Head, Tail>, BoundConstraints> {
	typedef typename Model<NullType, BoundVariables, Tail, Typelist<BoundConstraint<Head, BoundVariables>, BoundConstraints> >::Result Result;
};

// Takes first Variable, branches into two trees for the first value of the variable and the second value
// Effectively removes one element from Variables, and adds one element to BoundVariables
template<typename Head, typename Tail, typename BoundVariables, typename Constraints, typename BoundConstraints>
struct Model<Typelist<Head, Tail>, BoundVariables, Constraints, BoundConstraints> {
	typedef typename Disjunction<
		typename Model<Tail, Typelist<typename Head::value1, BoundVariables>, Constraints, BoundConstraints>::Result,
		typename Model<Tail, Typelist<typename Head::value2, BoundVariables>, Constraints, BoundConstraints>::Result
	>::Result Result;
};

template<typename Variables, typename Constraints>
struct FullModel {
	typedef typename Model<typename ReversedTypelist<Variables, NullType>::Result, NullType, Constraints, NullType>::Result Result;
};

// ============================


// ============================
// Print helpers

template<typename T> struct Print {};
template<typename Head, typename Tail>
struct Print<Typelist<Head, Tail> >{
	void print(){
		std::cout<<Head::value<<std::endl;
		Print<Tail>().print();
	}
};
template<>
struct Print<NullType>{
	void print(){
		std::cout<<"NullType"<<std::endl;
	}
};

// ============================


int main() {
	// XOR
	Print<typename FullModel< 
		Typelist<Variable<1>, Typelist<Variable<0>, Typelist<Variable<2>, NullType> > >,
			Typelist<Constraint<Negated<Literal<0> >, Id<Literal<1> >, Id<Literal<2> > >,
			Typelist<Constraint<Id<Literal<0> >, Negated<Literal<1> >, Id<Literal<2> > >,
			Typelist<Constraint<Id<Literal<0> >, Id<Literal<1> >, Negated<Literal<2> > >,
			Typelist<Constraint<Negated<Literal<0> >, Negated<Literal<1> >, Negated<Literal<2> > >,
				NullType> > > >
	>::Result>().print();
}

Problem definition

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

Print<typename FullModel< 
	Typelist<Variable<1>, Typelist<Variable<0>, Typelist<Variable<2>, NullType> > >,
		Typelist<Constraint<Negated<Literal<0> >, Id<Literal<1> >, Id<Literal<2> > >,
		Typelist<Constraint<Id<Literal<0> >, Negated<Literal<1> >, Id<Literal<2> > >,
		Typelist<Constraint<Id<Literal<0> >, Id<Literal<1> >, Negated<Literal<2> > >,
		Typelist<Constraint<Negated<Literal<0> >, Negated<Literal<1> >, Negated<Literal<2> > >,
			NullType> > > >
>::Result>().print();

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:

Constraint<Negated<Literal<0> >, Id<Literal<1> >, Id<Literal<2> >

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:

*** QuickLaTeX cannot compile formula:
\[\neg A \vee B \vee C\]

*** Error message:
Cannot connect to QuickLaTeX server: cURL error 6: Could not resolve host: www.quicklatex.com
Please make sure your server/PHP settings allow HTTP requests to external resources ("allow_url_fopen", etc.)
These links might help in finding solution:
http://wordpress.org/extend/plugins/core-control/
http://wordpress.org/support/topic/an-unexpected-http-error-occurred-during-the-api-request-on-wordpress-3?replies=37

Helpers

We need some helper structures to represent concepts.

class NullType {};

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:

template <class T, class U>
struct Typelist
{
	typedef T Head;
	typedef U Tail;
};

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

template <class TList, unsigned int index> struct TypeAt;
template <class Head, class Tail>
struct TypeAt<Typelist<Head, Tail>, 0>
{
	typedef Head Result;
};
template <class Head, class Tail, unsigned int i>
struct TypeAt<Typelist<Head, Tail>, i>
{
	typedef typename TypeAt<Tail, i - 1>::Result Result;
};

We also need a way to reverse the list:

template <class TList, class TAggregated> struct ReversedTypelist;
template<class TAggregated>
struct ReversedTypelist<NullType, TAggregated>{
	typedef TAggregated Result;
};
template <class Head, class Tail, class TAggregated>
struct ReversedTypelist<Typelist<Head, Tail>, TAggregated>
{
	typedef typename ReversedTypelist<Tail, Typelist<Head, TAggregated> >::Result Result;
};

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:

template<int v> struct Literal {
	enum {
		value = v
	};
};

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

struct LiteralTrue {
	enum {
		value = 1
	};
};

struct LiteralFalse {
	enum {
		value = 0
	};
};

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

template<typename T> struct Id { typedef T Result; };
template<typename T> struct Negated {};
template<> struct Negated<LiteralTrue> { typedef LiteralFalse Result; };
template<> struct Negated<LiteralFalse> { typedef LiteralTrue Result; };

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.

template<int i>
struct Variable {};

template<>
struct Variable<0> {
	typedef LiteralFalse value1;
	typedef LiteralFalse value2;
};

template<>
struct Variable<1> {
	typedef LiteralTrue value1;
	typedef LiteralTrue value2;
};

template<>
struct Variable<2> {
	typedef LiteralFalse value1;
	typedef LiteralTrue value2;
};

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:

template<typename Constraint, typename BoundVariables> struct Conjunction { };
template<typename BoundVariables> struct Conjunction<LiteralFalse, BoundVariables> { typedef NullType Result; };
template<typename BoundVariables> struct Conjunction<LiteralTrue, BoundVariables> { typedef BoundVariables Result; };

template<typename BoundVariables1, typename BoundVariables2> struct Disjunction { typedef BoundVariables1 Result; };
template<> struct Disjunction<NullType, NullType> { typedef NullType Result; };
template<typename BoundVariables1> struct Disjunction<BoundVariables1, NullType> { typedef BoundVariables1 Result; };
template<typename BoundVariables2> struct Disjunction<NullType, BoundVariables2> { typedef BoundVariables2 Result; };

Conceptually, we’ll use them as following:

Disjunction(first valuation, Disjunction(second valuation, Disjunction(third valuation, ...)))

For each valuation, we’ll calculate the following:

Conjunction(first constraint, Conjunction(second constraint, Conjunction(third constraint, ...)))

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:

template<typename AOrNegated, typename BOrNegated, typename COrNegated> struct Constraint {};

template<typename A, typename B, typename C> struct ThreeClause { };
template<> struct ThreeClause<LiteralFalse, LiteralFalse, LiteralFalse> { typedef LiteralFalse value; };
template<> struct ThreeClause<LiteralFalse, LiteralFalse, LiteralTrue> { typedef LiteralTrue value; };
template<> struct ThreeClause<LiteralFalse, LiteralTrue, LiteralFalse> { typedef LiteralTrue value; };
template<> struct ThreeClause<LiteralFalse, LiteralTrue, LiteralTrue> { typedef LiteralTrue value; };
template<> struct ThreeClause<LiteralTrue, LiteralFalse, LiteralFalse> { typedef LiteralTrue value; };
template<> struct ThreeClause<LiteralTrue, LiteralFalse, LiteralTrue> { typedef LiteralTrue value; };
template<> struct ThreeClause<LiteralTrue, LiteralTrue, LiteralFalse> { typedef LiteralTrue value; };
template<> struct ThreeClause<LiteralTrue, LiteralTrue, LiteralTrue> { typedef LiteralTrue value; };

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:

template<typename ConstraintType, typename BoundVariables> struct BoundConstraint {};
template<int A, int B, int C, typename BoundVariables>
struct BoundConstraint<Constraint<Id<Literal<A> >, Id<Literal<B> >, Id<Literal<C> > >, BoundVariables> {
	typedef typename ThreeClause<
		typename Id<typename TypeAt<BoundVariables, A>::Result>::Result,
		typename Id<typename TypeAt<BoundVariables, B>::Result>::Result,
		typename Id<typename TypeAt<BoundVariables, C>::Result>::Result
	>::value value;
};
template<int A, int B, int C, typename BoundVariables>
struct BoundConstraint<Constraint<Id<Literal<A> >, Id<Literal<B> >, Negated<Literal<C> > >, BoundVariables> {
	typedef typename ThreeClause<
		typename Id<typename TypeAt<BoundVariables, A>::Result>::Result,
		typename Id<typename TypeAt<BoundVariables, B>::Result>::Result,
		typename Negated<typename TypeAt<BoundVariables, C>::Result>::Result
	>::value value;
};
template<int A, int B, int C, typename BoundVariables>
struct BoundConstraint<Constraint<Id<Literal<A> >, Negated<Literal<B> >, Id<Literal<C> > >, BoundVariables> {
	typedef typename ThreeClause<
		typename Id<typename TypeAt<BoundVariables, A>::Result>::Result,
		typename Negated<typename TypeAt<BoundVariables, B>::Result>::Result,
		typename Id<typename TypeAt<BoundVariables, C>::Result>::Result
	>::value value;
};
template<int A, int B, int C, typename BoundVariables>
struct BoundConstraint<Constraint<Id<Literal<A> >, Negated<Literal<B> >, Negated<Literal<C> > >, BoundVariables> {
	typedef typename ThreeClause<
		typename Id<typename TypeAt<BoundVariables, A>::Result>::Result,
		typename Negated<typename TypeAt<BoundVariables, B>::Result>::Result,
		typename Negated<typename TypeAt<BoundVariables, C>::Result>::Result
	>::value value;
};
template<int A, int B, int C, typename BoundVariables>
struct BoundConstraint<Constraint<Negated<Literal<A> >, Id<Literal<B> >, Id<Literal<C> > >, BoundVariables> {
	typedef typename ThreeClause<
		typename Negated<typename TypeAt<BoundVariables, A>::Result>::Result,
		typename Id<typename TypeAt<BoundVariables, B>::Result>::Result,
		typename Id<typename TypeAt<BoundVariables, C>::Result>::Result
	>::value value;
};
template<int A, int B, int C, typename BoundVariables>
struct BoundConstraint<Constraint<Negated<Literal<A> >, Id<Literal<B> >, Negated<Literal<C> > >, BoundVariables> {
	typedef typename ThreeClause<
		typename Negated<typename TypeAt<BoundVariables, A>::Result>::Result,
		typename Id<typename TypeAt<BoundVariables, B>::Result>::Result,
		typename Negated<typename TypeAt<BoundVariables, C>::Result>::Result
	>::value value;
};
template<int A, int B, int C, typename BoundVariables>
struct BoundConstraint<Constraint<Negated<Literal<A> >, Negated<Literal<B> >, Id<Literal<C> > >, BoundVariables> {
	typedef typename ThreeClause<
		typename Negated<typename TypeAt<BoundVariables, A>::Result>::Result,
		typename Negated<typename TypeAt<BoundVariables, B>::Result>::Result,
		typename Id<typename TypeAt<BoundVariables, C>::Result>::Result
	>::value value;
};
template<int A, int B, int C, typename BoundVariables>
struct BoundConstraint<Constraint<Negated<Literal<A> >, Negated<Literal<B> >, Negated<Literal<C> > >, BoundVariables> {
	typedef typename ThreeClause<
		typename Negated<typename TypeAt<BoundVariables, A>::Result>::Result,
		typename Negated<typename TypeAt<BoundVariables, B>::Result>::Result,
		typename Negated<typename TypeAt<BoundVariables, C>::Result>::Result
	>::value value;
};

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:

template<typename Variables, typename BoundVariables, typename Constraints, typename BoundConstraints> struct Model {};

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:

template<typename Variables, typename Constraints>
struct FullModel {
	typedef typename Model<typename ReversedTypelist<Variables, NullType>::Result, NullType, Constraints, NullType>::Result Result;
};

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

FullModel(
  [fixed variable 0 with value true; fixed variable 1 with value false; free variable 2],
  [
    Constraint(!0, 1, 2),
    Constraint(0, !1, 2),
    Constraint(0, 1, !2),
    Constraint(!0, !1, !2)
  ]
)

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

Model(
  [free variable 2, fixed variable 1 with value false, fixed variable 0 with value true],
  [], // valuated variables
  [
    Constraint(!0, 1, 2),
    Constraint(0, !1, 2),
    Constraint(0, 1, !2),
    Constraint(!0, !1, !2)
  ],
  [] // bound constraints
)

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:

template<typename Head, typename Tail, typename BoundVariables, typename Constraints, typename BoundConstraints>
struct Model<Typelist<Head, Tail>, BoundVariables, Constraints, BoundConstraints> {
	typedef typename Disjunction<
		typename Model<Tail, Typelist<typename Head::value1, BoundVariables>, Constraints, BoundConstraints>::Result,
		typename Model<Tail, Typelist<typename Head::value2, BoundVariables>, Constraints, BoundConstraints>::Result
	>::Result Result;
};

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

Model(
  [fixed variable 1 with value false, fixed variable 0 with value true],
  [bound variable 2 with value false], // valuated variables
  [
    Constraint(!0, 1, 2),
    Constraint(0, !1, 2),
    Constraint(0, 1, !2),
    Constraint(!0, !1, !2)
  ],
  [] // bound constraints
)

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:

Model(
  [fixed variable 1 with value false, fixed variable 0 with value true],
  [bound variable 2 with value true], // valuated variables
  [
    Constraint(!0, 1, 2),
    Constraint(0, !1, 2),
    Constraint(0, 1, !2),
    Constraint(!0, !1, !2)
  ],
  [] // bound constraints
)

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

Model(
  [],
  [variable 0 with value true, variable 1 with value false, variable 2 with value false], // valuated variables
  [
    Constraint(!0, 1, 2),
    Constraint(0, !1, 2),
    Constraint(0, 1, !2),
    Constraint(!0, !1, !2)
  ],
  [] // bound constraints
)

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

template<typename BoundVariables, typename Head, typename Tail, typename BoundConstraints>
struct Model<NullType, BoundVariables, Typelist<Head, Tail>, BoundConstraints> {
	typedef typename Model<NullType, BoundVariables, Tail, Typelist<BoundConstraint<Head, BoundVariables>, BoundConstraints> >::Result Result;
};

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

Model(
  [],
  [bound variable 0 with value true, bound variable 1 with value false, bound variable 2 with value false], // valuated variables
  [    
    Constraint(0, !1, 2),
    Constraint(0, 1, !2),
    Constraint(!0, !1, !2)
  ],
  [
    BoundConstraint(!0, 1, 2) with bound variables(true, false, false),
  ] // bound constraints
)

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

Model(
  [],
  [bound variable 0 with value true, bound variable 1 with value false, bound variable 2 with value false], // valuated variables
  [],
  [
    BoundConstraint(0, !1, 2) with bound variables(true, false, false),
    BoundConstraint(0, 1, !2) with bound variables(true, false, false),
    BoundConstraint(!0, !1, !2) with bound variables(true, false, false),
    BoundConstraint(!0, 1, 2) with bound variables(true, false, false),
  ] // bound constraints
)

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

Finally, we can start evaluating the constraints:

template<typename BoundVariables, typename Head, typename Tail>
struct Model<NullType, BoundVariables, NullType, Typelist<Head, Tail> > {
	typedef typename Conjunction<
		typename Head::value,
		typename Model<NullType, BoundVariables, NullType, Tail>::Result
	>::Result Result;
};

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

Conjunction(BoundConstraint(0, !1, 2) with bound variables(true, false, false), Conjunction(BoundConstraint(0, 1, !2) with bound variables(true, false, false), Conjunction(BoundConstraint(!0, !1, !2) with bound variables(true, false, false), Conjunction(BoundConstraint(!0, 1, 2) with bound variables(true, false, false), Model([],  [bound variable 0 with value true, bound variable 1 with value false, bound variable 2 with value false], [], [])))))

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

template<typename BoundVariables>
struct Model<NullType, BoundVariables, NullType, NullType>{
	typedef BoundVariables Result;
};

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

template<typename BoundVariables> struct Conjunction<LiteralFalse, BoundVariables> { typedef NullType Result; };
template<typename BoundVariables> struct Conjunction<LiteralTrue, BoundVariables> { typedef BoundVariables Result; };

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:

template<int A, int B, int C, typename BoundVariables>
struct BoundConstraint<Constraint<Negated<Literal<A> >, Id<Literal<B> >, Id<Literal<C> > >, BoundVariables> {
	typedef typename ThreeClause<
		typename Negated<typename TypeAt<BoundVariables, A>::Result>::Result,
		typename Id<typename TypeAt<BoundVariables, B>::Result>::Result,
		typename Id<typename TypeAt<BoundVariables, C>::Result>::Result
	>::value value;
};

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

template<> struct ThreeClause<LiteralFalse, LiteralFalse, LiteralFalse> { typedef LiteralFalse value; };

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:

template<typename T> struct Print {};
template<typename Head, typename Tail>
struct Print<Typelist<Head, Tail> >{
	void print(){
		std::cout<<Head::value<<std::endl;
		Print<Tail>().print();
	}
};
template<>
struct Print<NullType>{
	void print(){
		std::cout<<"NullType"<<std::endl;
	}
};

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.

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

Today we are going to reduce ILP to SAT.

Introduction

Depending on the solver, typical ILP supports the following operations:

1. Adding two variables
2. Negating variable
3. Subtracting variables
4. Multiplying variable by constant
5. Dividing variable by constant
6. Adding equality constraint
7. Adding greater or equal constraint
8. Adding less or equal constraint
9. Adding goal function
10. Marking variable as integer

Some operations are obviously represented in SAT while others cannot be easily reduced.

If we assume that integers are of a specific width – which is not a crazy assumption as we use computers anyway and they do use fixed width numbers for increased performance – then we can implement operations 1-3 easily.

Operation 4 can be easily implemented as well assuming we work with integers only.

Operation 5 is tricky as the result may not be an integer so we can’t represent it properly.

Operation 6 is straightforward. So are operations 7 and 8 when we use slack variables.

Operation 9 is something we cannot implement in pure SAT. There is MAXSAT where we can optimize for a goal function, though.

Operation 10 is obvious.

Reduction

First we reduce the ILP problem to its canonical form. We replace all constraints with where . Same for – we change it to . We can stay with negative variables or replace them with subtraction and a slack variable.

Next, we reduce the canonical form to 0-1 ILP. We take every integer and replace it with bits.

Then, we remove the goal function. Ultimately we end up with a matrix of equalities of integer variables.

Now, we implement operations 1-4 and 6 using the approach from previous parts of this series.

Analysis

How slow is this going to be? For each integer we effectively introduce 32 clauses. For multiplication we need to add additional 32 partial sums which we then add together to get the result.

So, when we reduce the ILP model multiplying two integers with 27 bits width we end up with 2260029 clauses and 8409792 conjunctions. The model can be then solved in less than 2 minutes on my personal laptop. The DIMACS model has 210 MBs. For exponentiation it’s even bigger – 25375974 variables, 94454003 conjunctions, and 2.5 GBs.

Similarly, Nondeterministic Turing Machine for palindromes (the one we implemented in ILP) has 22123252 variables, 79175097 conjunctions, and 2.1 GBs.

That’s big. But it works and now we can use plenty of SAT solvers to calculate ILP models.

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

Today we’re going to implement some basic arithmetic in SAT.

Addition

We assume numbers are represented using U2 scheme. All we need to do is to implement a full-adder. We can use the following code (it comes from my custom SAT solver for MilpManager wrapper):

protected override IVariable InternalSumVariables(IVariable first, IVariable second, Domain domain)
{
	var variable = CreateAnonymous(domain).Typed();

	int previousCarryIndex = ++VariablesCount;
	Unset(previousCarryIndex);

	for (int i = 0; i < Settings.BitsCount; ++i)
	{
		int a = first.Typed().SourceVariables[i];
		int b = second.Typed().SourceVariables[i];

		int halfCarryIndex = ++VariablesCount;
		And(a, b, halfCarryIndex);

		int halfSumIndex = ++VariablesCount;
		Xor(a, b, halfSumIndex);

		int fullSumIndex = variable.Typed().SourceVariables[i];
		Xor(halfSumIndex, previousCarryIndex, fullSumIndex);

		int secondCarryIndex = ++VariablesCount;
		And(halfSumIndex, previousCarryIndex, secondCarryIndex);

		int fullCarryIndex = ++VariablesCount;
		Or(halfCarryIndex, secondCarryIndex, fullCarryIndex);

		previousCarryIndex = fullCarryIndex;
	}

	return variable;
}

Let’s unwrap this magic one by one.

First, in line 3 we create a variable for holding the result. We assume it creates enough clauses for integer.

Next, we clear previous carry index (the input to the full adder).

In lines 8-29 we implement a loop which adds bits one by one. We create a new carry in line 13 and then calculate it by using conjunction.

Next, in line 17 we calculate the half-add by xoring bits.

Next, we need to propagate carry properly. In lines 23-26 we do the math.

Negation

Negation is very simple. First, we negate all bits, and then we add one (using the addition scheme from previous section).

Subtraction

Super simple, just add negated number.

Multiplication

We’re going to cheat a little. Since we represent numbers with fixed number of bits, we can ignore the overflow and just do the long multiplication, like this:

protected override IVariable InternalMultiplyVariableByConstant(IVariable variable, IVariable constant, Domain domain)
{
	var variableTyped = variable.Typed();
	var constantTyped = constant.Typed();

	List<IVariable> partialSums = new List<IVariable>();

	for (int i = 0; i < Settings.BitsCount; ++i)
	{
		var partialSum = variable.MilpManager.CreateAnonymous(Domain.AnyInteger).Typed();

		for (int j = 0; j < i; ++j)
		{
			constraints.Add(string.Format("-{0} 0", partialSum.SourceVariables[j]));
		}

		for (int j = 0; i + j < Settings.BitsCount; ++j)
		{
			And(constantTyped.SourceVariables[i], variableTyped.SourceVariables[j], partialSum.SourceVariables[i + j]);
		}

		partialSums.Add(partialSum);
	}

	var total = variable.MilpManager.Operation<Addition>(partialSums.ToArray());

	return total;
}

This is the first part of the SAT series. For your convenience you can find other parts using the links below:
SAT Part 1 — Boolean logic
SAT Part 2 — Arithmetic
SAT Part 3 — Reducing ILP to SAT
SAT Part 4 — Solving 3CNF with C++ templates

Today we are going to implement some Boolean logic in SAT.

Equal and not equal

Let’s begin with equality. We have a clause and we want to add clause which is equal to . This means that if is in some assignment then is as well. We get this with the following:

a -b 0
-a b 0

If is then first clause is satisfied. For the second to be satisfied must be as well.
However, if is zero then second clause is satisfied but the first one is not. In that case must be so must be .

For inequality (or binary negation) we have the following:

a b 0
-a -b 0

When is then we need to have set to in second clause so is . When is then must be in the first clause.

Conjunction

We have clauses and , and we want to have clause being conjunction of and :

-a -b c 0
-a b -c 0
a -b -c 0
a b -c 0

For we have last clause make being .
For third clause makes being .
For we have second clause doing the same.
Finally, for we have first clause which makes equal to .

Disjunction

Goes this way:

a b -c 0
-a b c 0
a -b c 0
-a -b c 0

For we have first clause making equal to . All other clauses cover other permutations.

XOR

For exclusive or we can use:

-a b c 0 
a -b c 0
a b -c 0
-a -b -c 0

For third clause makes . For fourth clause does the same. Similarly, for and we have first clause which makes .

Introducing numbers to the model

Let’s now say that we would like to introduce some constant integer to the model. What we need to do is represent it in U2 system and set flags accordingly.

Let’s take . We add one clause for each bit with the following constraints:

a_0 0
-a_1 0
a_2 0

You can see that this will correctly assign values to clauses and from now on we can use these clauses as bits of the number.

In the next part we will implement some arithmetic.