Takeshi Tsukada

Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking

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…