Put a STAR in your system!

*SAT

Anything on SAT. This project is concerned with the development of SAT-based decision procedures for modal (temporal, description) logics. Currently, *SAT (ver 1.3) is a tool written in C that implements several decision procedures for modal K and modal E.

QuBE

Quantified Boolean formulas Evaluator. This project is aimed to build an efficient solver for the quantified proposition satisfiability (QSAT) problem. At the moment, QuBE is a family of tools written in C that implement decision procedures for QSAT.

SIM

Satisfiability Internal Module. This project is concerned with the development of an efficient, open and well documented library to solve propositional satisfiability (SAT) problems. Currently, SIM (ver. 1.0) is a library written in C featuring nine heuristics and several optimization techniques.

SIMO

SIM Object oriented. SIMO is the evolution along the lines of SIM. We are about to release a new version of SIMO (ver. 3.0) which will integrate our previous experience with SIM into an efficient and up-to-date tool for SAT.