cppsat - Propositional Encodings in C++11

cppsat is C++11 library for specifying and solving propositional encodings. The MiniSat SAT solver is used as solver backend.

cppsat provides a Bit class for representing potentially unknown Boolean values. As Bit overloads many C++ operators, propositional encodings can be specified in a concise and natural way. cppsat also provides the Bits class as a collection of Bits that supports unsigned integer arithmetic. See cppsat.hpp for cppsat’s complete API.

Example

Specification of an adder circuit:

std::pair <Bit, Bit> halfAdder (const Bit& a, const Bit& b) {
  return std::make_pair (a != b, a && b);
}

std::pair <Bit, Bit> fullAdder ( const Bit& a, const Bit& b
                               , const Bit& c )
{
  auto ha1 = halfAdder (a, b);
  auto ha2 = halfAdder (ha1.first, c);

  return std::make_pair (ha2.first, ha1.second || ha2.second);
}

Call cppsat::solve to solve a propositional constraint:

int main () {
  Bit a, b, c;

  if (cppsat::solve (fullAdder (a, b, c).second == Bit (true))) {
    std::cout << "a: " << a << std::endl;
    std::cout << "b: " << b << std::endl;
    std::cout << "c: " << c << std::endl;
  }
  else {
    std::cout << "unsatisfiable\n";
  }
  return 0;
}

See more exemplary applications including a Sudoku solver and a N-Queens solver.

In order to build the examples, install MiniSat, get cppsat’s sources, and compile via:

g++ --std=c++11 cppsat.cpp examples/sudoku.cpp -lminisat

cppsat - Propositional Encodings in C++11

Example

Related Work