Model Counting

Perform Weighted Model Counting on CNF file

#!/usr/bin/env python3
from pathlib import Path
import math
from pysdd.sdd import SddManager, Vtree, WmcManager


here = Path(__file__).parent


def main():
    # Start from a given CNF and VTREE file
    vtree = Vtree.from_file(bytes(here / "input" / "simple.vtree"))
    sdd = SddManager.from_vtree(vtree)
    print(f"Created an SDD with {sdd.var_count()} variables")
    root = sdd.read_cnf_file(bytes(here / "input" / "simple.cnf"))
    # For DNF functions use `read_dnf_file`
    # If the vtree is not given, you can also use 'from_cnf_file`

    # Model Counting
    wmc = root.wmc(log_mode=True)
    w = wmc.propagate()
    print(f"Model count: {int(math.exp(w))}")

    # Weighted Model Counting
    lits = [None] + [sdd.literal(i) for i in range(1, sdd.var_count() + 1)]
    # Positive literal weight
    wmc.set_literal_weight(lits[1], math.log(0.5))
    # Negative literal weight
    wmc.set_literal_weight(-lits[1], math.log(0.5))
    w = wmc.propagate()
    print(f"Weighted model count: {math.exp(w)}")

    # Visualize SDD and VTREE
    print("saving sdd and vtree ... ", end="")
    with open(here / "output" / "sdd.dot", "w") as out:
        print(sdd.dot(), file=out)
    with open(here / "output" / "vtree.dot", "w") as out:
        print(vtree.dot(), file=out)
    print("done")


if __name__ == "__main__":
    main()

Perform Weighted Model Counting on CNF file from CLI

Given a DIMACS file test.cnf

p cnf 2 2
c weights 0.4 0.6 0.3 0.7
-1 2 0
1 -2 0

We can run the CLI:

$ pysdd -c test.cnf
reading cnf...
Read CNF: vars=2 clauses=2
creating initial vtree balanced
creating manager...
compiling...

compilation time         : 0.000 sec
 sdd size                : 2
 sdd node count          : 1
 sdd model count         : 2    0.000 sec
 sdd weighted model count: 0.54    0.000 sec
done