satisfiability

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

The Yices SMT Solver

SAT and Answer Set solver based on Differentiable Satisfiability :::::: Use cases, e.g., Probabilistic SAT solving, Weighted SAT solving, Probabilistic Answer Set Programming, Distribution-aware model sampling, Multi-models optimization ::::::

Approximate Model Counter

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

Tools for working with circuits as graphs in python

A modern CDCL SAT solver in Rust

The Standard Interface for Incremental Satisfiability Solving

Boolean Constraint Solving in Prolog

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

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

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

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.

A Free World Class High Performance SAT Solver

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

Framework for studying cryptographic hash functions using SAT.

A simple SAT solver based on the CDCL algorithm

The first scalable probabilistic exact counter

The first efficient procedure to test whether a sampler is uniform

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

A Header-Only CDCL SAT Solver based on MiniSat (Fast and only 500 lines)

A fast, clean IPASIR SAT solver

PicoSAT bindings for R

High-level interfaces over @msoos's CryptoMiniSat.

Encoding different problems into Boolean satisfiability

An efficient minimal perfect hash function generator for small sets

A lightweight CNF SAT constraint encoder library

A python package that recognizes clauses, Cnfs, graphs, hypergraphs, and multi-hypergraphs. The package implements local graph-rewriting, graph-satchecking, calculation of graph disjunctions, as well as checking of new reduction rules.

Functionally Reduced And-Inverter Graph