@phdthesis{Phan2022quantitative,
  title={{Quantitative Reasoning on Hybrid Formulas with Dynamic Programming}},
  abstract={
    We perform quantitative reasoning via Stochastic Satisfiability (SSAT), a problem that involves the existential quantifier, the random quantifier, and Boolean formulas. SSAT generalizes the Weighted Satisfiability (WSAT), Weighted Model Counting (WMC), Weighted Projected Model Counting (WPMC), and Existential-Random Satisfiability (ERSAT) problems. SSAT has been used to model power-transmission reliability, machine-learning fairness, and other applications. Prior work on SSAT mainly focuses on Conjunctive Normal Form (CNF). A CNF formula is a conjunctively interpreted set of disjunctive clauses. We study a more general format, XOR-extended Conjunctive Normal Form (XOR-CNF). An XOR-CNF formula is a set of hybrid constraints that include XOR clauses and disjunctive clauses. Native support for XOR is desirable because this constraint type is prevalent in several applications, such as cryptography and circuit design. Although XOR-CNF can be converted into CNF by adding linearly many auxiliary variables and disjunctive clauses, this apparently small overhead actually decimates the performance of CNF solvers in our empirical evaluation. Our solvers natively handle hybrid constraints with algebraic decision diagrams, which provide compact representations of XOR and disjunctive clauses. To solve a big set of constraints, we employ dynamic programming. This approach partitions the constraint set and solves resultant subsets before merging partial solutions into a final answer. Given an XOR-CNF formula, we obtain a requested solution using a Project-Join Tree (PJT) that specifies how to conjoin clauses and project out variables of the formula. Existentially quantified variables are maximally projected, and randomly quantified variables are summatively projected. Our framework operates in two phases. First, the planning phase constructs a PJT from an XOR-CNF formula. Second, the execution phase traverses the constructed PJT to compute a solution. This framework is versatile because different planners and executors can be combined. Also, we may use a single plan with multiple executions: a one-layer PJT with WSAT and WMC, or a two-layer PJT with WPMC and ERSAT. We empirically demonstrate that our exact solvers meaningfully contribute to the state of the art. On 1606 one-layer instances from inference and planning applications, adding our framework leads to significant reductions in mean PAR-2 scores of solver portfolios: 6.0\% for WSAT and 27.7\% for WMC. On 613 two-layer instances from sampling and counting applications, the score reductions are 5.8\% for WPMC and 10.7\% for ERSAT. Future work includes merging our SSAT framework with another PJT-based framework that solves minimum-maximum satisfiability. We will also consider adding more layers of quantification to support a more general problem, maximum model counting.
  },
  url={https://repository.rice.edu/items/2e464125-244d-431b-b998-612f0dc2b41a},
  author={Phan, Vu H. N.},
  date={2022},
  type={{PhD thesis}},
  institution={Rice University},
}