SAT Calculator – SAT Solver and CNF Editor

SAT Calculator is an open source SAT formula editor and deterministic SAT solver designed for studying Boolean satisfiability problems in the context of complexity theory and propositional logic. The application allows users to create, edit and analyze SAT formulas in conjunctive normal form (CNF) through an interactive graphical interface.

The editor supports the creation and modification of variables, literals and clauses, while providing a clear visual representation of the formula structure. Users can manually assign values to variables in order to observe how different valuations affect the overall formula and determine whether it evaluates to true or false.

The integrated deterministic SAT solver computes all possible valuations of the variables and identifies those that satisfy the formula. This allows users to study solution spaces and better understand the behavior of SAT problems.

In addition to solving formulas, the application provides tools for logical analysis such as applying resolution operations to selected clauses. This makes it possible to experiment with resolution rules and observe how new clauses are derived during the reasoning process.

SAT Calculator also provides statistical information about variables and clauses, helping users analyze the structure and complexity of the formula. Formulas can be written manually, pasted from external sources or loaded from ready-made examples available online.

The application runs on Windows and is implemented using WPF, C# and .NET Framework 4.7.2.

You can download it from SAT Calculator for Windows or download the SAT Calculator source code on GitHub github.com/kritikov/SATCalculator.