Research map / Learning theory and algorithms / Combinatorial and search optimization
Unifying Decision and Function Queries in Stochastic Boolean Satisfiability
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.
Enriches stochastic Boolean satisfiability (SSAT) with arbitrarily placed threshold quantifiers (SSAT(Θ)), proves it is PSPACE-complete, and builds the solver ClauSSat(Θ) evaluated on DTMC parameter synthesis and converted SSAT benchmarks.
Problem
The decision version of SSAT imposes only a single outermost threshold quantification, which restricts its expressive power and prevents unified handling of decision and function queries.
Approach
Add a threshold quantifier that can be placed at arbitrary positions in the SSAT prefix, so that SSAT(Θ) unifies decision and function queries, remains in PSPACE, and subsumes counting hierarchy languages; a solver extends ClauSSat with modified quantification levels and disabled pruning for the R-Θ-R alternation.
Key results
- SSAT(Θ) decision problem is shown PSPACE-complete, while subsuming counting formulas and the counting hierarchy.
- ClauSSat(Θ) solves parameter synthesis instances (Crowds, range [2..4] and [2..6]) with k up to 4 within the 1000-second limit, with run times from 0.07 s to 658 s.
- Inserting threshold quantifiers into SSAT benchmarks generally slows solving; e.g., stracomp instances solved in under 1 s as SSAT time out as SSAT(Θ) once random variables reach 30.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| increase the k-step bound from k=1 to k=4 | ClauSSat(Θ) on Crowds parameter synthesis [2..4] · Crowds parameter synthesis [2..4] | runtime (s): 9.13 -> 554.75 | Hurt |
| increase the k-step bound from k=1 to k=4 | ClauSSat(Θ) on Crowds parameter synthesis [2..6] · Crowds parameter synthesis [2..6] | runtime (s): 25.00 -> 658.14 | Hurt |
| insert a threshold quantifier into tlc instances | ClauSSat on tlc · tlc depth-7, depth-8, and depth-9 | runtime (s): 0.56 -> 0.47; 0.73 -> 0.61; 0.92 -> 0.78 | Helped |
| insert a threshold quantifier into gttt instances | ClauSSat on gttt · gttt 2_2_0010, 2_2_001020, and 2_2_000111 | runtime (s): 10.05 -> 26.85; 144.16 -> 310.16; 145.36 -> 298.59 | Hurt |
| insert a threshold quantifier into Robot instances | ClauSSat on Robot · Robot 8, 9, and 10 | runtime (s): 41.97 -> 61.14; 50.32 -> 34.35; 63.78 -> 286.01 | Mixed |
| insert a threshold quantifier into stracomp instances | ClauSSat on stracomp · stracomp 25.9, 30.9, and 35.9 | runtime (s): 0.45 -> 309.74; 0.38 -> TO; 0.37 -> TO | Hurt |
| increase the k-step bound | ClauSSat(Θ) on Crowds parameter synthesis · Crowds parameter synthesis | runtime (s) | Hurt |
Surprising findings
- On one Robot instance, the SSAT(Θ) variant solved faster than the original SSAT instance (34.35 s vs 50.32 s).
Limitations
- Pruning techniques are disabled for the R-Θ-R alternation, which hurts efficiency.
- SharpSSAT's component decomposition does not hold for SSAT(Θ), so it could not be directly extended.
- Parameter synthesis and model-checking instances grow too large for k=5 and larger parameter ranges within the time limit.
Experimental setup
Datasets: Crowds protocol DTMC instances SSAT benchmarks from ClauSSat (tlc, gttt, Robot, stracomp)
Benchmarks: Crowds parameter synthesis instances SSAT(Θ) instances converted from ClauSSat benchmarks
Metrics: run time (s) number of clauses number of variables
Baselines: SSAT solver (ClauSSat) Algorithm 1 naive evaluation
Builds on: ClauSSat SSAT QBF Counting Hierarchy BPCTL
Closest papers by meaning
- A Sharp Leap from Quantified Boolean Formula to Stochastic Boolean Satisfiability Solving (AAAI 2021 · similarity 0.96)
- SharpSSAT: A Witness-Generating Stochastic Boolean Satisfiability Solver (AAAI 2023 · similarity 0.93)
- Dependency Stochastic Boolean Satisfiability: A Logical Formalism for NEXPTIME Decision Problems with Uncertainty (AAAI 2021 · similarity 0.93)
- Lifting (D)QBF Preprocessing and Solving Techniques to (D)SSAT (AAAI 2023 · similarity 0.91)
- Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking (AAAI 2025 · similarity 0.86)
- SAT-Based Tree Decomposition with Iterative Cascading Policy Selection (AAAI 2024 · similarity 0.84)
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.