sampling-and-counting

ApproxMC

A hashing-based algorithm for discrete integration over finite domains.

CrystalBall

A framework to provide white-box access to the execution of SAT solver.

UniGen

An algorithm to generate uniform samples subject to given set of constraints.

Bosphorus

An ANF and CNF simplifier and converter.

MIS

An algorithm to compute minimal independent support for a given CNF formula.

SMTApproxMC

An approximate model counter for Bitvector theory.

WeightGen

A hashing-based approximate sampler for weighted CNF formulas.

WeightMC

A weighted model counter over Boolean domains.