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

• UpdatedJun 27, 2025
• Rust

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

• UpdatedJan 1, 2021
• Jupyter Notebook

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

Program Design affiliated to General Course Design of CSE College, HUST, for students enrolled in 2018.

• UpdatedApr 9, 2021
• C

SAT solvers from Knuth's The Art of Computer Programming, Vol. 4B

• UpdatedSep 16, 2025
• C++

[wip] Modular SMT solver in rust

• UpdatedNov 13, 2020
• SMT

A small SAT solver implementation. 2020年度の情報科学特別演習にて書いたプログラム

• UpdatedNov 3, 2021
• D

CDCL SAT Solver from Scratch in Python

• UpdatedJun 24, 2025
• Python

Command line tool for SAT solving, SMT solving in various theories (NRA, LRA, LIA, EQ, EQUF, BV)

• UpdatedFeb 9, 2025
• Java

SAT and SMT solving.

• UpdatedMay 28, 2019

🚥 `cron` & dashboard in cloud land

• UpdatedOct 23, 2025
• HTML

SAT Solver

• UpdatedJun 26, 2021
• Rust

SAT Competition 2013 Source Archives

• UpdatedApr 14, 2019

A BDD library written in Rust to support a CDCL Sat Solver like Glucose, while running in parallel.

• UpdatedMay 29, 2023
• C++

OCaml bindings for batsmt

• UpdatedMar 21, 2019
• Rust

A comprehensive Go implementation of the PubGrub version solving algorithm with CDCL, semantic versioning, and enhanced error reporting

• UpdatedNov 1, 2025
• Go

An ocaml implementation of the CDCL algorithm.

• UpdatedMar 23, 2020
• OCaml

CDCL SAT Solver implementation for babies

• UpdatedMay 31, 2020
• Jupyter Notebook

Lightweight but fast SAT solver with input sorting and CDCL

• UpdatedMar 28, 2018
• C++

Simple CDCL SAT solver

• UpdatedMay 14, 2020
• C