Description

This is a Haskell library for dealing with propositional logic. In particular, it currently provides the following features:

• Translation of diophantine constraints to propositional formulas
• Translation of common arithmetical functions over Integers and Naturals to propositional formulas
• A general interface to SAT-solvers, including efficient translation of arbitrary formulas to CNF.

News

• Jan 01 2012: Recent development version 0.9 has been released.
• Aug 10 2011: Recent development version 0.8 has been released.
• Mar 01 2011: Recent development version 0.7 has been released.
• Jul 07 2010: Recent development version 0.6 has been released.
• Oct 27 2009: Early development version 0.5 has been released. This release is still heavily in development, so be aware that interfaces are likely to change.

Requirements

Currently compiling requires the following software packages:

• The Glasgow Haskell Compiler (GHC), version 6.10.3 or above
• Cabal, the common architecture for building applications and libraries. Cabals usually comes (depending on the distribution) bundled with GHC.
• The parfold package.
• The SAT solver minisat, version 2.2.

Download

The latest version is available on github. Alternatively, you can download a single tar file of the current version or check out the archive.

Installation

Thanks to cabal, installation should be as easy as

  > cabal install

Documentation

Currently, only a partial and rudimentary source code documentation is available.

Contact

The main authors are Martin Avanzini, Georg Moser and Andreas Schnabl.