CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.

• UpdatedJun 13, 2025
• Rust

SRI Yices SMT Solver

• UpdatedFeb 19, 2026
• SMT

a Pythonic toolkit for working with Boolean expressions

• UpdatedMay 8, 2025
• Python

The glucose SAT solver

• UpdatedDec 30, 2025
• C++

Tools for working with circuits as graphs in python

• UpdatedNov 17, 2023
• Verilog

A modern (trail saving, clause subsumption/vivification, learning-rate based selecting, rephrase) CDCL SAT solver in Rust

• UpdatedJun 27, 2025
• Rust

A library for building efficient set-membership filters and dictionaries based on the Satisfiability problem.

• UpdatedAug 4, 2022
• C

Approximate Model Counter

• UpdatedFeb 14, 2026
• C++

Probabilistic Answer Set Programming and Probabilistic SAT solving, based on Differentiable Satisfiability

• UpdatedJul 1, 2024
• Scala

High-performance model counter

• UpdatedFeb 17, 2026
• C++

Kiwi is a minimalist and extendable Constraint Programming (CP) solver.

• UpdatedJun 6, 2019
• Java

The Standard Interface for Incremental Satisfiability Solving

• UpdatedJun 28, 2022
• C++

This library aims to provide implementations of elements commonly used in the development on software in the area of satisfiability solving. The focus of the library is to provide as much ease of use without giving up on performance.

• UpdatedFeb 20, 2026
• Rust

Boolean Constraint Solving in Prolog

• UpdatedDec 8, 2024
• Prolog

A simple SAT solver that implements the DPLL algorithm with unit resolution

• UpdatedSep 10, 2019
• C++

A customizable timetabling software for educational institutions that encodes timetabling constraints as a SAT formula and solves them using a MaxSAT solver

• UpdatedSep 29, 2019
• C++

CGen is a tool for encoding SHA-1 and SHA-256 hash functions into CNF in DIMACS format, also into ANF polynominal system in PolyBoRi output format.

• UpdatedJun 3, 2023
• C++

A SAT Solver based on CDCL (Conflict Driven Clause Learning) implemented in python

• UpdatedJan 1, 2021
• Jupyter Notebook

[SIGKDD 2023] HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline

• UpdatedJun 16, 2023
• Python

SAT solver based on CDCL in Python with Conflict Driven Clause Learning, clever Heuristics - VSIDS, 2 - Literal watch advanced data structure, Random restarts with restart probability decay

• UpdatedSep 16, 2020
• Jupyter Notebook