[  download | web | interface | description | license ]

Download

[ limboole1.2.tgz (src) ]
[ limboole1.1.tar.gz (src) ]
[ limboole1.tar.gz (src) ]
[ limboole-0.2.tar.gz (src) ]
[ limboole-linux-amd64.exe (Linux amd64 binary) ]
[ limboole-linux-x86.exe (Linux x86 binary) ]
[ limboole-OSX (Mach-O 64-bit executable x86_64) ]
[ limboole.exe (Windows binary) ]
[ limbooleAPE.exe (Actually Portable Executable; Running on all modern systems) ]

Limboole on the Go!

Description

Limboole is a simple tool for checking satisfiability respectively tautology on arbitrary structural formulas, and not just satisfiability for formulas in conjunctive normal form (CNF), like the DIMACS format, which the standard input format of SAT solvers. The tool can also be used as a translator of such structural problems into CNF.

The structural input format of Limboole is described in the README that is included in the sources. The NEWS files describes new features and changes, and the BUILD file describes how to compile the tool.

Since Version 1 we support and require at least one of Lingeling or PicoSAT as SAT solver back-end. See BUILD file for more information. Support for Limmat has been removed. Version 1.3 prenex QBFs using the QBF solver DepQBF.

License

There is no specific license for the Limboole SAT solver front-end software. It is provided "as is" and can be used in any way without warranty of any kind.

However, linking against Lingeling and PicoSAT will produce a binary, which falls under the license restrictions of those tools, which are more restricted.