Fix #571: Add QuantifiedBooleanFormulas model

docs/paper/examples/maximumindependentset_to_maximumclique.json

@@ -31,8 +31,8 @@
   "target": {
     "problem": "MaximumClique",
     "variant": {
-      "weight": "i32",
-      "graph": "SimpleGraph"
+      "graph": "SimpleGraph",
+      "weight": "i32"
     },
     "instance": {
       "edges": [

docs/paper/reductions.typ

@@ -116,39 +116,40 @@
   "Partition": [Partition],
   "MinimumFeedbackArcSet": [Minimum Feedback Arc Set],
   "MinimumFeedbackVertexSet": [Minimum Feedback Vertex Set],
-  "SteinerTreeInGraphs": [Steiner Tree in Graphs],
+  "ConjunctiveBooleanQuery": [Conjunctive Boolean Query],
+  "ConsecutiveBlockMinimization": [Consecutive Block Minimization],
+  "ConsecutiveOnesSubmatrix": [Consecutive Ones Submatrix],
+  "DirectedTwoCommodityIntegralFlow": [Directed Two-Commodity Integral Flow],
+  "FlowShopScheduling": [Flow Shop Scheduling],
   "MinimumCutIntoBoundedSets": [Minimum Cut Into Bounded Sets],
-  "MultipleChoiceBranching": [Multiple Choice Branching],
-  "PartitionIntoPathsOfLength2": [Partition into Paths of Length 2],
-  "ResourceConstrainedScheduling": [Resource Constrained Scheduling],
-  "QuadraticAssignment": [Quadratic Assignment],
-  "SequencingWithReleaseTimesAndDeadlines": [Sequencing with Release Times and Deadlines],
-  "ShortestCommonSupersequence": [Shortest Common Supersequence],
   "MinimumSumMulticenter": [Minimum Sum Multicenter],
+  "MinimumTardinessSequencing": [Minimum Tardiness Sequencing],
+  "MultipleChoiceBranching": [Multiple Choice Branching],
   "MultipleCopyFileAllocation": [Multiple Copy File Allocation],
-  "SteinerTree": [Steiner Tree],
-  "StrongConnectivityAugmentation": [Strong Connectivity Augmentation],
-  "SubgraphIsomorphism": [Subgraph Isomorphism],
-  "PartitionIntoTriangles": [Partition Into Triangles],
-  "PrimeAttributeName": [Prime Attribute Name],
-  "FlowShopScheduling": [Flow Shop Scheduling],
   "MultiprocessorScheduling": [Multiprocessor Scheduling],
+  "PartitionIntoPathsOfLength2": [Partition into Paths of Length 2],
+  "PartitionIntoTriangles": [Partition Into Triangles],
   "PrecedenceConstrainedScheduling": [Precedence Constrained Scheduling],
+  "PrimeAttributeName": [Prime Attribute Name],
+  "QuadraticAssignment": [Quadratic Assignment],
+  "QuantifiedBooleanFormulas": [Quantified Boolean Formulas (QBF)],
+  "RectilinearPictureCompression": [Rectilinear Picture Compression],
+  "ResourceConstrainedScheduling": [Resource Constrained Scheduling],
   "SchedulingWithIndividualDeadlines": [Scheduling With Individual Deadlines],
-  "StaffScheduling": [Staff Scheduling],
-  "MinimumTardinessSequencing": [Minimum Tardiness Sequencing],
-  "ConsecutiveBlockMinimization": [Consecutive Block Minimization],
-  "ConsecutiveOnesSubmatrix": [Consecutive Ones Submatrix],
   "SequencingToMinimizeMaximumCumulativeCost": [Sequencing to Minimize Maximum Cumulative Cost],
   "SequencingToMinimizeWeightedCompletionTime": [Sequencing to Minimize Weighted Completion Time],
   "SequencingToMinimizeWeightedTardiness": [Sequencing to Minimize Weighted Tardiness],
+  "SequencingWithReleaseTimesAndDeadlines": [Sequencing with Release Times and Deadlines],
   "SequencingWithinIntervals": [Sequencing Within Intervals],
+  "ShortestCommonSupersequence": [Shortest Common Supersequence],
+  "StaffScheduling": [Staff Scheduling],
+  "SteinerTree": [Steiner Tree],
+  "SteinerTreeInGraphs": [Steiner Tree in Graphs],
+  "StringToStringCorrection": [String-to-String Correction],
+  "StrongConnectivityAugmentation": [Strong Connectivity Augmentation],
+  "SubgraphIsomorphism": [Subgraph Isomorphism],
   "SumOfSquaresPartition": [Sum of Squares Partition],
   "TwoDimensionalConsecutiveSets": [2-Dimensional Consecutive Sets],
-  "DirectedTwoCommodityIntegralFlow": [Directed Two-Commodity Integral Flow],
-  "ConjunctiveBooleanQuery": [Conjunctive Boolean Query],
-  "RectilinearPictureCompression": [Rectilinear Picture Compression],
-  "StringToStringCorrection": [String-to-String Correction],
 )
 
 // Definition label: "def:<ProblemName>" — each definition block must have a matching label
@@ -2485,6 +2486,26 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76],
   ]
 }
 
+#{
+  let x = load-model-example("QuantifiedBooleanFormulas")
+  let n = x.instance.num_vars
+  let m = x.instance.clauses.len()
+  let clauses = x.instance.clauses
+  let quantifiers = x.instance.quantifiers
+  let fmt-lit(l) = if l > 0 { $u_#l$ } else { $not u_#(-l)$ }
+  let fmt-clause(c) = $paren.l #c.literals.map(fmt-lit).join($or$) paren.r$
+  let fmt-quant(q, i) = if q == "Exists" { $exists u_#(i + 1)$ } else { $forall u_#(i + 1)$ }
+  [
+    #problem-def("QuantifiedBooleanFormulas")[
+      Given a set $U = {u_1, dots, u_n}$ of Boolean variables and a fully quantified Boolean formula $F = (Q_1 u_1)(Q_2 u_2) dots.c (Q_n u_n) E$, where each $Q_i in {exists, forall}$ is a quantifier and $E$ is a Boolean expression in CNF with $m$ clauses, determine whether $F$ is true.
+    ][
+    Quantified Boolean Formulas (QBF) is the canonical PSPACE-complete problem, established by #cite(<stockmeyer1973>, form: "prose"). QBF generalizes SAT by adding universal quantifiers ($forall$) alongside existential ones ($exists$), creating a two-player game semantics: the existential player chooses values for $exists$-variables, the universal player for $forall$-variables, and the formula is true iff the existential player has a winning strategy ensuring all clauses are satisfied. This quantifier alternation is the source of PSPACE-hardness and makes QBF the primary source of PSPACE-completeness reductions for combinatorial game problems. The problem remains PSPACE-complete even when $E$ is restricted to 3-CNF (Quantified 3-SAT), but is polynomial-time solvable when each clause has at most 2 literals @schaefer1978. The best known exact algorithm is brute-force game-tree evaluation in $O^*(2^n)$ time. For QBF with $m$ CNF clauses, #cite(<williams2002>, form: "prose") achieves $O^*(1.709^m)$ time.
+
+    *Example.* Consider $F = #quantifiers.enumerate().map(((i, q)) => fmt-quant(q, i)).join($space$) space #clauses.map(fmt-clause).join($and$)$ with $n = #n$ variables and $m = #m$ clauses. The existential player chooses $u_1 = 1$: then $C_1 = (1 or u_2) = 1$ and $C_2 = (1 or not u_2) = 1$ for any value of $u_2$. Hence $F$ is #x.optimal_value --- the existential player has a winning strategy.
+    ]
+  ]
+}
+
 == Specialized Problems
 
 #{