Satire

The sequel to GRASP, from the University of Michigan.

May 23, 2003

Check out PBS (the sequel to Satire)
Features include:

• Solves both Decision (yes/no) and optimization problems
• Includes incremental reasoning
• Reads CNF and Pseudo-Boolean (PB) constraints
• Includes recent advances in SAT algorithms (e.g. 2-watched literals approach, 1-UIP conflict diagnosis, etc.)

This is the home page of the Satire satisfiability (SAT) tool.

Satire release 1.0.0 is now available!

Papers describing Satire will be added to this site soon.

Satire features:

·  incremental reasoning

·  generalized constraints

Download the tarred, gzipped Satire distribution: Satire.tgz (272KB)

Precompiled Win32 beta releases are available. These will soon be replaced by Release 1.0.0 binaries.

Grasp2: a stand-alone solver that accepts DIMAC and BLIF formatted input

• Grasp2.exe (32KB) (requires Incsat.dll and IncsatParser.dll)
• Incsat.dll (140KB)
• IncsatParser.dll (60KB)

IncsatInterface.pm: a perl module interface built for ActiveState perl

• IncsatInterface.pm (small) (requires Incsat.dll and IncsatInterface.dll)
• IncsatInterface.dll (69KB)
• IncsatInterface.html (small, auto-documentation)
• cnfsat.pl (a sample perl script using IncstInterface)
• allsat.pl (a perl script for finding ALL answers to a CNF problem)
• Incsat.pm (a small perl module required by allsat.pl)

Linux builds: the grasp2 executable and IncsatInterface perl module are available pre-built for Linux. Like the Win32 executables, these are pre-release versions that will soon be updated with Release 1.0.0 versions. (The Perl scripts, IncsatInterface.pm, cnfsat.pl, etc., are platform-independent, but the CR/LFs must be converted (by dos2unix, for example).)

• grasp2 (300KB)
• IncsatInterface.html
• IncsatInterface.pm
• IncsatInterface.so (300KB)

last updated: 23 May 2003, Fadi Aloul