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