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.