diff --git a/docs/paper/examples/maximumindependentset_to_maximumclique.json b/docs/paper/examples/maximumindependentset_to_maximumclique.json index e8be9c621..abcd99576 100644 --- a/docs/paper/examples/maximumindependentset_to_maximumclique.json +++ b/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": [ diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index b00d592a3..a66536baf 100644 --- a/docs/paper/reductions.typ +++ b/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:" — 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(, 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(, 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 #{ diff --git a/docs/paper/references.bib b/docs/paper/references.bib index 9b87db469..fae878926 100644 --- a/docs/paper/references.bib +++ b/docs/paper/references.bib @@ -802,6 +802,17 @@ @article{cygan2014 doi = {10.1137/140990255} } +@article{alon1995, + author = {Noga Alon and Raphael Yuster and Uri Zwick}, + title = {Color-coding}, + journal = {Journal of the ACM}, + volume = {42}, + number = {4}, + pages = {844--856}, + year = {1995}, + doi = {10.1145/210332.210337} +} + @inproceedings{bjorklund2007, author = {Andreas Bj\"{o}rklund and Thore Husfeldt and Petteri Kaski and Mikko Koivisto}, title = {Fourier Meets M\"{o}bius: Fast Subset Convolution}, @@ -811,17 +822,6 @@ @inproceedings{bjorklund2007 doi = {10.1145/1250790.1250801} } -@inproceedings{nederlof2009, - author = {Jesper Nederlof}, - title = {Fast Polynomial-Space Algorithms Using {M\"{o}bius} Inversion: Improving on {Steiner} Tree and Related Problems}, - booktitle = {Proceedings of the 36th International Colloquium on Automata, Languages and Programming (ICALP)}, - series = {LNCS}, - volume = {5555}, - pages = {713--725}, - year = {2009}, - doi = {10.1007/978-3-642-02927-1_59} -} - @article{johnson1983, author = {David S. Johnson and Kenneth A. Niemi}, title = {On Knapsacks, Partitions, and a New Dynamic Programming Technique for Trees}, @@ -844,6 +844,17 @@ @article{kolliopoulos2007 doi = {10.1016/j.dam.2006.09.003} } +@inproceedings{nederlof2009, + author = {Jesper Nederlof}, + title = {Fast Polynomial-Space Algorithms Using {M\"{o}bius} Inversion: Improving on {Steiner} Tree and Related Problems}, + booktitle = {Proceedings of the 36th International Colloquium on Automata, Languages and Programming (ICALP)}, + series = {LNCS}, + volume = {5555}, + pages = {713--725}, + year = {2009}, + doi = {10.1007/978-3-642-02927-1_59} +} + @article{raiha1981, author = {Kari-Jouko R{\"a}ih{\"a} and Esko Ukkonen}, title = {The Shortest Common Supersequence Problem over Binary Alphabet is {NP}-Complete}, @@ -866,134 +877,6 @@ @article{bodlaender2012 doi = {10.1007/s00224-011-9312-0} } -@article{chen2008, - author = {Jianer Chen and Yang Liu and Songjian Lu and Barry O'Sullivan and Igor Razgon}, - title = {A Fixed-Parameter Algorithm for the Directed Feedback Vertex Set Problem}, - journal = {Journal of the ACM}, - volume = {55}, - number = {5}, - pages = {1--19}, - year = {2008}, - doi = {10.1145/1411509.1411511} -} - -@article{lucchesi1978, - author = {Cl\'audio L. Lucchesi and Daniel H. Younger}, - title = {A Minimax Theorem for Directed Graphs}, - journal = {Journal of the London Mathematical Society}, - volume = {s2-17}, - number = {3}, - pages = {369--374}, - year = {1978}, - doi = {10.1112/jlms/s2-17.3.369} -} - -@article{lucchesi1978keys, - author = {Cl\'audio L. Lucchesi and Sylvia L. Osborn}, - title = {Candidate Keys for Relations}, - journal = {Journal of Computer and System Sciences}, - volume = {17}, - number = {2}, - pages = {270--279}, - year = {1978}, - doi = {10.1016/0022-0000(78)90009-0} -} - -@article{lenstra1976, - author = {Jan Karel Lenstra and Alexander H. G. Rinnooy Kan}, - title = {On General Routing Problems}, - journal = {Networks}, - volume = {6}, - number = {3}, - pages = {273--280}, - year = {1976}, - doi = {10.1002/net.3230060305} -} - -@article{frederickson1979, - author = {Greg N. Frederickson}, - title = {Approximation Algorithms for Some Postman Problems}, - journal = {Journal of the ACM}, - volume = {26}, - number = {3}, - pages = {538--554}, - year = {1979}, - doi = {10.1145/322139.322150} -} - -@article{alon1995, - author = {Noga Alon and Raphael Yuster and Uri Zwick}, - title = {Color-coding}, - journal = {Journal of the ACM}, - volume = {42}, - number = {4}, - pages = {844--856}, - year = {1995}, - doi = {10.1145/210332.210337} -} - -@inproceedings{cordella2004, - author = {Luigi P. Cordella and Pasquale Foggia and Carlo Sansone and Mario Vento}, - title = {A (Sub)Graph Isomorphism Algorithm for Matching Large Graphs}, - booktitle = {IEEE Transactions on Pattern Analysis and Machine Intelligence}, - volume = {26}, - number = {10}, - pages = {1367--1372}, - year = {2004}, - doi = {10.1109/TPAMI.2004.75} -} - -@article{even1976, - author = {Shimon Even and Alon Itai and Adi Shamir}, - title = {On the Complexity of Timetable and Multicommodity Flow Problems}, - journal = {SIAM Journal on Computing}, - volume = {5}, - number = {4}, - pages = {691--703}, - year = {1976}, - doi = {10.1137/0205048} -} - -@inproceedings{chandra1977, - author = {Ashok K. Chandra and Philip M. Merlin}, - title = {Optimal Implementation of Conjunctive Queries in Relational Data Bases}, - booktitle = {Proceedings of the 9th Annual ACM Symposium on Theory of Computing (STOC)}, - pages = {77--90}, - year = {1977}, - doi = {10.1145/800105.803397} -} - -@article{gottlob2002, - author = {Georg Gottlob and Nicola Leone and Francesco Scarcello}, - title = {Hypertree Decompositions and Tractable Queries}, - journal = {Journal of Computer and System Sciences}, - volume = {64}, - number = {3}, - pages = {579--627}, - year = {2002}, - doi = {10.1006/jcss.2001.1809} -} - -@inproceedings{kolaitis1998, - author = {Phokion G. Kolaitis and Moshe Y. Vardi}, - title = {Conjunctive-Query Containment and Constraint Satisfaction}, - booktitle = {Proceedings of the 17th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS)}, - pages = {205--213}, - year = {1998}, - doi = {10.1145/275487.275511} -} - -@article{papadimitriou1982, - author = {Christos H. Papadimitriou and Mihalis Yannakakis}, - title = {The Complexity of Restricted Spanning Tree Problems}, - journal = {Journal of the ACM}, - volume = {29}, - number = {2}, - pages = {285--309}, - year = {1982}, - doi = {10.1145/322307.322309} -} - @article{booth1976, author = {Booth, Kellogg S. and Lueker, George S.}, title = {Testing for the consecutive ones property, interval graphs, and graph planarity using {PQ}-tree algorithms}, @@ -1004,6 +887,13 @@ @article{booth1976 year = {1976} } +@phdthesis{booth1975, + author = {Booth, Kellogg S.}, + title = {{PQ}-Tree Algorithms}, + school = {University of California, Berkeley}, + year = {1975} +} + @article{boothlueker1976, author = {Kellogg S. Booth and George S. Lueker}, title = {Testing for the Consecutive Ones Property, Interval Graphs, and Graph Planarity Using {PQ}-Tree Algorithms}, @@ -1015,11 +905,24 @@ @article{boothlueker1976 doi = {10.1016/S0022-0000(76)80045-1} } -@phdthesis{booth1975, - author = {Booth, Kellogg S.}, - title = {{PQ}-Tree Algorithms}, - school = {University of California, Berkeley}, - year = {1975} +@inproceedings{chandra1977, + author = {Ashok K. Chandra and Philip M. Merlin}, + title = {Optimal Implementation of Conjunctive Queries in Relational Data Bases}, + booktitle = {Proceedings of the 9th Annual ACM Symposium on Theory of Computing (STOC)}, + pages = {77--90}, + year = {1977}, + doi = {10.1145/800105.803397} +} + +@article{chen2008, + author = {Jianer Chen and Yang Liu and Songjian Lu and Barry O'Sullivan and Igor Razgon}, + title = {A Fixed-Parameter Algorithm for the Directed Feedback Vertex Set Problem}, + journal = {Journal of the ACM}, + volume = {55}, + number = {5}, + pages = {1--19}, + year = {2008}, + doi = {10.1145/1411509.1411511} } @article{chopra1996, @@ -1043,6 +946,17 @@ @article{coffman1972 doi = {10.1007/BF00288685} } +@inproceedings{cordella2004, + author = {Luigi P. Cordella and Pasquale Foggia and Carlo Sansone and Mario Vento}, + title = {A (Sub)Graph Isomorphism Algorithm for Matching Large Graphs}, + booktitle = {IEEE Transactions on Pattern Analysis and Machine Intelligence}, + volume = {26}, + number = {10}, + pages = {1367--1372}, + year = {2004}, + doi = {10.1109/TPAMI.2004.75} +} + @article{eppstein1992, author = {David Eppstein}, title = {Finding the $k$ Smallest Spanning Trees}, @@ -1054,6 +968,50 @@ @article{eppstein1992 doi = {10.1007/BF01994880} } +@article{even1976, + author = {Shimon Even and Alon Itai and Adi Shamir}, + title = {On the Complexity of Timetable and Multicommodity Flow Problems}, + journal = {SIAM Journal on Computing}, + volume = {5}, + number = {4}, + pages = {691--703}, + year = {1976}, + doi = {10.1137/0205048} +} + +@article{frederickson1979, + author = {Greg N. Frederickson}, + title = {Approximation Algorithms for Some Postman Problems}, + journal = {Journal of the ACM}, + volume = {26}, + number = {3}, + pages = {538--554}, + year = {1979}, + doi = {10.1145/322139.322150} +} + +@article{gottlob2002, + author = {Georg Gottlob and Nicola Leone and Francesco Scarcello}, + title = {Hypertree Decompositions and Tractable Queries}, + journal = {Journal of Computer and System Sciences}, + volume = {64}, + number = {3}, + pages = {579--627}, + year = {2002}, + doi = {10.1006/jcss.2001.1809} +} + +@article{haddadi2008, + author = {Salim Haddadi and Zohra Layouni}, + title = {Consecutive block minimization is 1.5-approximable}, + journal = {Information Processing Letters}, + volume = {108}, + number = {3}, + pages = {161--163}, + year = {2008}, + doi = {10.1016/j.ipl.2008.05.003} +} + @techreport{Heidari2022, author = {Heidari, Shahrokh and Dinneen, Michael J. and Delmas, Patrice}, title = {An Equivalent {QUBO} Model to the Minimum Multi-Way Cut Problem}, @@ -1073,6 +1031,15 @@ @article{hu1961 doi = {10.1287/opre.9.6.841} } +@inproceedings{kolaitis1998, + author = {Phokion G. Kolaitis and Moshe Y. Vardi}, + title = {Conjunctive-Query Containment and Constraint Satisfaction}, + booktitle = {Proceedings of the 17th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS)}, + pages = {205--213}, + year = {1998}, + doi = {10.1145/275487.275511} +} + @article{kou1977, author = {Lawrence T. Kou}, title = {Polynomial Complete Consecutive Information Retrieval Problems}, @@ -1084,17 +1051,6 @@ @article{kou1977 doi = {10.1137/0206005} } -@article{haddadi2008, - author = {Salim Haddadi and Zohra Layouni}, - title = {Consecutive block minimization is 1.5-approximable}, - journal = {Information Processing Letters}, - volume = {108}, - number = {3}, - pages = {161--163}, - year = {2008}, - doi = {10.1016/j.ipl.2008.05.003} -} - @article{lawler1972, author = {Eugene L. Lawler}, title = {A Procedure for Computing the $K$ Best Solutions to Discrete Optimization Problems and Its Application to the Shortest Path Problem}, @@ -1106,6 +1062,17 @@ @article{lawler1972 doi = {10.1287/mnsc.18.7.401} } +@article{lenstra1976, + author = {Jan Karel Lenstra and Alexander H. G. Rinnooy Kan}, + title = {On General Routing Problems}, + journal = {Networks}, + volume = {6}, + number = {3}, + pages = {273--280}, + year = {1976}, + doi = {10.1002/net.3230060305} +} + @article{lenstra1978, author = {Jan Karel Lenstra and Alexander H. G. Rinnooy Kan}, title = {Complexity of Scheduling under Precedence Constraints}, @@ -1129,12 +1096,37 @@ @inproceedings{lipski1977fct doi = {10.1007/3-540-08442-8_115} } -@book{papadimitriou-steiglitz1982, - author = {Christos H. Papadimitriou and Kenneth Steiglitz}, - title = {Combinatorial Optimization: Algorithms and Complexity}, - publisher = {Prentice-Hall}, - address = {Englewood Cliffs, NJ}, - year = {1982} +@article{lucchesi1978, + author = {Cl\'audio L. Lucchesi and Daniel H. Younger}, + title = {A Minimax Theorem for Directed Graphs}, + journal = {Journal of the London Mathematical Society}, + volume = {s2-17}, + number = {3}, + pages = {369--374}, + year = {1978}, + doi = {10.1112/jlms/s2-17.3.369} +} + +@article{lucchesi1978keys, + author = {Cl\'audio L. Lucchesi and Sylvia L. Osborn}, + title = {Candidate Keys for Relations}, + journal = {Journal of Computer and System Sciences}, + volume = {17}, + number = {2}, + pages = {270--279}, + year = {1978}, + doi = {10.1016/0022-0000(78)90009-0} +} + +@article{papadimitriou1982, + author = {Christos H. Papadimitriou and Mihalis Yannakakis}, + title = {The Complexity of Restricted Spanning Tree Problems}, + journal = {Journal of the ACM}, + volume = {29}, + number = {2}, + pages = {285--309}, + year = {1982}, + doi = {10.1145/322307.322309} } @inproceedings{papadimitriou1979, @@ -1146,6 +1138,32 @@ @inproceedings{papadimitriou1979 doi = {10.1145/800135.804393} } +@book{papadimitriou-steiglitz1982, + author = {Christos H. Papadimitriou and Kenneth Steiglitz}, + title = {Combinatorial Optimization: Algorithms and Complexity}, + publisher = {Prentice-Hall}, + address = {Englewood Cliffs, NJ}, + year = {1982} +} + +@article{schaefer1978, + author = {Thomas J. Schaefer}, + title = {The Complexity of Satisfiability Problems}, + journal = {Conference Record of the 10th Annual ACM Symposium on Theory of Computing (STOC)}, + pages = {216--226}, + year = {1978}, + doi = {10.1145/800133.804350} +} + +@inproceedings{stockmeyer1973, + author = {Larry J. Stockmeyer and Albert R. Meyer}, + title = {Word Problems Requiring Exponential Time: Preliminary Report}, + booktitle = {Proceedings of the 5th Annual ACM Symposium on Theory of Computing (STOC)}, + pages = {1--9}, + year = {1973}, + doi = {10.1145/800125.804029} +} + @article{ullman1975, author = {Jeffrey D. Ullman}, title = {NP-Complete Scheduling Problems}, @@ -1156,3 +1174,11 @@ @article{ullman1975 year = {1975}, doi = {10.1016/S0022-0000(75)80008-0} } + +@inproceedings{williams2002, + author = {Ryan Williams}, + title = {Algorithms for Quantified Boolean Formulas}, + booktitle = {Proceedings of the 13th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA)}, + pages = {299--307}, + year = {2002} +} diff --git a/docs/plans/2026-03-13-quantified-boolean-formulas-model.md b/docs/plans/2026-03-13-quantified-boolean-formulas-model.md new file mode 100644 index 000000000..767650d0a --- /dev/null +++ b/docs/plans/2026-03-13-quantified-boolean-formulas-model.md @@ -0,0 +1,99 @@ +# Plan: Add QuantifiedBooleanFormulas Model + +**Issue:** #571 — [Model] QuantifiedBooleanFormulas(qbf)(*) +**Skill:** add-model + +## Information Checklist + +| # | Item | Value | +|---|------|-------| +| 1 | Problem name | `QuantifiedBooleanFormulas` | +| 2 | Mathematical definition | Given a fully quantified Boolean formula F=(Q_1 u_1)...(Q_n u_n)E where each Q_i is ∀ or ∃ and E is a CNF formula, determine whether F is true | +| 3 | Problem type | Satisfaction (Metric = bool) | +| 4 | Type parameters | None | +| 5 | Struct fields | `num_vars: usize`, `quantifiers: Vec`, `clauses: Vec` | +| 6 | Configuration space | `vec![2; num_vars]` — each variable is 0 or 1 | +| 7 | Feasibility check | A config represents a full assignment; evaluate returns true iff the formula is true under that assignment (ignoring quantifier semantics in evaluate — quantifier semantics are captured by the brute-force solver's game-tree search) | +| 8 | Objective function | `bool` — satisfied or not under the given assignment | +| 9 | Best known exact algorithm | O(2^n) brute-force game-tree evaluation (Stockmeyer & Meyer, 1973); complexity string: `"2^num_vars"` | +| 10 | Solving strategy | BruteForce works — but needs special handling: `find_satisfying` must find a *witnessing assignment* for the existential variables such that for all universal variable assignments, E is satisfied. The `evaluate()` method just checks if a single full assignment satisfies the CNF matrix E (standard SAT-like evaluation). | +| 11 | Category | `formula` | + +## Design Decisions + +### evaluate() Semantics +Following the check-issue comment's analysis, `evaluate()` will treat the config as a full assignment and check whether the CNF matrix E is satisfied. This is consistent with how the `Problem` trait works (a single config → metric). The quantifier semantics are implicit: a QBF is TRUE iff there exists an assignment to existential variables such that for ALL universal variable assignments, E evaluates to true. The brute-force solver enumerates all 2^n assignments and returns any satisfying one. + +### Quantifier Enum +Define a `Quantifier` enum with `Exists` and `ForAll` variants, serializable with serde. + +### Reusing CNFClause +Reuse the existing `CNFClause` type from `sat.rs` (1-indexed signed integers). + +## Steps + +### Step 1: Implement the model (`src/models/formula/qbf.rs`) + +1. Define `Quantifier` enum: `{ Exists, ForAll }` with `Debug, Clone, PartialEq, Eq, Serialize, Deserialize` +2. Define `QuantifiedBooleanFormulas` struct with fields: `num_vars`, `quantifiers`, `clauses` +3. Add `inventory::submit!` for `ProblemSchemaEntry` +4. Constructor: `new(num_vars, quantifiers, clauses)` with assertion that `quantifiers.len() == num_vars` +5. Getter methods: `num_vars()`, `num_clauses()`, `quantifiers()`, `clauses()` +6. Implement `Problem` trait: + - `NAME = "QuantifiedBooleanFormulas"` + - `Metric = bool` + - `dims() = vec![2; num_vars]` + - `evaluate(config)` — convert to bool assignment, check if all clauses are satisfied (same as SAT) + - `variant() = variant_params![]` +7. Implement `SatisfactionProblem` (marker trait) +8. Add `declare_variants!` with complexity `"2^num_vars"` +9. Add `is_true(&self) -> bool` method that implements proper QBF game-tree evaluation (recursive minimax) +10. Link test file: `#[cfg(test)] #[path = "../../unit_tests/models/formula/qbf.rs"] mod tests;` + +### Step 2: Register the model + +1. `src/models/formula/mod.rs` — add `pub(crate) mod qbf;` and `pub use qbf::{QuantifiedBooleanFormulas, Quantifier};` +2. `src/models/mod.rs` — add `QuantifiedBooleanFormulas, Quantifier` to the formula re-export line +3. `src/lib.rs` prelude — add `QuantifiedBooleanFormulas` to the formula prelude exports + +### Step 3: Register in CLI + +1. `problemreductions-cli/src/dispatch.rs`: + - Add import for `QuantifiedBooleanFormulas` + - Add `"QuantifiedBooleanFormulas" => deser_sat::(data)` in `load_problem()` + - Add `"QuantifiedBooleanFormulas" => try_ser::(any)` in `serialize_any_problem()` +2. `problemreductions-cli/src/problem_name.rs`: + - Add `"qbf" | "quantifiedbooleanformulas" => "QuantifiedBooleanFormulas".to_string()` in `resolve_alias()` + - Add `("QBF", "QuantifiedBooleanFormulas")` to `ALIASES` array + +### Step 4: Add CLI creation support + +1. `problemreductions-cli/src/commands/create.rs`: + - Add `"QuantifiedBooleanFormulas"` match arm: parse `--num-vars`, `--clauses`, and a new `--quantifiers` flag + - Add to `example_for()`: `"QuantifiedBooleanFormulas" => "--num-vars 3 --clauses \"1,2;-1,3\" --quantifiers \"E,A,E\""` +2. `problemreductions-cli/src/cli.rs`: + - Add `--quantifiers` flag to `CreateArgs`: `pub quantifiers: Option` + - Update `all_data_flags_empty()` to include `args.quantifiers.is_none()` + - Add QBF to "Flags by problem type" table + +### Step 5: Write unit tests (`src/unit_tests/models/formula/qbf.rs`) + +1. `test_quantifier_creation` — verify Quantifier enum +2. `test_qbf_creation` — construct instance, verify dimensions +3. `test_qbf_evaluate` — verify evaluate() on valid/invalid assignments +4. `test_qbf_is_true` — verify game-tree evaluation for known true/false instances +5. `test_qbf_solver` — verify brute-force solver finds satisfying assignments +6. `test_qbf_serialization` — round-trip serde test +7. `test_qbf_trivial` — empty formula, all-exists (reduces to SAT) + +### Step 6: Document in paper + +Add problem-def entry in `docs/paper/reductions.typ`: +- Add display name: `"QuantifiedBooleanFormulas": [Quantified Boolean Formulas (QBF)]` +- Add `#problem-def("QuantifiedBooleanFormulas")[...]` with formal definition and background + +### Step 7: Verify + +```bash +make test clippy fmt-check +``` diff --git a/problemreductions-cli/src/cli.rs b/problemreductions-cli/src/cli.rs index c92b68754..5c3bae2d1 100644 --- a/problemreductions-cli/src/cli.rs +++ b/problemreductions-cli/src/cli.rs @@ -265,6 +265,7 @@ Flags by problem type: LCS --strings, --bound [--alphabet-size] FAS --arcs [--weights] [--num-vertices] FVS --arcs [--weights] [--num-vertices] + QBF --num-vars, --clauses, --quantifiers SteinerTreeInGraphs --graph, --edge-weights, --terminals PartitionIntoPathsOfLength2 --graph ResourceConstrainedScheduling --num-processors, --resource-bounds, --resource-requirements, --deadline @@ -493,6 +494,9 @@ pub struct CreateArgs { /// Directed arcs for directed graph problems (e.g., 0>1,1>2,2>0) #[arg(long)] pub arcs: Option, + /// Quantifiers for QBF (comma-separated, E=Exists, A=ForAll, e.g., "E,A,E") + #[arg(long)] + pub quantifiers: Option, /// Size bound for partition sets (for MinimumCutIntoBoundedSets) #[arg(long)] pub size_bound: Option, diff --git a/problemreductions-cli/src/commands/create.rs b/problemreductions-cli/src/commands/create.rs index c66f87c9d..85fb53849 100644 --- a/problemreductions-cli/src/commands/create.rs +++ b/problemreductions-cli/src/commands/create.rs @@ -10,6 +10,7 @@ use problemreductions::export::{ModelExample, ProblemRef, ProblemSide, RuleExamp use problemreductions::models::algebraic::{ ClosestVectorProblem, ConsecutiveBlockMinimization, ConsecutiveOnesSubmatrix, BMF, }; +use problemreductions::models::formula::Quantifier; use problemreductions::models::graph::{ GeneralizedHex, GraphPartitioning, HamiltonianCircuit, HamiltonianPath, LengthBoundedDisjointPaths, MinimumCutIntoBoundedSets, MinimumMultiwayCut, @@ -97,6 +98,7 @@ fn all_data_flags_empty(args: &CreateArgs) -> bool { && args.strings.is_none() && args.costs.is_none() && args.arcs.is_none() + && args.quantifiers.is_none() && args.usage.is_none() && args.storage.is_none() && args.source.is_none() @@ -394,6 +396,9 @@ fn example_for(canonical: &str, graph_type: Option<&str>) -> &'static str { "--graph 0-1,1-2,2-3 --potential-edges 0-2:3,0-3:4,1-3:2 --budget 5" } "Satisfiability" => "--num-vars 3 --clauses \"1,2;-1,3\"", + "QuantifiedBooleanFormulas" => { + "--num-vars 3 --clauses \"1,2;-1,3\" --quantifiers \"E,A,E\"" + } "KSatisfiability" => "--num-vars 3 --clauses \"1,2,3;-1,2,-3\" --k 3", "QUBO" => "--matrix \"1,0.5;0.5,2\"", "QuadraticAssignment" => "--matrix \"0,5;5,0\" --distance-matrix \"0,1;1,0\"", @@ -1313,6 +1318,26 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> { util::ser_ksat(num_vars, clauses, k)? } + // QBF + "QuantifiedBooleanFormulas" => { + let num_vars = args.num_vars.ok_or_else(|| { + anyhow::anyhow!( + "QuantifiedBooleanFormulas requires --num-vars, --clauses, and --quantifiers\n\n\ + Usage: pred create QBF --num-vars 3 --clauses \"1,2;-1,3\" --quantifiers \"E,A,E\"" + ) + })?; + let clauses = parse_clauses(args)?; + let quantifiers = parse_quantifiers(args, num_vars)?; + ( + ser(QuantifiedBooleanFormulas::new( + num_vars, + quantifiers, + clauses, + ))?, + resolved_variant.clone(), + ) + } + // QuadraticAssignment "QuadraticAssignment" => { let cost_str = args.matrix.as_deref().ok_or_else(|| { @@ -3948,6 +3973,36 @@ fn parse_matrix(args: &CreateArgs) -> Result>> { .collect() } +/// Parse `--quantifiers` as comma-separated quantifier labels (E/A or Exists/ForAll). +/// E.g., "E,A,E" or "Exists,ForAll,Exists" +fn parse_quantifiers(args: &CreateArgs, num_vars: usize) -> Result> { + let q_str = args + .quantifiers + .as_deref() + .ok_or_else(|| anyhow::anyhow!("QBF requires --quantifiers (e.g., \"E,A,E\")"))?; + + let quantifiers: Vec = q_str + .split(',') + .map(|s| match s.trim().to_lowercase().as_str() { + "e" | "exists" => Ok(Quantifier::Exists), + "a" | "forall" => Ok(Quantifier::ForAll), + other => Err(anyhow::anyhow!( + "Invalid quantifier '{}': expected E/Exists or A/ForAll", + other + )), + }) + .collect::>>()?; + + if quantifiers.len() != num_vars { + bail!( + "Expected {} quantifiers but got {}", + num_vars, + quantifiers.len() + ); + } + Ok(quantifiers) +} + /// Parse a semicolon-separated matrix of i64 values. /// E.g., "0,5;5,0" fn parse_i64_matrix(s: &str) -> Result>> { @@ -4921,6 +4976,7 @@ mod tests { size_bound: None, usage: None, storage: None, + quantifiers: None, } } diff --git a/src/lib.rs b/src/lib.rs index 8fbb921ba..34ca7f66a 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -43,7 +43,9 @@ pub mod variant; pub mod prelude { // Problem types pub use crate::models::algebraic::{QuadraticAssignment, BMF, QUBO}; - pub use crate::models::formula::{CNFClause, CircuitSAT, KSatisfiability, Satisfiability}; + pub use crate::models::formula::{ + CNFClause, CircuitSAT, KSatisfiability, QuantifiedBooleanFormulas, Satisfiability, + }; pub use crate::models::graph::{ BalancedCompleteBipartiteSubgraph, BicliqueCover, BiconnectivityAugmentation, BoundedComponentSpanningForest, DirectedTwoCommodityIntegralFlow, GeneralizedHex, diff --git a/src/models/formula/mod.rs b/src/models/formula/mod.rs index 71459cfb4..568dc0760 100644 --- a/src/models/formula/mod.rs +++ b/src/models/formula/mod.rs @@ -4,13 +4,16 @@ //! - [`Satisfiability`]: Boolean satisfiability (SAT) with CNF clauses //! - [`KSatisfiability`]: K-SAT where each clause has exactly K literals //! - [`CircuitSAT`]: Boolean circuit satisfiability +//! - [`QuantifiedBooleanFormulas`]: Quantified Boolean Formulas (QBF) — PSPACE-complete pub(crate) mod circuit; pub(crate) mod ksat; +pub(crate) mod qbf; pub(crate) mod sat; pub use circuit::{Assignment, BooleanExpr, BooleanOp, Circuit, CircuitSAT}; pub use ksat::KSatisfiability; +pub use qbf::{QuantifiedBooleanFormulas, Quantifier}; pub use sat::{CNFClause, Satisfiability}; #[cfg(feature = "example-db")] @@ -19,5 +22,6 @@ pub(crate) fn canonical_model_example_specs() -> Vec", description: "Quantifier for each variable (Exists or ForAll)" }, + FieldInfo { name: "clauses", type_name: "Vec", description: "CNF clauses of the Boolean expression E" }, + ], + } +} + +/// Quantifier type for QBF variables. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)] +pub enum Quantifier { + /// Existential quantifier (∃) + Exists, + /// Universal quantifier (∀) + ForAll, +} + +/// Quantified Boolean Formulas (QBF) problem. +/// +/// Given a fully quantified Boolean formula F = (Q_1 u_1)...(Q_n u_n) E, +/// where each Q_i is ∀ or ∃ and E is in CNF, determine whether F is true. +/// +/// # Example +/// +/// ``` +/// use problemreductions::models::formula::{QuantifiedBooleanFormulas, Quantifier, CNFClause}; +/// use problemreductions::Problem; +/// +/// // F = ∃u_1 ∀u_2 (u_1 ∨ u_2) ∧ (u_1 ∨ ¬u_2) +/// let problem = QuantifiedBooleanFormulas::new( +/// 2, +/// vec![Quantifier::Exists, Quantifier::ForAll], +/// vec![ +/// CNFClause::new(vec![1, 2]), // u_1 OR u_2 +/// CNFClause::new(vec![1, -2]), // u_1 OR NOT u_2 +/// ], +/// ); +/// +/// // With u_1=true, both clauses are satisfied regardless of u_2 +/// assert!(problem.is_true()); +/// ``` +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct QuantifiedBooleanFormulas { + /// Number of variables. + num_vars: usize, + /// Quantifier for each variable (indexed 0..num_vars). + quantifiers: Vec, + /// Clauses in CNF representing the Boolean expression E. + clauses: Vec, +} + +impl QuantifiedBooleanFormulas { + /// Create a new QBF problem. + /// + /// # Panics + /// + /// Panics if `quantifiers.len() != num_vars`. + pub fn new(num_vars: usize, quantifiers: Vec, clauses: Vec) -> Self { + assert_eq!( + quantifiers.len(), + num_vars, + "quantifiers length ({}) must equal num_vars ({})", + quantifiers.len(), + num_vars + ); + Self { + num_vars, + quantifiers, + clauses, + } + } + + /// Get the number of variables. + pub fn num_vars(&self) -> usize { + self.num_vars + } + + /// Get the number of clauses. + pub fn num_clauses(&self) -> usize { + self.clauses.len() + } + + /// Get the quantifiers. + pub fn quantifiers(&self) -> &[Quantifier] { + &self.quantifiers + } + + /// Get the clauses. + pub fn clauses(&self) -> &[CNFClause] { + &self.clauses + } + + /// Evaluate whether the QBF formula is true using game-tree search. + /// + /// This implements a recursive minimax-style evaluation: + /// - For ∃ quantifiers: true if ANY assignment to the variable leads to true + /// - For ∀ quantifiers: true if ALL assignments to the variable lead to true + /// + /// Runtime is O(2^n) in the worst case. + pub fn is_true(&self) -> bool { + let mut assignment = vec![false; self.num_vars]; + self.evaluate_recursive(&mut assignment, 0) + } + + /// Recursive QBF evaluation. + fn evaluate_recursive(&self, assignment: &mut Vec, var_idx: usize) -> bool { + if var_idx == self.num_vars { + // All variables assigned — evaluate the CNF matrix + return self.clauses.iter().all(|c| c.is_satisfied(assignment)); + } + + match self.quantifiers[var_idx] { + Quantifier::Exists => { + // Try both values; true if either works + assignment[var_idx] = false; + if self.evaluate_recursive(assignment, var_idx + 1) { + return true; + } + assignment[var_idx] = true; + self.evaluate_recursive(assignment, var_idx + 1) + } + Quantifier::ForAll => { + // Try both values; true only if both work + assignment[var_idx] = false; + if !self.evaluate_recursive(assignment, var_idx + 1) { + return false; + } + assignment[var_idx] = true; + self.evaluate_recursive(assignment, var_idx + 1) + } + } + } + +} + +impl Problem for QuantifiedBooleanFormulas { + const NAME: &'static str = "QuantifiedBooleanFormulas"; + type Metric = bool; + + fn dims(&self) -> Vec { + vec![] + } + + fn evaluate(&self, config: &[usize]) -> bool { + if !config.is_empty() { + return false; + } + self.is_true() + } + + fn variant() -> Vec<(&'static str, &'static str)> { + crate::variant_params![] + } +} + +impl SatisfactionProblem for QuantifiedBooleanFormulas {} + +crate::declare_variants! { + default sat QuantifiedBooleanFormulas => "2^num_vars", +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_model_example_specs() -> Vec { + vec![crate::example_db::specs::ModelExampleSpec { + id: "quantified_boolean_formulas", + instance: Box::new(QuantifiedBooleanFormulas::new( + 2, + vec![Quantifier::Exists, Quantifier::ForAll], + vec![ + CNFClause::new(vec![1, 2]), // u_1 OR u_2 + CNFClause::new(vec![1, -2]), // u_1 OR NOT u_2 + ], + )), + optimal_config: vec![], + optimal_value: serde_json::json!(true), + }] +} + +#[cfg(test)] +#[path = "../../unit_tests/models/formula/qbf.rs"] +mod tests; diff --git a/src/models/mod.rs b/src/models/mod.rs index 0d0086584..a3eb9ef14 100644 --- a/src/models/mod.rs +++ b/src/models/mod.rs @@ -13,7 +13,9 @@ pub use algebraic::{ ClosestVectorProblem, ConsecutiveBlockMinimization, ConsecutiveOnesSubmatrix, QuadraticAssignment, BMF, ILP, QUBO, }; -pub use formula::{CNFClause, CircuitSAT, KSatisfiability, Satisfiability}; +pub use formula::{ + CNFClause, CircuitSAT, KSatisfiability, QuantifiedBooleanFormulas, Quantifier, Satisfiability, +}; pub use graph::{ BalancedCompleteBipartiteSubgraph, BicliqueCover, BiconnectivityAugmentation, BoundedComponentSpanningForest, DirectedTwoCommodityIntegralFlow, GeneralizedHex, diff --git a/src/unit_tests/models/formula/qbf.rs b/src/unit_tests/models/formula/qbf.rs new file mode 100644 index 000000000..be46c741f --- /dev/null +++ b/src/unit_tests/models/formula/qbf.rs @@ -0,0 +1,264 @@ +use super::*; +use crate::solvers::{BruteForce, Solver}; +use crate::traits::Problem; + +#[test] +fn test_quantifier_creation() { + let q1 = Quantifier::Exists; + let q2 = Quantifier::ForAll; + assert_eq!(q1, Quantifier::Exists); + assert_eq!(q2, Quantifier::ForAll); + assert_ne!(q1, q2); +} + +#[test] +fn test_qbf_creation() { + let problem = QuantifiedBooleanFormulas::new( + 3, + vec![Quantifier::Exists, Quantifier::ForAll, Quantifier::Exists], + vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, 3])], + ); + assert_eq!(problem.num_vars(), 3); + assert_eq!(problem.num_clauses(), 2); + assert_eq!(problem.num_variables(), 0); + assert_eq!(problem.quantifiers().len(), 3); + assert_eq!(problem.clauses().len(), 2); +} + +#[test] +#[should_panic(expected = "quantifiers length")] +fn test_qbf_creation_mismatch() { + QuantifiedBooleanFormulas::new( + 3, + vec![Quantifier::Exists, Quantifier::ForAll], // Only 2, need 3 + vec![], + ); +} + +#[test] +fn test_qbf_evaluate_true() { + // F = ∃u_1 ∀u_2 (u_1 ∨ u_2) ∧ (u_1 ∨ ¬u_2) + // Setting u_1=T satisfies both clauses regardless of u_2 + let problem = QuantifiedBooleanFormulas::new( + 2, + vec![Quantifier::Exists, Quantifier::ForAll], + vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![1, -2])], + ); + + // dims() is empty; evaluate([]) runs the game-tree search + assert_eq!(problem.dims(), Vec::::new()); + assert!(problem.evaluate(&[])); + assert!(problem.is_true()); +} + +#[test] +fn test_qbf_evaluate_false() { + // F = ∀u_1 ∃u_2 (u_1) ∧ (¬u_1) + // Always false: no assignment can satisfy both u_1 and NOT u_1 + let problem = QuantifiedBooleanFormulas::new( + 2, + vec![Quantifier::ForAll, Quantifier::Exists], + vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])], + ); + + assert!(!problem.evaluate(&[])); + assert!(!problem.is_true()); +} + +#[test] +fn test_qbf_evaluate_nonempty_config_returns_false() { + // Non-empty config is always false (no external variables) + let problem = QuantifiedBooleanFormulas::new( + 2, + vec![Quantifier::Exists, Quantifier::ForAll], + vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![1, -2])], + ); + assert!(!problem.evaluate(&[1, 0])); +} + +#[test] +fn test_qbf_is_true_all_exists() { + // When all quantifiers are Exists, QBF reduces to SAT + // F = ∃u_1 ∃u_2 (u_1 ∨ u_2) ∧ (¬u_1 ∨ ¬u_2) + let problem = QuantifiedBooleanFormulas::new( + 2, + vec![Quantifier::Exists, Quantifier::Exists], + vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![-1, -2])], + ); + // Satisfiable: u_1=T,u_2=F or u_1=F,u_2=T + assert!(problem.is_true()); +} + +#[test] +fn test_qbf_is_true_all_forall() { + // F = ∀u_1 ∀u_2 (u_1 ∨ u_2) + // False: u_1=F, u_2=F fails the clause + let problem = QuantifiedBooleanFormulas::new( + 2, + vec![Quantifier::ForAll, Quantifier::ForAll], + vec![CNFClause::new(vec![1, 2])], + ); + assert!(!problem.is_true()); +} + +#[test] +fn test_qbf_is_true_all_forall_tautology() { + // F = ∀u_1 (u_1 ∨ ¬u_1) + // Always true (tautology) + let problem = QuantifiedBooleanFormulas::new( + 1, + vec![Quantifier::ForAll], + vec![CNFClause::new(vec![1, -1])], + ); + assert!(problem.is_true()); +} + +#[test] +fn test_qbf_empty_formula() { + // Empty CNF is trivially true + let problem = + QuantifiedBooleanFormulas::new(2, vec![Quantifier::Exists, Quantifier::ForAll], vec![]); + assert!(problem.evaluate(&[])); + assert!(problem.is_true()); +} + +#[test] +fn test_qbf_zero_vars() { + // Zero variables, empty clauses + let problem = QuantifiedBooleanFormulas::new(0, vec![], vec![]); + assert!(problem.evaluate(&[])); + assert!(problem.is_true()); + assert_eq!(problem.dims(), Vec::::new()); +} + +#[test] +fn test_qbf_zero_vars_unsat() { + // Zero variables, but a clause that refers to var 1 (unsatisfiable) + let problem = QuantifiedBooleanFormulas::new(0, vec![], vec![CNFClause::new(vec![1])]); + assert!(!problem.evaluate(&[])); + assert!(!problem.is_true()); +} + +#[test] +fn test_qbf_solver() { + // F = ∃u_1 ∀u_2 (u_1 ∨ u_2) ∧ (u_1 ∨ ¬u_2) — TRUE + let problem = QuantifiedBooleanFormulas::new( + 2, + vec![Quantifier::Exists, Quantifier::ForAll], + vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![1, -2])], + ); + + let solver = BruteForce::new(); + // With dims()=[], there is exactly one config: []. evaluate([]) = is_true() = true + let solution = solver.find_satisfying(&problem); + assert!(solution.is_some()); + let sol = solution.unwrap(); + assert_eq!(sol, Vec::::new()); + assert!(problem.evaluate(&sol)); +} + +#[test] +fn test_qbf_solver_false() { + // F = ∀u_1 ∃u_2 (u_1) ∧ (¬u_1) — FALSE + let problem = QuantifiedBooleanFormulas::new( + 2, + vec![Quantifier::ForAll, Quantifier::Exists], + vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])], + ); + + let solver = BruteForce::new(); + let solution = solver.find_satisfying(&problem); + assert!(solution.is_none()); +} + +#[test] +fn test_qbf_solver_all_satisfying() { + // F = ∃u_1 ∀u_2 (u_1 ∨ u_2) ∧ (u_1 ∨ ¬u_2) — TRUE + let problem = QuantifiedBooleanFormulas::new( + 2, + vec![Quantifier::Exists, Quantifier::ForAll], + vec![CNFClause::new(vec![1, 2]), CNFClause::new(vec![1, -2])], + ); + + let solver = BruteForce::new(); + let solutions = solver.find_all_satisfying(&problem); + // Only one config exists (the empty config []), and it satisfies + assert_eq!(solutions.len(), 1); + assert_eq!(solutions[0], Vec::::new()); +} + +#[test] +fn test_qbf_serialization() { + let problem = QuantifiedBooleanFormulas::new( + 2, + vec![Quantifier::Exists, Quantifier::ForAll], + vec![CNFClause::new(vec![1, -2])], + ); + + let json = serde_json::to_string(&problem).unwrap(); + let deserialized: QuantifiedBooleanFormulas = serde_json::from_str(&json).unwrap(); + + assert_eq!(deserialized.num_vars(), problem.num_vars()); + assert_eq!(deserialized.num_clauses(), problem.num_clauses()); + assert_eq!(deserialized.quantifiers(), problem.quantifiers()); + assert_eq!(deserialized.dims(), problem.dims()); +} + +#[test] +fn test_qbf_three_vars() { + // F = ∃u_1 ∀u_2 ∃u_3 (u_1 ∨ u_2 ∨ u_3) ∧ (¬u_1 ∨ ¬u_2 ∨ u_3) + // Strategy: set u_1=T. Then for any u_2: + // Clause 1 is satisfied (u_1=T). + // Set u_3=T: Clause 2 = (F ∨ ¬u_2 ∨ T) = T. + // So this is true. + let problem = QuantifiedBooleanFormulas::new( + 3, + vec![Quantifier::Exists, Quantifier::ForAll, Quantifier::Exists], + vec![ + CNFClause::new(vec![1, 2, 3]), + CNFClause::new(vec![-1, -2, 3]), + ], + ); + assert!(problem.is_true()); +} + +#[test] +fn test_qbf_dims() { + let problem = QuantifiedBooleanFormulas::new( + 4, + vec![ + Quantifier::Exists, + Quantifier::ForAll, + Quantifier::Exists, + Quantifier::ForAll, + ], + vec![CNFClause::new(vec![1, 2, 3, 4])], + ); + // dims() is always empty — QBF has no external config variables + assert_eq!(problem.dims(), Vec::::new()); +} + +#[test] +fn test_qbf_variant() { + assert_eq!(QuantifiedBooleanFormulas::variant(), vec![]); +} + +#[test] +fn test_qbf_quantifier_clone() { + let q = Quantifier::Exists; + let q2 = q; + assert_eq!(q, q2); + let q3 = Quantifier::ForAll; + assert_ne!(q, q3); +} + +#[test] +fn test_qbf_empty_clause() { + // An empty clause (disjunction of zero literals) is always false + let problem = QuantifiedBooleanFormulas::new( + 1, + vec![Quantifier::Exists], + vec![CNFClause::new(vec![])], + ); + assert!(!problem.is_true()); +}