Boolean formula - marcbenedi/SAT-tfg GitHub Wiki

Features
- Boolean formulas representation
- CNF encodings
  - Tseytin transformation
  - Extracting primes transformation
  - Mix transformation
- Execute a SAT Solver
- BDD conversion
Examples

Features

Boolean formulas representation

This feature allows the representation of Boolean formulas. The class BoolFunc is the one with this responsibility.

#include "BoolFunc.h"

Formula a = BoolFunc::newLit("a");

This creates a Boolean formula with one literal, a. To manipulate Boolean formulae always use Formula. BoolFunc is only used to declare literals.

#include "BoolFunc.h"

Formula a = BoolFunc::newLit("a");
Formula f = !a;

This creates a Boolean formula f=not a.

As you can see, the operator can be used to build formulas. Currently, the supported operators are: NOT, AND, and OR. (XOR in progress).

#include "BoolFunc.h"

Formula a = BoolFunc::newLit("a");
Formula b = BoolFunc::newLit("b");
Formula f = a*b; //AND
f = a+b; //OR
a += b; // a = a + b
a *= b; //a = a * b

CNF encodings

Three encodings are implemented:

Tseytin transformation

#include "CnfConverter.h"

Formula f = ...;
Cnf cnf = CnfConverter::tseitin(f);

Extracting primes transformation

#include "CnfConverter.h"
#include "BDDConverter.h"

Formula f = ...;
BDD bdd = BDDConverter::convertFormula(f);
Cnf cnf = CnfConverter::convertToCnf(bdd);

Mix transformation

#include "MixCNFConverter.h"
#include "BDDConverter.h"

Formula f = ...;

MixCNFConverter m = MixCNFConverter();
m.convert(f);
Cnf result = m.getResult();

Execute a SAT Solver

#include "SatSolver.h"

Cnf cnf = ...;
std::cout << SatSolver::solve2(cnf) << std::endl;

BDD conversion

#include "BDDConverter.h"

Formula f = ...;
BDD bdd = BDDConverter::convertFormula(f);