DPER (dynamic-programming existential-random stochastic SAT solver)

DPER runs in two phases:

• The planning phase constructs a graded project-join tree for a CNF formula.
• The execution phase computes the maximum and a maximizer from the constructed tree.

---

Cloning this repository

git clone https://github.com/vuphan314/DPER

---

Files

• Dir lg: DPER's planner
• Dir dmc: DPER's executor
• Dir eval: empirical evaluation

---

Acknowledgment

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