DPMC/ProCount/DPO/DPER

• We provide four exact solvers that support XOR-CNF formulas.
  • DPMC solves weighted model counting (WMC).
  • ProCount solves weighted projected model counting (WPMC).
  • DPO solves weighted SAT (WSAT), i.e., Boolean MPE.
  • DPER solves exist-random SAT (ERSAT).
• Each of these four solvers is a combination of a planner and an executor.
  • A planner produces a project-join tree T from an XOR-CNF formula F.
  • An executor traverses T to computes a solution of F.
  • For WPMC and ERSAT, T must be graded.
• Two planners are available.
  • HTB uses constraint-programming heuristics.
  • LG uses tree decomposers.
• Two executors are available.
  • DMC uses algebraic decision diagrams (ADDs).
  • Tensor uses tensors and only solves WMC on pure CNF.
• Developers:
  • Jeffrey Dudek: LG and Tensor
  • Vu Phan: HTB and DMC

---

Releases

• 2021/05/25: mc-2021
  • Model Counting Competition MC-2021
• 2021/05/23: v2.0.0
  • SAT-2021 paper: ProCount: Weighted Projected Model Counting with Graded Project-Join Trees
    • Authors: Jeffrey M. Dudek, Vu H. N. Phan, Moshe Y. Vardi
• 2020/07/20: v1.0.0
  • CP-2020 paper: DPMC: Weighted Model Counting by Dynamic Programming on Project-Join Trees
    • Authors: Jeffrey M. Dudek, Vu H. N. Phan, Moshe Y. Vardi

---

Cloning this repository and its submodules

git clone --recursive https://github.com/vardigroup/DPMC

---

Examples

---

Acknowledgment

• ADDMC: Dudek, Phan, Vardi
• BIRD: Soos, Meel
• Cachet: Sang, Beame, Kautz
• CryptoMiniSat: Soos
• CUDD package: Somenzi
• CUDD visualization: Kebo
• cxxopts: Beck
• FlowCutter: Strasser
• htd: Abseher, Musliu, Woltran
• miniC2D: Oztok, Darwiche
• Model Counting Competition: Hecher, Fichte
• pmc: Lagniez, Marquis
• SlurmQueen: Dudek
• Sylvan: van Dijk
• Tamaki: Tamaki
• TensorOrder: Dudek, Duenas-Osorio, Vardi
• WAPS: Gupta, Sharma, Roy, Meel