Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking
Abstract
The satisfiability (SAT) problem of higher-order quantified Boolean formula (HOQBF) emerged as a natural generalization of SAT, quantified SAT, and second-order quantified SAT. It allows succinct encoding of k-EXPTIME problems beyond the reach of prior Boolean satisfiability formulations, but its application was hampered by the lack of solvers. In this paper, we present the first HOQBF solver that leverages techniques from the model-checking community. Our HOQBF solver is based on reduction to higher-order model checking, which is a generalization from model checking of while-programs to that of higher-order functional programs. The ability of a higher-order model checker to deal with higher-order functions in a program is used to reason about higher-order quantifiers in HOQBF.
Cite
Text
Unno et al. "Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking." AAAI Conference on Artificial Intelligence, 2025. doi:10.1609/AAAI.V39I11.33237Markdown
[Unno et al. "Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking." AAAI Conference on Artificial Intelligence, 2025.](https://mlanthology.org/aaai/2025/unno2025aaai-solving/) doi:10.1609/AAAI.V39I11.33237BibTeX
@inproceedings{unno2025aaai-solving,
title = {{Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking}},
author = {Unno, Hiroshi and Tsukada, Takeshi and Jiang, Jie-Hong Roland},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2025},
pages = {11372-11380},
doi = {10.1609/AAAI.V39I11.33237},
url = {https://mlanthology.org/aaai/2025/unno2025aaai-solving/}
}