kaktusat

Introduction

This is a playground for learning about several topics that interests me, including satisfiability, SAT solving, proof theory and mathematical logic in general. Currently, it consists of the following:

• solver interface: a SAT solver interface with basic functionality such as creating new variables, adding clauses, solving and verifying instances. This interface is akin to those used in well-known solvers such as [1].

• encoders: encoders encode an instance of a problem into a satisfiability instance that can be readily used with a SAT solver. Such problems include cardinality contraints, graph coloring, circuits, etc. Encoders are not mutually exclusive, e.g. circuit encoders can be used incrementally for build an integer factorization instance. An encoder to read instances stored in external files in the DIMACS format is also included.

• transforms: transforms take an existing instance and transform it to an equivalent instance with desirable properties. For example, the sat3 transform takes an arbitrary k-CNF instance and transforms it to an equivalent 3-CNF instance.

• algorithms: algorithms to actually solve SAT instances. Most of them are named and implemented following [2] and are self-contained.

• demos: short programs illustrating the usage of the above.

• repl: a REPL for exploring basic logic computations interactively.

As I study and learn new things, this organization might change and new items will be added. Additional notes on exercises from [2] and diagrams can be found in doc.

The following sections provide more detail on specific components.

Algorithms

Currently the following algorithms are implemented (listed by their corresponding ID):

• A: implements Algorithm A (Satisfiability by backtracking), as presented in [2], page 28.
• A2: small variation of Algorithm A.
• Analyze: not really a solver, but rather an analyzer of instances, printing interesting information such as clause length statistics and redundant literals.
• B: implements Algorithm B (Satisfiability by watching), as presented in [2], page 31.
• C: implements Algorithm C (Satisfiability by CDCL), as presented in [2], page 68.
• D: implements Algorithm D (Satisfiability by cyclic DPLL), as presented in [2], page 33.
• I0: implements Algorithm I (Satisfiability by clause learning), as presented in [2], page 61. Or rather, a straightforward implementation of the algorithm description, since it's a family of algorithms rather than a specific one.
• NOP: a dummy solver that always returns UNKNOWN as result. It's useful for testing properties that do not need an actual solver, such as encoders and transformers.
• Z: the slowest solver ever. Literally tries every assignment.

Encoders

These are some of the provided encoders:

• basic: encoders for basic concepts: unit clauses, tautologies, contradictions.
• cardinality: encodes cardinality constraints such as "at most two of these variables can be true". It employs techniques described in [2], [3] and [4], among others. They serve as the basis of many other encoders and transforms.
• circuit: encodes common circuit functions, such as AND, OR and NOT gates. Serves as the basis for e.g. multiplication and factoring encoders. See Tseytin transformation and [5].
• dimacs: reads an instance from an external file in DIMACS CNF format.
• rand: generates a random k-CNF instance on N variables and M clauses.

The full list can be examined here.

Basic usage

Most of the code is written in C++ and uses the Bazel build system.

The solver can be used from a provided command-line application that takes the algorithm ID to use and the path to a DIMACS file in CNF format. For example:

bazel run -c opt //main -- C /path/to/instance.cnf

will try to solve the instance contained in the file /path/to/instance.cnf using Algorithm C (see [2]).

The solver can also be used programmatically. Here's a small example with comments:

#include <iostream>

#include "solver/solver.h"      // general solver interface
#include "solver/algorithm/c.h" // specific algorithm to use
#include "util/log.h"           // utilities for logging

int main() {
  util::InitLogging();

  // Create an instance of the solver.
  solver::algorithm::C solver;

  // Create a few new variables. Variables can be named arbitrarily.
  auto x1 = solver.NewVar("x1");
  auto x2 = solver.NewVar("x2");
  auto x3 = solver.NewVar("x3");
  auto x4 = solver.NewVar("x4");

  // Add a few clauses. Variables are implicitly converted to literals.
  // The ~ operator negates a literal.
  solver.AddClause({x1, x2, ~x3});
  solver.AddClause({x2, x3, ~x4});
  solver.AddClause({x3, x4, x1});
  solver.AddClause({x4, ~x1, x2});
  solver.AddClause({~x1, ~x2, x3});
  solver.AddClause({~x2, ~x3, x4});
  solver.AddClause({~x3, ~x4, ~x1});

  // Actually solve the instance.
  auto [res, sol] = solver.Solve();
  if (res == solver::Result::kSAT) {
    // Print the solution using the original variable names.
    std::cout << "SAT: " << solver.ToString(sol) << std::endl;
  } else {
    std::cout << "UNSAT" << std::endl;
  }

  return 0;
}

This example recreates the satisfiable instance R' from [2], page 4. It outputs:

SAT: ¬x1, x4, x2, x3

REPL

The REPL can be executed as follows:

bazel run -c opt //repl

It is useful for interactively exploring basic logic computations. The notation used mostly follows the one in [6] and [7].

Demos

A couple of demos are provided in demo:

• factor: encodes a factorization problem. Number to factorize is given as a program argument.
• life: encodes a bounded model checking (Conway's Game of Life) problem.
• sudoku: encodes a sudoku problem. Sudoku to solve is read from stdin.

Development usage

When developing, the following commands are handy.

For running all the tests:

bazel test //test:all

The current test suite includes unit tests for most algorithms and many of the encoders/transforms.

Additionally, a utility application for batch running a specific algorithm against all the CNF instance files in a directory is included:

bazel run -c opt //benchmark:batch -- D /path/to/instance/dir/

It will also verify results and output statistics about solve time.

References

[1] Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Theory and Applications of Satisfiability Testing. pp. 502–518. Springer Berlin Heidelberg (2004)

[2] Knuth, D. E.: The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability. Pearson Education (US) (2015)

[3] Sinz, C.: Towards an Optimal CNF Encoding of Boolean Cardinality Constraints. In: Principles and Practice of Constraint Programming - CP 2005. pp. 827–831. Springer Berlin Heidelberg (2005)

[4] Bailleux, O., Boufkhad, Y.: Efficient CNF Encoding of Boolean Cardinality Constraints. In: Principles and Practice of Constraint Programming – CP 2003. pp. 108–122. Springer Berlin Heidelberg (2003)

[5] Tseytin, G. S.: On the complexity of derivation in propositional calculus. In: (ed.)Slisenko, A. O. Studies in Constructive Mathematics and Mathematical Logic. pp. 115–125. Springer (1969)

[6] Krajícek, J.: Proof Complexity. Cambridge University Press (2019)

[7] Buss, S.: Handbook of Proof Theory. Elsevier, New York (1998)