Home

Libraries

Core

sat	Various functionality for research in Satisfiability.
stats	Various statistical functions that are commonly used.
utils	Utilities for making experimental setup simplified.
planning	Libraries for automated planning tasks.

Coming Soon

encoding	Provides encodings between different problem types.
search	Libraries for backtracking and local search techniques.
viz	Generic libraries for visualization.

---

Dependencies

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

	matplotlib	rpy2	pygtk	pygraph	XDot	Sympy
sat	no	no	no	no	no	yes
stats	yes	yes	no	no	no	no
utils	no	no	no	no	no	no
viz	yes	no	yes	no	yes	no
planning	no	no	no	yes	no	no
search	no	no	no	no	no	no

---

Installation

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

hg clone ssh://[email protected]/haz/krtoolkit
cd krtoolkit
sudo python setup.py 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 http://docs.python.org/library/distutils.html:

• 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 setup.py install --home=~/python

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

---

Usage

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
theory.clauses.pop(0)

# Write the theory back to file
theory.writeCNF('input2.cnf')

---