Поиск входных переменных в булевой формуле

Source code of paper 'SAT Solving Using XOR-OR-AND Normal Forms'

Windows builds for The Glucose SAT Solver.

Lab sessions about SAT solving using the IDP IDE

Python tool for converting ANF to (2-)XNF.

Immediate Massively Parallel Propositional Proof Checking

A search program that uses SAT solvers to find patterns in Higher Range Outer Totalistic (HROT) rules

STTF

Looking for solutions of certain sizes with Glucose, Kissat and CaDiCaL

Solving the Yashi game using a combination of graph theory and SAT-solving. First, connectivity of the graph is verified, and if true, identification of all possible cycles is done. Then, after generating all necessary constraints, they are passed to a SAT solver.

Low-level Java bindings to the IPASIR C interface

Projects on symbolic systems, covering logic and problem solving (June 2020).

My first SMT solver (only QF_UF)

SAT-Web is a web-based educational tool for explaining SAT solving. It provides visualisations with search trees and variable interaction graphs, and includes a DPLL solver with tracing.

Boolean DSL

A collection of combinatorial solvers for the Sudoku variant Str8ts.

Kissat-VSA is a solver submitted to the SAT Competition 2025, achieving third place in the Main Track and second place in the Main Track UNSAT category.

Approximation and randomized algorithms - Assignment 01 - SAT