DPMC (Dynamic Programming for Model Counting)

DPMC computes weighted model counts of formulas in conjunctive normal form (CNF)

• The DPMC framework runs in two phases:
  • Planning phase: LG or HTB constructs a join tree of a CNF formula
  • Execution phase: DMC computes the model count of the formula using the join tree
• Developers:
  • Jeffrey Dudek
  • Vu Phan

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

Example files

Acknowledgment