Put a STAR in your system! |
| 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. |
| 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. |
| 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. |
| 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. |