This part contains links to some research software.
More recently developed software can be found at https://github.com/arminbiere.
Older JKU software is available at http://fmv.jku.at/software.
This part contain links to some tools that have developed by students for teaching purposes.
This D-Algorithm project was developed by Benny Wennberg as part of his bachelor project. It is a tool to visualize the D-Algorithm by Roth to find suitable tests for stuck at faults in digital circuits.
This grs-bits project (in German) was developed by Robin Trüby as part of his bachelor thesis. It is a tool to visualize how GRS bits work (used in arithmetic circuits to calculate floating-point results with enough precision without increasing the size of the circuits too much).
This https://maximaximal.github.io/limboole/ developed by Maximilian Heisinger is a simple tool for checking satisfiability respectively tautology on arbitrary structural formulas, and not just satisfiability for formulas. It has a more user friendly input format than CNF and is a perfect supplement for an introductory course in logic.