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

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

test commit