Fix #571: Add QuantifiedBooleanFormulas model#625
Merged
Conversation
Co-Authored-By: Claude Opus 4.6 <[email protected]>
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #625 +/- ##
==========================================
- Coverage 97.54% 97.53% -0.01%
==========================================
Files 371 373 +2
Lines 46958 47182 +224
==========================================
+ Hits 45803 46020 +217
- Misses 1155 1162 +7 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
Implement the canonical PSPACE-complete problem: given a fully quantified Boolean formula with alternating universal/existential quantifiers, determine whether it is true. Includes model, CLI support, paper entry, and comprehensive tests. Closes #571 Co-Authored-By: Claude Opus 4.6 <[email protected]>
Contributor
|
Autonomous Conflicts:
The board item was moved to |
Co-Authored-By: Claude Opus 4.6 (1M context) <[email protected]>
Add missing display_name, aliases, and dimensions fields to ProblemSchemaEntry, and add `default sat` prefix to declare_variants! macro to match the current API after merging main. Co-Authored-By: Claude Opus 4.6 (1M context) <[email protected]>
Register QBF in the example-db chain so `pred create --example` and paper exports include a canonical instance. Co-Authored-By: Claude Opus 4.6 (1M context) <[email protected]>
Replaces hand-written paper example with data loaded from the canonical example database, consistent with other problem definitions. Co-Authored-By: Claude Opus 4.6 (1M context) <[email protected]>
Co-Authored-By: Claude Opus 4.6 (1M context) <[email protected]>
The SequencingToMinimizeWeightedCompletionTime paper section was accessing x.optimal (non-existent) instead of x.optimal_config and x.optimal_value. Pre-existing error from main. Co-Authored-By: Claude Opus 4.6 (1M context) <[email protected]>
isPANN
approved these changes
Mar 20, 2026
3 tasks
QBF is a PSPACE-complete two-player game problem. Following the established pattern (GeneralizedHex), dims() returns [] and evaluate([]) runs the full game-tree search via is_true(). This fixes a semantic inconsistency where evaluate() was only checking CNF matrix satisfaction without quantifier semantics, making BruteForce treat QBF as plain SAT. Co-Authored-By: Claude Opus 4.6 (1M context) <[email protected]>
Co-Authored-By: Claude Opus 4.6 (1M context) <[email protected]>
Resolved merge conflicts (both-sides-added-entries pattern) in reductions.typ, references.bib, and cli.rs. Removed duplicate bib entries (johnson1983, kolliopoulos2007, raiha1981) introduced by the merge. Co-Authored-By: Claude Opus 4.6 (1M context) <[email protected]>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds the
QuantifiedBooleanFormulas(QBF) problem model — the canonical PSPACE-complete problem. Given a fully quantified Boolean formula with alternating universal and existential quantifiers, determine whether it is true.Fixes #571