pyganak — Python bindings for Ganak

pyganak provides Python bindings for Ganak, a high-performance exact model counter for CNF formulas. It exposes two classes:

  • Counter — unweighted (and projected) model counting. Returns an arbitrary-precision Python int.
  • WeightedCounter — weighted model counting with per-literal float weights. Uses MPFR internally; returns a Python float.

Arjun preprocessing is applied automatically before each count, just as the command-line tool does.

Installation

pip install pyganak

Pre-built wheels are available for Linux (x86-64, ARM64) and macOS (Apple Silicon, Intel).

Quick start

Unweighted counting

from pyganak import Counter

c = Counter()
c.add_clause([1, 2])      # x1 OR x2
c.add_clause([-1, 2])     # NOT x1 OR x2
print(c.count())          # → 2  (exact Python int)

Weighted counting

from pyganak import WeightedCounter

c = WeightedCounter()
c.add_clause([1, 2])           # x1 OR x2

# Set weights for both polarities of each variable.
c.set_lit_weight( 1, 0.3)     # P(x1 = True)  = 0.3
c.set_lit_weight(-1, 0.7)     # P(x1 = False) = 0.7
c.set_lit_weight( 2, 0.4)     # P(x2 = True)  = 0.4
c.set_lit_weight(-2, 0.6)     # P(x2 = False) = 0.6

# Models: (T,T)=0.12  (T,F)=0.18  (F,T)=0.28  → total=0.58
print(c.count())               # → 0.58  (Python float)

Counter API

Counter(verbose=0, seed=0)

Parameter Type Default Description
verbose int 0 Verbosity level (0 = silent)
seed int 0 Random seed for the solver

add_clause(clause)

Add a single clause — iterable of nonzero signed integers (1-indexed variables; positive = positive literal, negative = negated literal).

c.add_clause([1, -2, 3])   # x1 OR NOT x2 OR x3

add_clauses(clauses)

Add multiple clauses at once.

c.add_clauses([[1, 2], [-1, 3]])

set_sampling_set(vars)

Set the projection set (independent support). Only the given variables are counted; all others are existentially quantified out. If never called, all variables are included.

c.add_clause([1, 2, 3])
c.set_sampling_set([1, 2])
print(c.count())   # → 4

count() → int

Run Arjun preprocessing + Ganak and return the exact model count as a Python int. May only be called once per instance.

new_vars(n) / nof_vars() → int / nof_clauses() → int

Declare extra variables, or query the current variable / clause count.

WeightedCounter API

WeightedCounter(verbose=0, seed=0, prec=128)

Parameter Type Default Description
verbose int 0 Verbosity level
seed int 0 Random seed
prec int 128 MPFR precision in bits (≥ 2)

The internal arithmetic is performed with MPFR at prec bits of precision (default 128 ≈ 38 significant decimal digits). The final result is returned as a Python float (double).

Floating-point caveat: Because floating-point arithmetic is not associative, the result is a high-precision approximation rather than an exact value — the order in which partial sums are accumulated can affect the last few bits. For exact rational weighted counting, use the command-line tool with --mode 1 (GMP mpq rationals).

set_lit_weight(lit, weight)

Set the weight of a literal.

  • lit — nonzero signed integer (1-indexed; positive = positive literal).
  • weight — Python float (double). Stored internally as an MPFR value at the precision given to the constructor.

Always set weights for both a literal and its negation to get well-defined weighted counting. Literals whose weights are not set default to weight 1.0.

c.set_lit_weight( 1, 0.3)   # weight of  x1 = 0.3
c.set_lit_weight(-1, 0.7)   # weight of ¬x1 = 0.7

add_clause(clause) / add_clauses(clauses) / set_sampling_set(vars) / new_vars(n) / nof_vars() / nof_clauses()

Identical to the Counter versions.

count() → float

Run Arjun preprocessing + Ganak weighted model counting. Returns the weighted count as a Python float. The internal computation uses MPFR at the configured precision. May only be called once per instance.

Examples

Plain model counting

from pyganak import Counter

# (x1 XOR x2): 2 models
c = Counter()
c.add_clause([1, 2])
c.add_clause([-1, -2])
print(c.count())   # 2

Projected model counting

from pyganak import Counter

# (x1 OR x2 OR x3) projected onto {x1, x2}: 4 models
c = Counter()
c.add_clause([1, 2, 3])
c.set_sampling_set([1, 2])
print(c.count())   # 4

Large count (arbitrary precision)

from pyganak import Counter

# 30 unconstrained variables → 2^30 models
c = Counter()
c.new_vars(30)
print(c.count())   # 1073741824

Weighted counting

from pyganak import WeightedCounter

# (x1 OR x2) with independent Bernoulli weights
c = WeightedCounter()
c.add_clause([1, 2])
c.set_lit_weight( 1, 0.3);  c.set_lit_weight(-1, 0.7)
c.set_lit_weight( 2, 0.4);  c.set_lit_weight(-2, 0.6)
print(c.count())   # 0.58

Weighted counting with higher MPFR precision

from pyganak import WeightedCounter

# Use 256-bit MPFR precision for the internal computation.
c = WeightedCounter(prec=256)
c.add_clause([1, 2, 3])
c.set_lit_weight( 1, 0.1);  c.set_lit_weight(-1, 0.9)
c.set_lit_weight( 2, 0.2);  c.set_lit_weight(-2, 0.8)
c.set_lit_weight( 3, 0.5);  c.set_lit_weight(-3, 0.5)
print(c.count())

Building from source (venv)

If you have already built Ganak with CMake (see the top-level README.md for instructions), the extension is in build/lib/pyganak*.so. Test it without a full pip install using a venv:

python3 -m venv venv
venv/bin/pip install pytest
PYTHONPATH=build/lib venv/bin/pytest python/tests/ -v

To rebuild the extension after editing python/src/pyganak.cpp:

# If the build directory already exists:
cmake -DBUILD_PYTHON_EXTENSION=ON build   # or cmake .. from inside build/
cmake --build build --target pyganak -j$(nproc)

# Then re-run tests as above.

To do a full pip install (builds everything from scratch):

pip install .

Requires: GMP ≥ 5, MPFR ≥ 3, FLINT ≥ 2. On Ubuntu/Debian:

sudo apt install libgmp-dev libmpfr-dev libflint-dev

On macOS:

brew install gmp mpfr flint

License

MIT — see LICENSE.txt in the repository root.

Key dates

PyPI data
Data sourced directly from PyPI's database.
  • Released:
Latest release

1 maintainer

PyPI data
Data sourced directly from PyPI's database.
Avatar for msoos from gravatar.com msoos

Credits

Author/Maintainer: Mate Soos

License

MIT License (There is a BSD 2-style license for Flow Cutter and an MIT license for the rest)

Requires

Python >=3.9

Tags

sat model counting exact counting projected counting

Classifiers

Report project as malware

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distributions

No source distribution files available for this release.See tutorial on generating distribution archives.

Built Distributions

If you're not sure about the file name format, learn more about wheel file names.

pyganak-2.6.4-cp313-cp313-manylinux_2_34_x86_64.whl (6.3 MB view details)

Uploaded CPython 3.13manylinux: glibc 2.34+ x86-64

pyganak-2.6.4-cp313-cp313-manylinux_2_34_aarch64.whl (5.8 MB view details)

Uploaded CPython 3.13manylinux: glibc 2.34+ ARM64

pyganak-2.6.4-cp313-cp313-macosx_11_0_arm64.whl (5.2 MB view details)

Uploaded CPython 3.13macOS 11.0+ ARM64

pyganak-2.6.4-cp312-cp312-manylinux_2_34_x86_64.whl (6.3 MB view details)

Uploaded CPython 3.12manylinux: glibc 2.34+ x86-64

pyganak-2.6.4-cp312-cp312-manylinux_2_34_aarch64.whl (5.8 MB view details)

Uploaded CPython 3.12manylinux: glibc 2.34+ ARM64

pyganak-2.6.4-cp312-cp312-macosx_11_0_arm64.whl (5.2 MB view details)

Uploaded CPython 3.12macOS 11.0+ ARM64

pyganak-2.6.4-cp311-cp311-manylinux_2_34_x86_64.whl (6.3 MB view details)

Uploaded CPython 3.11manylinux: glibc 2.34+ x86-64

pyganak-2.6.4-cp311-cp311-manylinux_2_34_aarch64.whl (5.8 MB view details)

Uploaded CPython 3.11manylinux: glibc 2.34+ ARM64

pyganak-2.6.4-cp311-cp311-macosx_11_0_arm64.whl (5.2 MB view details)

Uploaded CPython 3.11macOS 11.0+ ARM64

pyganak-2.6.4-cp310-cp310-manylinux_2_34_x86_64.whl (6.3 MB view details)

Uploaded CPython 3.10manylinux: glibc 2.34+ x86-64

pyganak-2.6.4-cp310-cp310-manylinux_2_34_aarch64.whl (5.8 MB view details)

Uploaded CPython 3.10manylinux: glibc 2.34+ ARM64

pyganak-2.6.4-cp310-cp310-macosx_11_0_arm64.whl (5.2 MB view details)

Uploaded CPython 3.10macOS 11.0+ ARM64

pyganak-2.6.4-cp39-cp39-manylinux_2_34_x86_64.whl (6.3 MB view details)

Uploaded CPython 3.9manylinux: glibc 2.34+ x86-64

pyganak-2.6.4-cp39-cp39-manylinux_2_34_aarch64.whl (5.8 MB view details)

Uploaded CPython 3.9manylinux: glibc 2.34+ ARM64

pyganak-2.6.4-cp39-cp39-macosx_11_0_arm64.whl (5.2 MB view details)

Uploaded CPython 3.9macOS 11.0+ ARM64

File details

Details for the file pyganak-2.6.4-cp313-cp313-manylinux_2_34_x86_64.whl.

File metadata

File hashes

Hashes for pyganak-2.6.4-cp313-cp313-manylinux_2_34_x86_64.whl
Algorithm Hash digest
SHA256 c3b2517262e62a4101f79005e5a6e0a2527fe835676b2681bd51c2022856961d
MD5 e687e4854cabaac28732b82bdc5e556c
BLAKE2b-256 9d61891803ce7e49f0c33e56df433b87d5268b37011f45dd9980a16915f02cef

See more details on using hashes here.

Provenance

The following attestation bundles were made for pyganak-2.6.4-cp313-cp313-manylinux_2_34_x86_64.whl:

Publisher: python-wheels.yml on meelgroup/ganak

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file pyganak-2.6.4-cp313-cp313-manylinux_2_34_aarch64.whl.

File metadata

File hashes

Hashes for pyganak-2.6.4-cp313-cp313-manylinux_2_34_aarch64.whl
Algorithm Hash digest
SHA256 fd3f90736d0aaea1023a88189cfd7d94ed06ae908fa5c68257d7c099ed710d83
MD5 465b5ff419190f6e21fcb18e2f33261f
BLAKE2b-256 3c9851beb6c6393ffa5d250a4409b1dfabfb54babb8d6fb2f5ac1fe0700638a7

See more details on using hashes here.

Provenance

The following attestation bundles were made for pyganak-2.6.4-cp313-cp313-manylinux_2_34_aarch64.whl:

Publisher: python-wheels.yml on meelgroup/ganak

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file pyganak-2.6.4-cp313-cp313-macosx_11_0_arm64.whl.

File metadata

File hashes

Hashes for pyganak-2.6.4-cp313-cp313-macosx_11_0_arm64.whl
Algorithm Hash digest
SHA256 08b08424ac7dc248b405503abad233e5e38d996c927990c88206be3d48033309
MD5 c2808876d65977c3d4571678ea1ab10e
BLAKE2b-256 c3aaca5e6a6a109cf3e51f0a90ff9a0fa4d59d007e9b0ef1b7580d9e4f74b3da

See more details on using hashes here.

Provenance

The following attestation bundles were made for pyganak-2.6.4-cp313-cp313-macosx_11_0_arm64.whl:

Publisher: python-wheels.yml on meelgroup/ganak

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file pyganak-2.6.4-cp312-cp312-manylinux_2_34_x86_64.whl.

File metadata

File hashes

Hashes for pyganak-2.6.4-cp312-cp312-manylinux_2_34_x86_64.whl
Algorithm Hash digest
SHA256 1375cee16f8fcaf3f7f2f91b86eaa8041762a36b806b5d7102a5a18d40b28b9e
MD5 05d24c1be2c23589b2b604b9437f478a
BLAKE2b-256 4df1b0cb0dae510cea31324526c2a7679e14b8c99795d970013aa7dc50ad1dd8

See more details on using hashes here.

Provenance

The following attestation bundles were made for pyganak-2.6.4-cp312-cp312-manylinux_2_34_x86_64.whl:

Publisher: python-wheels.yml on meelgroup/ganak

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file pyganak-2.6.4-cp312-cp312-manylinux_2_34_aarch64.whl.

File metadata

File hashes

Hashes for pyganak-2.6.4-cp312-cp312-manylinux_2_34_aarch64.whl
Algorithm Hash digest
SHA256 035503460d9bb6f41a9a54fa59113e37ccbd5b73ff495046048ff9d6823c1980
MD5 3adfd345db408af46773f9d099eb09a4
BLAKE2b-256 b36e98d2fcf3377ba74af4d7dee1a8ba1863c15b50b0a77f16a8f602d86289bb

See more details on using hashes here.

Provenance

The following attestation bundles were made for pyganak-2.6.4-cp312-cp312-manylinux_2_34_aarch64.whl:

Publisher: python-wheels.yml on meelgroup/ganak

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file pyganak-2.6.4-cp312-cp312-macosx_11_0_arm64.whl.

File metadata

File hashes

Hashes for pyganak-2.6.4-cp312-cp312-macosx_11_0_arm64.whl
Algorithm Hash digest
SHA256 c51333229d5647ae9031f9665a6c21e62289d552aee26d9acc3bd044bd1e0a66
MD5 ca68d3eafee6283552a5415c52dbd872
BLAKE2b-256 dd5ffd80476b88f81f648a201e85fa7811e61a36c28d488f4b987297ccf43bbc

See more details on using hashes here.

Provenance

The following attestation bundles were made for pyganak-2.6.4-cp312-cp312-macosx_11_0_arm64.whl:

Publisher: python-wheels.yml on meelgroup/ganak

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file pyganak-2.6.4-cp311-cp311-manylinux_2_34_x86_64.whl.

File metadata

File hashes

Hashes for pyganak-2.6.4-cp311-cp311-manylinux_2_34_x86_64.whl
Algorithm Hash digest
SHA256 7279261f6af9613129e0fb92f2c1469ecab47cae8be448f5c779aac97c7c2494
MD5 a08cc04fb04bc54eaaba168ac14215de
BLAKE2b-256 14e38ba27e20b46fa778920bb76b48b53553b51a2bb7d914e93bb739047de437

See more details on using hashes here.

Provenance

The following attestation bundles were made for pyganak-2.6.4-cp311-cp311-manylinux_2_34_x86_64.whl:

Publisher: python-wheels.yml on meelgroup/ganak

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file pyganak-2.6.4-cp311-cp311-manylinux_2_34_aarch64.whl.

File metadata

File hashes

Hashes for pyganak-2.6.4-cp311-cp311-manylinux_2_34_aarch64.whl
Algorithm Hash digest
SHA256 1008a14cd68a58edd2fe572430d496d4758e3d4b4de9ae0fe8ec5faba1bb37cd
MD5 0597694d57caf8e6458639e51befd6b6
BLAKE2b-256 9852c5179911f178f12c1a84b68e96857fc40424c97950fd0328b51e52c0fdd3

See more details on using hashes here.

Provenance

The following attestation bundles were made for pyganak-2.6.4-cp311-cp311-manylinux_2_34_aarch64.whl:

Publisher: python-wheels.yml on meelgroup/ganak

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file pyganak-2.6.4-cp311-cp311-macosx_11_0_arm64.whl.

File metadata

File hashes

Hashes for pyganak-2.6.4-cp311-cp311-macosx_11_0_arm64.whl
Algorithm Hash digest
SHA256 0160999bc370a8a9d91f0375304e86a730f6fb40279b0f1f3e8c24b1ee0ee74f
MD5 f059e34e60949c249e2c36330965e1ec
BLAKE2b-256 7e564dbdbba04a94298f13bfc38779ce93c588cbc3322e8d27088c7960e0cc61

See more details on using hashes here.

Provenance

The following attestation bundles were made for pyganak-2.6.4-cp311-cp311-macosx_11_0_arm64.whl:

Publisher: python-wheels.yml on meelgroup/ganak

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file pyganak-2.6.4-cp310-cp310-manylinux_2_34_x86_64.whl.

File metadata

File hashes

Hashes for pyganak-2.6.4-cp310-cp310-manylinux_2_34_x86_64.whl
Algorithm Hash digest
SHA256 5bbad4bd149acd9d462fedc91178f225d93f194a20798361b5f92872ef951df8
MD5 176eaf4bae8158cc1cee755fa239a032
BLAKE2b-256 1ece1ff5e348b510d51360939b4690048b5b5d2760ea29650874018efee4d159

See more details on using hashes here.

Provenance

The following attestation bundles were made for pyganak-2.6.4-cp310-cp310-manylinux_2_34_x86_64.whl:

Publisher: python-wheels.yml on meelgroup/ganak

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file pyganak-2.6.4-cp310-cp310-manylinux_2_34_aarch64.whl.

File metadata

File hashes

Hashes for pyganak-2.6.4-cp310-cp310-manylinux_2_34_aarch64.whl
Algorithm Hash digest
SHA256 aab23ebcbde2d58f7c038b1b090e69663dadc08fb345acdc1b849111128fefd6
MD5 855d13d83a9c2987762ff2e6cd35f428
BLAKE2b-256 e693a0fc6ecdf19653a650ab4ac7729d697e98b7d6ed423f5028dfed36c6eea0

See more details on using hashes here.

Provenance

The following attestation bundles were made for pyganak-2.6.4-cp310-cp310-manylinux_2_34_aarch64.whl:

Publisher: python-wheels.yml on meelgroup/ganak

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file pyganak-2.6.4-cp310-cp310-macosx_11_0_arm64.whl.

File metadata

File hashes

Hashes for pyganak-2.6.4-cp310-cp310-macosx_11_0_arm64.whl
Algorithm Hash digest
SHA256 06ad7e234cb27cbf963b0dadd3ce3628886e3e0af847e725ced3e65cbe431c68
MD5 91426c61a7044bb4c7e2876fe2f37306
BLAKE2b-256 7aa355d1a85f975e0adda0c9a3b6863eb750ce60e4671dbefc729df6400fbc88

See more details on using hashes here.

Provenance

The following attestation bundles were made for pyganak-2.6.4-cp310-cp310-macosx_11_0_arm64.whl:

Publisher: python-wheels.yml on meelgroup/ganak

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file pyganak-2.6.4-cp39-cp39-manylinux_2_34_x86_64.whl.

File metadata

File hashes

Hashes for pyganak-2.6.4-cp39-cp39-manylinux_2_34_x86_64.whl
Algorithm Hash digest
SHA256 6ccf684ad5d40338a040222e71c5c0d7257dd383c9d04c13fd38c4917d8b6de3
MD5 9f37963a0c3ce28d6f6aaaf16f1f2e9a
BLAKE2b-256 f4003ed1b3de04b0c5698237531ad1abe351cf500fdde04ffec4f7673e2a8daa

See more details on using hashes here.

Provenance

The following attestation bundles were made for pyganak-2.6.4-cp39-cp39-manylinux_2_34_x86_64.whl:

Publisher: python-wheels.yml on meelgroup/ganak

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file pyganak-2.6.4-cp39-cp39-manylinux_2_34_aarch64.whl.

File metadata

File hashes

Hashes for pyganak-2.6.4-cp39-cp39-manylinux_2_34_aarch64.whl
Algorithm Hash digest
SHA256 66761406b670c39da1776bb2a38ba1012705335468179e438e34eb5f22627084
MD5 273de26670ba4c83409e3d2f7374b51f
BLAKE2b-256 bd912cfff5540d2967b830e435c676304ff6ca9b1241cae575318536dfe19011

See more details on using hashes here.

Provenance

The following attestation bundles were made for pyganak-2.6.4-cp39-cp39-manylinux_2_34_aarch64.whl:

Publisher: python-wheels.yml on meelgroup/ganak

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file pyganak-2.6.4-cp39-cp39-macosx_11_0_arm64.whl.

File metadata

File hashes

Hashes for pyganak-2.6.4-cp39-cp39-macosx_11_0_arm64.whl
Algorithm Hash digest
SHA256 799525bb51dbe9c91e4e33a941ddf0b5dfdaf57b7a5524f3a5db711612abee8c
MD5 42fdb73b0f79fd79cf4d95836f12a783
BLAKE2b-256 83189615b8239e654060e8df0b5c824f9ac156aecd19f64b17962ce5a234f996

See more details on using hashes here.

Provenance

The following attestation bundles were made for pyganak-2.6.4-cp39-cp39-macosx_11_0_arm64.whl:

Publisher: python-wheels.yml on meelgroup/ganak

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

Release history Release notifications | RSS feed

This release

2.6.4 This release

15 files

2.6.3

15 files

2.6.2

15 files

2.6.1

15 files

Anthropic, PBC Visionary sponsor Bloomberg Visionary sponsor Hudson River Trading Visionary sponsor Meta Visionary sponsor NVIDIA Visionary sponsor Microsoft Sustainability sponsor Depot Continuous Integration AWS Cloud computing and Security Sponsor Datadog Monitoring Fastly CDN Google Download Analytics Sentry Error logging StatusPage Status page