Quantitative Reasoning on Hybrid Formulas with Dynamic Programming

• This repository supplements Vu Phan's PhD thesis in Computer Science at Rice University.
• 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), also called 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

• Vu Phan: HTB and DMC
• Jeffrey Dudek: LG and Tensor

---

Cloning this repository

git clone https://github.com/vuphan314/phd-thesis

---

Evaluation

---

Examples

---

Acknowledgment

• ADDMC: Dudek, Phan, Vardi
• BIRD: Soos, Meel
• Cachet: Sang, Beame, Kautz
• CryptoMiniSat: Soos
• CUDD package: Somenzi
• CUDD visualization: Kebo
• cxxopts: Beck
• DPMC/ProCount/DPO/DPER: Dudek, Phan, Vardi
• 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