A Resolution Proof System for Dependency Stochastic Boolean Satisfiability
Yun-Rong Luo*, Che Cheng*, Jie-Hong Roland Jiang. In Journal of Automated Reasoning, 2023.
In this work, we present the first sound and complete resolution calculus for Dependency Stochastic Boolean Satisfiability (DSSAT).
Paper and Slides
Abstract
Dependency stochastic Boolean satisfiability (DSSAT), which generalizes stochastic Boolean satisfiability (SSAT) and dependency quantified Boolean formula (DQBF), is a new logical formalism that allows compact encoding of NEXPTIME decision problems under uncertainty. Despite potentially broad applications, a decision procedure for DSSAT remains lacking. In this work, we present the first sound and complete resolution calculus for DSSAT. The resolution system deduces the maximum satisfying probability of a DSSAT formula and provides a witnessing certificate. We also show that when the special case of SSAT formulas is considered, the DSSAT resolution calculus p-simulates a known SSAT resolution scheme. Our result may pave a theoretical foundation for further development and certification of DSSAT solvers.
Citation
@article{luo_resolution_2021,
author = {Luo, Yun-Rong and Cheng, Che and Jiang, Jie-Hong},
year = {2023},
month = {08},
pages = {},
title = {A Resolution Proof System for Dependency Stochastic Boolean Satisfiability},
volume = {67},
journal = {Journal of Automated Reasoning},
doi = {10.1007/s10817-023-09670-6}
}