Clone wiki

krtoolkit / Home



satVarious functionality for research in Satisfiability.
statsVarious statistical functions that are commonly used.
utilsUtilities for making experimental setup simplified.
planningLibraries for automated planning tasks.

Coming Soon

encodingProvides encodings between different problem types.
searchLibraries for backtracking and local search techniques.
vizGeneric libraries for visualization.


The krtoolkit contains a wide range of functionality, and as a consequence it has a large number of external dependencies. Rather than have users install every package the krtoolkit code depends on, the dependencies will silently fail and only print an error when code requiring them is executed. If you are only using a subset of the krtoolkit functionality, the following compatibility matrix will help figure out which packages are required:

Compatibility Matrix



Eventually this package will be included in the pypi repository for easy_install, but until then a bleeding-edge version can be installed by doing the following:

hg clone ssh://
cd krtoolkit
sudo python install

If you don't happen to have root, then an easy approach is to define a new location for python packages to be installed with dist utils:

  • Make a directory for all of your python packages:
mkdir ~/python
  • Include this in your python path, by adding the following to your .bashrc or equivalent:
export PYTHONPATH=~/python/lib/python/
  • Install the toolkit with the home option:
cd krtoolkit
python install --home=~/python

Note: It has only been tested on Linux so far, and requires mercurial to access.


Eventually there will be documentation / usage examples for all parts of the toolkit, but for now here's a small example on how to read in a 3SAT CNF file, print the clauses, change the formula, and write it back to a new file:

# Get access to the kr toolkit
import krrt

# Load a theory from the dimacs cnf file
theory = krrt.sat.Dimacs.parseFile('input.cnf')

# Print all of the clauses
for clause in theory.clauses:
    print clause

# Delete the first clause

# Write the theory back to file