Python package for Sentential Decision Diagrams (SDD)

High-performance model counter

A toolbox for knowledge compilation

CNF minimizer and minimal independent set minimizer

VACSEM: Verifying Average Errors in Approximate Circuits Using Simulation-Enhanced Model Counting

Neural Property Approximate Quantifier

Minimal Independent Set Finder for CNFs

SATX is a declarative framework for modeling, analysis, and synthesis using exact SAT and model counting (#SAT) under a unified semantic discipline. SATX treats satisfiability and model counting as coordinated operators, enabling existence checking, constructive synthesis, and structural analysis of solution spaces and theories.

Bottom-up sentential decision diagram compiler.

Empirical evaluation for the EMSE journal extension "Evaluating State-of-the-Art #SAT Solvers on Industrial Configuration Spaces"

EstiMate 🦉: A fast and accurate model counter tool for estimating the number of models for LTL formulas using transfer matrices.

CNF to d-DNNF compiler

An isomorphism-aware #SAT solver

Scalable Precise Computation of Shannon Entropy

Generator for CNF'S considering the variance by using model counting with #sat

Model Counting Competition Submission of Ganak + Approxmc 2025

answer set counter

#SAT solver implemented as part of my bachelor thesis at TU Wien.

Model-counting algorithm written in Coq