Research map / Learning theory and algorithms / Combinatorial and search optimization
Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Presents HOMCSAT, the first higher-order quantified Boolean formula (HOQBF) solver, which reduces HOSAT to higher-order model checking (via HORSAT2) and extracts Skolem functions from the model checker's witnesses.
Problem
Solving higher-order quantified Boolean satisfiability (HOSAT/HOQBF), which generalizes SAT, QBF, DQBF and SOQBF, has lacked any practical solver.
Approach
Translate a HOQBF into a higher-order functional program (with recursive enumeration structures for bool and function types) whose evaluation is true iff the formula is satisfiable, then decide it with a higher-order model checker; witnesses (intersection-type specifications) give Skolem functions.
Key results
- HOMCSAT correctly solved 18 of 21 HOSAT benchmark instances, with timeouts on sym-asym-bb and out-of-memory on sym-cl-uniq, trans-cl-uniq, cps-arity2 (among others)
- Simple instances such as example1 and sym-asym-b are solved in under 0.2 seconds, while aaai23 ex2 takes 12.3 seconds and refl-cl-uniq takes 124.7 seconds
- The reduction is linear-time in formula size and maps an order-n formula to order-(n+1) model checking
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Expand the relation domain from bool to bool × bool | HOMCSAT · sym-asym-b to sym-asym-bb | runtime: under 0.2 seconds -> timed out (300 seconds) | Hurt |
Surprising findings
- The backend HORSAT2 struggles with the extensive branching caused by higher-order quantifiers, unlike typical program-verification inputs, leading to very large intersection refinement types.
Limitations
- HORSAT2 backend scales poorly with branching from many quantifiers, causing timeouts and out-of-memory failures
- Evaluation uses only a small set of 21 preliminary benchmark instances
- No abstraction, pruning, or propagation techniques from SAT/QBF solvers are yet incorporated
Experimental setup
Datasets: HOSAT benchmark set of 21 problems
Benchmarks: HOSAT benchmark set (21 instances)
Metrics: solved result (SAT/UNSAT correctness) solving time (s) timeouts and out-of-memory
Builds on: higher-order model checking (Ong 2006) HORSAT2 HOQBF complexity (Chistikov et al. 2022) refinement intersection types (Kobayashi 2013)
Closest papers by meaning
- Second-Order Quantified Boolean Logic (AAAI 2023 · similarity 0.90)
- Unifying Decision and Function Queries in Stochastic Boolean Satisfiability (AAAI 2024 · similarity 0.86)
- An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes (AAAI 2024 · similarity 0.86)
- Computationally Hard Problems Are Hard for QBF Proof Systems Too (AAAI 2025 · similarity 0.86)
- The Impact of Literal Sorting on Cardinality Constraint Encodings (AAAI 2025 · similarity 0.85)
- Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization (AAAI 2025 · similarity 0.85)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.