Bosphorus, ANF simplifier and solver, and ANF-to-CNF converter

TouIST, the IDE & Language for Logic (backed by SAT, SMT and QBF solvers)

Graph grounding for graph coloring algorithms such as Welsh Powell and Evolution algorithms like Harmony Search and Genetic

Implementation of branch and bound algorithm for maximum clique 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.

Genetic Algorithm for the Maximum Clique Problem

Manipulate NNF (Negation Normal Form) logical sentences

A diabolic implementation of mcSAT 😈

LibMVC is a collection of fast iterative minimum vertex cover solvers. Currently NuMVC and FastVC are implemented.

Results of popular Steiner tree instances

a collection of benchmarks (in DIMACS format) for various NP-Complete problems

Utilities to parse files in DIMACS format which is the de-facto standard for input to SAT solvers.

Windows builds for The Glucose SAT Solver.

Compile MiniSat to WebAssembly using emscripten

A simple theorem prover made for a university programming assignment

Coverts a generic Verilog netlist into the DIMACS format compatible with many SAT solvers

An implementation of a recursive DPLL solver in OCaml. It parses setup (cnf ) DIMACS and checks if the formula is satisfied.

Compile microsat to WebAssembly using emscripten

Simple CDCL SAT solver

A set of parsers for DIMACS formats written in Prolog