From c3b0b19abc63fe2030979fb43b3e4a5a31c99fb9 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Tue, 17 Mar 2026 09:48:19 +0800 Subject: [PATCH 1/8] Add plan for #449: [Model] ConjunctiveBooleanQuery --- .../2026-03-17-conjunctive-boolean-query.md | 167 ++++++++++++++++++ 1 file changed, 167 insertions(+) create mode 100644 docs/plans/2026-03-17-conjunctive-boolean-query.md diff --git a/docs/plans/2026-03-17-conjunctive-boolean-query.md b/docs/plans/2026-03-17-conjunctive-boolean-query.md new file mode 100644 index 000000000..0b5cae988 --- /dev/null +++ b/docs/plans/2026-03-17-conjunctive-boolean-query.md @@ -0,0 +1,167 @@ +# Plan: [Model] ConjunctiveBooleanQuery (#449) + +## Overview + +Add the **Conjunctive Boolean Query** (CBQ) problem model — a satisfaction problem from database theory (Garey & Johnson A4 SR31). Given a finite domain D, a collection of relations R, and an existentially quantified conjunctive query Q, determine whether Q is true over R and D. + +This is equivalent to the Constraint Satisfaction Problem (CSP) and the Graph Homomorphism problem. NP-complete via reduction from CLIQUE (Chandra & Merlin, 1977). + +**Category:** `misc/` (unique input structure: domain + relations + conjunctive query) + +## Information Checklist + +| # | Item | Value | +|---|------|-------| +| 1 | Problem name | `ConjunctiveBooleanQuery` | +| 2 | Mathematical definition | INSTANCE: Finite domain D, relations R={R_1,...,R_m}, conjunctive query Q = (∃y_1,...,y_l)(A_1 ∧ ... ∧ A_r). QUESTION: Is Q true? | +| 3 | Problem type | Satisfaction (`Metric = bool`) | +| 4 | Type parameters | None | +| 5 | Struct fields | `domain_size: usize`, `relations: Vec`, `num_variables: usize`, `conjuncts: Vec<(usize, Vec)>` | +| 6 | Configuration space | `vec![domain_size; num_variables]` — l variables each over domain D | +| 7 | Feasibility check | For each conjunct (rel_idx, args), substitute variables from config and check tuple membership in the relation | +| 8 | Objective function | N/A (satisfaction) | +| 9 | Best known exact | Brute-force O(|D|^l * r * max_arity). No substantially faster general algorithm known. | +| 10 | Solving strategy | BruteForce (enumerate all |D|^l assignments) | +| 11 | Category | `misc` | +| 12 | Expected outcome | Example: D={0..5}, 2 relations (binary+ternary), query with 2 variables, 3 conjuncts → TRUE, satisfying assignment y_1=0, y_2=1 | + +## Batch 1: Implementation (Steps 1-5.5) + +### Task 1.1: Create model file `src/models/misc/conjunctive_boolean_query.rs` + +Define companion types and the main struct: + +```rust +/// A relation with fixed arity and a set of tuples. +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct Relation { + pub arity: usize, + pub tuples: Vec>, +} + +/// An argument in a conjunctive query: either a bound variable or a domain constant. +#[derive(Debug, Clone, Serialize, Deserialize)] +pub enum QueryArg { + Variable(usize), + Constant(usize), +} + +/// The Conjunctive Boolean Query problem. +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct ConjunctiveBooleanQuery { + domain_size: usize, + relations: Vec, + num_variables: usize, + conjuncts: Vec<(usize, Vec)>, +} +``` + +**Constructor:** `new(domain_size, relations, num_variables, conjuncts)` with validation: +- All relation tuples have correct arity +- All tuple entries < domain_size +- All conjunct relation indices are valid +- All conjunct args reference valid variable indices or constants < domain_size +- Conjunct argument count matches relation arity + +**Getter methods:** `domain_size()`, `num_relations()`, `num_variables()`, `num_conjuncts()`, `relations()`, `conjuncts()` + +**Problem trait impl:** +- `NAME = "ConjunctiveBooleanQuery"` +- `type Metric = bool` +- `variant() -> crate::variant_params![]` +- `dims() -> vec![self.domain_size; self.num_variables]` +- `evaluate(config)`: for each conjunct, resolve args (Variable → config[idx], Constant → value), check if resulting tuple is in the relation + +**SatisfactionProblem impl:** marker trait + +**`declare_variants!`:** +```rust +crate::declare_variants! { + default sat ConjunctiveBooleanQuery => "domain_size ^ num_variables", +} +``` + +**ProblemSchemaEntry:** +```rust +inventory::submit! { + ProblemSchemaEntry { + name: "ConjunctiveBooleanQuery", + display_name: "Conjunctive Boolean Query", + aliases: &["CBQ"], + dimensions: &[], + module_path: module_path!(), + description: "Evaluate a conjunctive Boolean query over a relational database", + fields: &[ + FieldInfo { name: "domain_size", type_name: "usize", description: "Size of the finite domain D" }, + FieldInfo { name: "relations", type_name: "Vec", description: "Collection of relations R" }, + FieldInfo { name: "num_variables", type_name: "usize", description: "Number of existentially quantified variables" }, + FieldInfo { name: "conjuncts", type_name: "Vec<(usize, Vec)>", description: "Query conjuncts: (relation_index, arguments)" }, + ], + } +} +``` + +### Task 1.2: Register in module tree + +1. **`src/models/misc/mod.rs`:** Add `mod conjunctive_boolean_query;` and `pub use conjunctive_boolean_query::{ConjunctiveBooleanQuery, Relation as CbqRelation, QueryArg};` +2. **`src/models/mod.rs`:** Add to misc re-exports +3. **`src/lib.rs`/prelude:** Add ConjunctiveBooleanQuery to prelude if needed + +### Task 1.3: CLI registration + +1. **`problemreductions-cli/src/problem_name.rs`:** Add alias `"cbq" => "ConjunctiveBooleanQuery"` (CBQ is not a well-established abbreviation, so only add lowercase pass-through; the `aliases` in ProblemSchemaEntry handles `CBQ`) +2. **`problemreductions-cli/src/commands/create.rs`:** + - Add CLI flags to `CreateArgs` in `cli.rs`: `--domain-size`, `--relations`, `--conjuncts` + - Add match arm for `"ConjunctiveBooleanQuery"` that parses these flags + - Add to `help_data_flags()` table + - Update `all_data_flags_empty()` if new flags added +3. **`problemreductions-cli/src/cli.rs`:** Add the new flag fields + +### Task 1.4: Add canonical model example to example_db + +Add `canonical_model_example_specs()` to the model file (feature-gated with `example-db`): + +Use the issue's example instance: +- D = {0,...,5}, R_1 (arity 2): {(0,3),(1,3),(2,4),(3,4),(4,5)}, R_2 (arity 3): {(0,1,5),(1,2,5),(2,3,4),(0,4,3)} +- Query: (∃y_1,y_2)(R_1(y_1,3) ∧ R_1(y_2,3) ∧ R_2(y_1,y_2,5)) +- But keep it small enough for brute force (6^2 = 36 configs — fine) + +Register in `src/models/misc/mod.rs`'s `canonical_model_example_specs()`. + +### Task 1.5: Write unit tests `src/unit_tests/models/misc/conjunctive_boolean_query.rs` + +Required tests (≥3): +- `test_conjunctivebooleanquery_basic` — create instance, verify dims, getters, NAME +- `test_conjunctivebooleanquery_evaluate_yes` — verify satisfying assignment y_1=0, y_2=1 +- `test_conjunctivebooleanquery_evaluate_no` — verify non-satisfying assignment +- `test_conjunctivebooleanquery_out_of_range` — variable value ≥ domain_size returns false +- `test_conjunctivebooleanquery_brute_force` — BruteForce finds satisfying assignment +- `test_conjunctivebooleanquery_unsatisfiable` — instance with no solution +- `test_conjunctivebooleanquery_serialization` — round-trip serde JSON +- `test_conjunctivebooleanquery_paper_example` — same instance as paper, verify expected solution and count + +Link test file via `#[cfg(test)] #[path = "../../unit_tests/models/misc/conjunctive_boolean_query.rs"] mod tests;` + +### Task 1.6: Verify build and tests + +```bash +make check # fmt + clippy + test +``` + +## Batch 2: Paper Entry (Step 6) + +### Task 2.1: Write paper entry in `docs/paper/reductions.typ` + +1. Add to `display-name` dict: `"ConjunctiveBooleanQuery": [Conjunctive Boolean Query]` +2. Add `#problem-def("ConjunctiveBooleanQuery")[definition][body]` with: + - Formal definition: domain D, relations R, conjunctive query Q + - Background: classical in database theory, equivalent to CSP and graph homomorphism + - Best known algorithm: brute-force O(|D|^l), cite Chandra & Merlin 1977 + - Example with CeTZ visualization: show the relations as tables, the query structure, and the satisfying assignment + - Evaluation: verify the three conjuncts on (y_1=0, y_2=1) +3. Build: `make paper` + +## Dependencies + +- Batch 2 depends on Batch 1 (needs exports from compiled code) +- No external model dependencies (this is a standalone model) From e51c98462145a5a1e5e99dce7ca22b2c9e079e97 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Tue, 17 Mar 2026 10:11:39 +0800 Subject: [PATCH 2/8] Implement ConjunctiveBooleanQuery model (#449) Co-Authored-By: Claude Opus 4.6 --- problemreductions-cli/src/cli.rs | 10 + problemreductions-cli/src/commands/create.rs | 105 ++++++- src/lib.rs | 6 +- src/models/misc/conjunctive_boolean_query.rs | 265 ++++++++++++++++++ src/models/misc/mod.rs | 4 + src/models/mod.rs | 6 +- .../models/misc/conjunctive_boolean_query.rs | 140 +++++++++ 7 files changed, 528 insertions(+), 8 deletions(-) create mode 100644 src/models/misc/conjunctive_boolean_query.rs create mode 100644 src/unit_tests/models/misc/conjunctive_boolean_query.rs diff --git a/problemreductions-cli/src/cli.rs b/problemreductions-cli/src/cli.rs index e71a9e426..2739958e2 100644 --- a/problemreductions-cli/src/cli.rs +++ b/problemreductions-cli/src/cli.rs @@ -251,6 +251,7 @@ Flags by problem type: MinimumTardinessSequencing --n, --deadlines [--precedence-pairs] SCS --strings, --bound [--alphabet-size] D2CIF --arcs, --capacities, --source-1, --sink-1, --source-2, --sink-2, --requirement-1, --requirement-2 + CBQ --domain-size, --relations, --conjuncts-spec ILP, CircuitSAT (via reduction only) Geometry graph variants (use slash notation, e.g., MIS/KingsSubgraph): @@ -456,6 +457,15 @@ pub struct CreateArgs { /// Alphabet size for SCS (optional; inferred from max symbol + 1 if omitted) #[arg(long)] pub alphabet_size: Option, + /// Domain size for ConjunctiveBooleanQuery + #[arg(long)] + pub domain_size: Option, + /// Relations for ConjunctiveBooleanQuery (format: "arity:tuple1|tuple2;arity:tuple1|tuple2") + #[arg(long)] + pub relations: Option, + /// Conjuncts for ConjunctiveBooleanQuery (format: "rel:args;rel:args" where args use v0,v1 for variables, c0,c1 for constants) + #[arg(long)] + pub conjuncts_spec: Option, } #[derive(clap::Args)] diff --git a/problemreductions-cli/src/commands/create.rs b/problemreductions-cli/src/commands/create.rs index 03220f4f6..61286c277 100644 --- a/problemreductions-cli/src/commands/create.rs +++ b/problemreductions-cli/src/commands/create.rs @@ -13,8 +13,9 @@ use problemreductions::models::graph::{ SteinerTree, }; use problemreductions::models::misc::{ - BinPacking, FlowShopScheduling, LongestCommonSubsequence, MinimumTardinessSequencing, - PaintShop, SequencingWithinIntervals, ShortestCommonSupersequence, SubsetSum, + BinPacking, CbqRelation, ConjunctiveBooleanQuery, FlowShopScheduling, LongestCommonSubsequence, + MinimumTardinessSequencing, PaintShop, QueryArg, SequencingWithinIntervals, + ShortestCommonSupersequence, SubsetSum, }; use problemreductions::prelude::*; use problemreductions::registry::collect_schemas; @@ -90,6 +91,9 @@ fn all_data_flags_empty(args: &CreateArgs) -> bool { && args.sink_2.is_none() && args.requirement_1.is_none() && args.requirement_2.is_none() + && args.domain_size.is_none() + && args.relations.is_none() + && args.conjuncts_spec.is_none() } fn emit_problem_output(output: &ProblemJsonOutput, out: &OutputConfig) -> Result<()> { @@ -296,6 +300,9 @@ fn example_for(canonical: &str, graph_type: Option<&str>) -> &'static str { "SubsetSum" => "--sizes 3,7,1,8,2,4 --target 11", "SetBasis" => "--universe 4 --sets \"0,1;1,2;0,2;0,1,2\" --k 3", "ShortestCommonSupersequence" => "--strings \"0,1,2;1,2,0\" --bound 4", + "ConjunctiveBooleanQuery" => { + "--domain-size 6 --relations \"2:0,3|1,3|2,4;3:0,1,5|1,2,5\" --conjuncts-spec \"0:v0,c3;0:v1,c3;1:v0,v1,c5\"" + } _ => "", } } @@ -1542,6 +1549,100 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> { ) } + // ConjunctiveBooleanQuery + "ConjunctiveBooleanQuery" => { + let usage = "Usage: pred create CBQ --domain-size 6 --relations \"2:0,3|1,3;3:0,1,5|1,2,5\" --conjuncts-spec \"0:v0,c3;0:v1,c3;1:v0,v1,c5\""; + let domain_size = args.domain_size.ok_or_else(|| { + anyhow::anyhow!("ConjunctiveBooleanQuery requires --domain-size\n\n{usage}") + })?; + let relations_str = args.relations.as_deref().ok_or_else(|| { + anyhow::anyhow!("ConjunctiveBooleanQuery requires --relations\n\n{usage}") + })?; + let conjuncts_str = args.conjuncts_spec.as_deref().ok_or_else(|| { + anyhow::anyhow!("ConjunctiveBooleanQuery requires --conjuncts-spec\n\n{usage}") + })?; + // Parse relations: "arity:t1,t2|t3,t4;arity:t5,t6,t7|t8,t9,t10" + let relations: Vec = relations_str + .split(';') + .map(|rel_str| { + let rel_str = rel_str.trim(); + let (arity_str, tuples_str) = rel_str.split_once(':').ok_or_else(|| { + anyhow::anyhow!( + "Invalid relation format: expected 'arity:tuples', got '{rel_str}'" + ) + })?; + let arity: usize = arity_str + .trim() + .parse() + .map_err(|e| anyhow::anyhow!("Invalid arity '{arity_str}': {e}"))?; + let tuples: Vec> = tuples_str + .split('|') + .map(|t| { + t.trim() + .split(',') + .map(|v| { + v.trim() + .parse::() + .map_err(|e| anyhow::anyhow!("Invalid tuple value: {e}")) + }) + .collect::>>() + }) + .collect::>>()?; + Ok(CbqRelation { arity, tuples }) + }) + .collect::>>()?; + // Parse conjuncts: "rel_idx:arg1,arg2;rel_idx:arg1,arg2,arg3" + let mut num_vars_inferred: usize = 0; + let conjuncts: Vec<(usize, Vec)> = conjuncts_str + .split(';') + .map(|conj_str| { + let conj_str = conj_str.trim(); + let (idx_str, args_str) = conj_str.split_once(':').ok_or_else(|| { + anyhow::anyhow!( + "Invalid conjunct format: expected 'rel_idx:args', got '{conj_str}'" + ) + })?; + let rel_idx: usize = idx_str.trim().parse().map_err(|e| { + anyhow::anyhow!("Invalid relation index '{idx_str}': {e}") + })?; + let query_args: Vec = args_str + .split(',') + .map(|a| { + let a = a.trim(); + if let Some(rest) = a.strip_prefix('v') { + let v: usize = rest.parse().map_err(|e| { + anyhow::anyhow!("Invalid variable index '{rest}': {e}") + })?; + if v + 1 > num_vars_inferred { + num_vars_inferred = v + 1; + } + Ok(QueryArg::Variable(v)) + } else if let Some(rest) = a.strip_prefix('c') { + let c: usize = rest.parse().map_err(|e| { + anyhow::anyhow!("Invalid constant value '{rest}': {e}") + })?; + Ok(QueryArg::Constant(c)) + } else { + Err(anyhow::anyhow!( + "Invalid query arg '{a}': expected vN (variable) or cN (constant)" + )) + } + }) + .collect::>>()?; + Ok((rel_idx, query_args)) + }) + .collect::>>()?; + ( + ser(ConjunctiveBooleanQuery::new( + domain_size, + relations, + num_vars_inferred, + conjuncts, + ))?, + resolved_variant.clone(), + ) + } + _ => bail!("{}", crate::problem_name::unknown_problem_error(canonical)), }; diff --git a/src/lib.rs b/src/lib.rs index 42bc6c927..b5f1e1272 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -57,9 +57,9 @@ pub mod prelude { UndirectedTwoCommodityIntegralFlow, }; pub use crate::models::misc::{ - BinPacking, Factoring, FlowShopScheduling, Knapsack, LongestCommonSubsequence, - MinimumTardinessSequencing, PaintShop, SequencingWithinIntervals, - ShortestCommonSupersequence, SubsetSum, + BinPacking, CbqRelation, ConjunctiveBooleanQuery, Factoring, FlowShopScheduling, Knapsack, + LongestCommonSubsequence, MinimumTardinessSequencing, PaintShop, QueryArg, + SequencingWithinIntervals, ShortestCommonSupersequence, SubsetSum, }; pub use crate::models::set::{ ExactCoverBy3Sets, MaximumSetPacking, MinimumSetCovering, SetBasis, diff --git a/src/models/misc/conjunctive_boolean_query.rs b/src/models/misc/conjunctive_boolean_query.rs new file mode 100644 index 000000000..4dd9fbe1d --- /dev/null +++ b/src/models/misc/conjunctive_boolean_query.rs @@ -0,0 +1,265 @@ +//! Conjunctive Boolean Query problem implementation. +//! +//! Given a finite domain `D = {0, ..., domain_size-1}`, a collection of +//! relations `R`, and a conjunctive Boolean query +//! `Q = (exists y_1, ..., y_l)(A_1 /\ ... /\ A_r)`, determine whether `Q` is +//! true over `R` and `D`. +//! +//! Each conjunct `A_i` applies a relation to a tuple of arguments, where each +//! argument is either an existentially quantified variable or a constant from +//! the domain. The query is satisfiable iff there exists an assignment to the +//! variables such that every conjunct's resolved tuple belongs to its relation. + +use crate::registry::{FieldInfo, ProblemSchemaEntry}; +use crate::traits::{Problem, SatisfactionProblem}; +use serde::{Deserialize, Serialize}; + +inventory::submit! { + ProblemSchemaEntry { + name: "ConjunctiveBooleanQuery", + display_name: "Conjunctive Boolean Query", + aliases: &["CBQ"], + dimensions: &[], + module_path: module_path!(), + description: "Evaluate a conjunctive Boolean query over a relational database", + fields: &[ + FieldInfo { name: "domain_size", type_name: "usize", description: "Size of the finite domain D" }, + FieldInfo { name: "relations", type_name: "Vec", description: "Collection of relations R" }, + FieldInfo { name: "num_variables", type_name: "usize", description: "Number of existentially quantified variables" }, + FieldInfo { name: "conjuncts", type_name: "Vec<(usize, Vec)>", description: "Query conjuncts: (relation_index, arguments)" }, + ], + } +} + +/// A relation with fixed arity and a set of tuples over a finite domain. +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct Relation { + /// The arity (number of columns) of this relation. + pub arity: usize, + /// The set of tuples; each tuple has length == arity, entries in `0..domain_size`. + pub tuples: Vec>, +} + +/// An argument in a conjunctive query atom. +#[derive(Debug, Clone, Serialize, Deserialize)] +pub enum QueryArg { + /// A reference to existential variable `y_i` (0-indexed). + Variable(usize), + /// A constant value from the domain `D`. + Constant(usize), +} + +/// The Conjunctive Boolean Query problem. +/// +/// Given a finite domain `D = {0, ..., domain_size-1}`, a collection of +/// relations `R`, and a conjunctive Boolean query +/// `Q = (exists y_1, ..., y_l)(A_1 /\ ... /\ A_r)`, determine whether `Q` is +/// true over `R` and `D`. +/// +/// # Representation +/// +/// The configuration is a vector of length `num_variables`, where each entry is +/// a value in `{0, ..., domain_size-1}` representing an assignment to the +/// existentially quantified variables. +/// +/// # Example +/// +/// ``` +/// use problemreductions::models::misc::{ConjunctiveBooleanQuery, CbqRelation, QueryArg}; +/// use problemreductions::{Problem, Solver, BruteForce}; +/// +/// let relations = vec![ +/// CbqRelation { arity: 2, tuples: vec![vec![0, 3], vec![1, 3]] }, +/// ]; +/// let conjuncts = vec![ +/// (0, vec![QueryArg::Variable(0), QueryArg::Constant(3)]), +/// ]; +/// let problem = ConjunctiveBooleanQuery::new(6, relations, 1, conjuncts); +/// let solver = BruteForce::new(); +/// let solution = solver.find_satisfying(&problem); +/// assert!(solution.is_some()); +/// ``` +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct ConjunctiveBooleanQuery { + domain_size: usize, + relations: Vec, + num_variables: usize, + conjuncts: Vec<(usize, Vec)>, +} + +impl ConjunctiveBooleanQuery { + /// Create a new ConjunctiveBooleanQuery instance. + /// + /// # Panics + /// + /// Panics if: + /// - Any relation's tuples have incorrect arity + /// - Any tuple entry is >= domain_size + /// - Any conjunct references a non-existent relation + /// - Any `Variable(i)` has `i >= num_variables` + /// - Any `Constant(c)` has `c >= domain_size` + /// - Any conjunct's argument count does not match the referenced relation's arity + pub fn new( + domain_size: usize, + relations: Vec, + num_variables: usize, + conjuncts: Vec<(usize, Vec)>, + ) -> Self { + for (i, rel) in relations.iter().enumerate() { + for (j, tuple) in rel.tuples.iter().enumerate() { + assert!( + tuple.len() == rel.arity, + "Relation {i}: tuple {j} has length {}, expected arity {}", + tuple.len(), + rel.arity + ); + for (k, &val) in tuple.iter().enumerate() { + assert!( + val < domain_size, + "Relation {i}: tuple {j}, entry {k} is {val}, must be < {domain_size}" + ); + } + } + } + for (i, (rel_idx, args)) in conjuncts.iter().enumerate() { + assert!( + *rel_idx < relations.len(), + "Conjunct {i}: relation index {rel_idx} out of range (have {} relations)", + relations.len() + ); + assert!( + args.len() == relations[*rel_idx].arity, + "Conjunct {i}: has {} args, expected arity {}", + args.len(), + relations[*rel_idx].arity + ); + for (k, arg) in args.iter().enumerate() { + match arg { + QueryArg::Variable(v) => { + assert!( + *v < num_variables, + "Conjunct {i}, arg {k}: Variable({v}) >= num_variables ({num_variables})" + ); + } + QueryArg::Constant(c) => { + assert!( + *c < domain_size, + "Conjunct {i}, arg {k}: Constant({c}) >= domain_size ({domain_size})" + ); + } + } + } + } + Self { + domain_size, + relations, + num_variables, + conjuncts, + } + } + + /// Returns the size of the finite domain. + pub fn domain_size(&self) -> usize { + self.domain_size + } + + /// Returns the number of relations. + pub fn num_relations(&self) -> usize { + self.relations.len() + } + + /// Returns the number of existentially quantified variables. + pub fn num_variables(&self) -> usize { + self.num_variables + } + + /// Returns the number of conjuncts in the query. + pub fn num_conjuncts(&self) -> usize { + self.conjuncts.len() + } + + /// Returns the relations. + pub fn relations(&self) -> &[Relation] { + &self.relations + } + + /// Returns the conjuncts. + pub fn conjuncts(&self) -> &[(usize, Vec)] { + &self.conjuncts + } +} + +impl Problem for ConjunctiveBooleanQuery { + const NAME: &'static str = "ConjunctiveBooleanQuery"; + type Metric = bool; + + fn variant() -> Vec<(&'static str, &'static str)> { + crate::variant_params![] + } + + fn dims(&self) -> Vec { + vec![self.domain_size; self.num_variables] + } + + fn evaluate(&self, config: &[usize]) -> bool { + if config.len() != self.num_variables { + return false; + } + if config.iter().any(|&v| v >= self.domain_size) { + return false; + } + self.conjuncts.iter().all(|(rel_idx, args)| { + let tuple: Vec = args + .iter() + .map(|arg| match arg { + QueryArg::Variable(i) => config[*i], + QueryArg::Constant(c) => *c, + }) + .collect(); + self.relations[*rel_idx].tuples.contains(&tuple) + }) + } +} + +impl SatisfactionProblem for ConjunctiveBooleanQuery {} + +crate::declare_variants! { + default sat ConjunctiveBooleanQuery => "domain_size ^ num_variables", +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_model_example_specs() -> Vec { + vec![crate::example_db::specs::ModelExampleSpec { + id: "conjunctive_boolean_query", + build: || { + let relations = vec![ + Relation { + arity: 2, + tuples: vec![vec![0, 3], vec![1, 3], vec![2, 4], vec![3, 4], vec![4, 5]], + }, + Relation { + arity: 3, + tuples: vec![vec![0, 1, 5], vec![1, 2, 5], vec![2, 3, 4], vec![0, 4, 3]], + }, + ]; + let conjuncts = vec![ + (0, vec![QueryArg::Variable(0), QueryArg::Constant(3)]), + (0, vec![QueryArg::Variable(1), QueryArg::Constant(3)]), + ( + 1, + vec![ + QueryArg::Variable(0), + QueryArg::Variable(1), + QueryArg::Constant(5), + ], + ), + ]; + let problem = ConjunctiveBooleanQuery::new(6, relations, 2, conjuncts); + crate::example_db::specs::satisfaction_example(problem, vec![vec![0, 1]]) + }, + }] +} + +#[cfg(test)] +#[path = "../../unit_tests/models/misc/conjunctive_boolean_query.rs"] +mod tests; diff --git a/src/models/misc/mod.rs b/src/models/misc/mod.rs index c4b125274..4ea196287 100644 --- a/src/models/misc/mod.rs +++ b/src/models/misc/mod.rs @@ -2,6 +2,7 @@ //! //! Problems with unique input structures that don't fit other categories: //! - [`BinPacking`]: Bin Packing (minimize bins) +//! - [`ConjunctiveBooleanQuery`]: Evaluate a conjunctive Boolean query over relations //! - [`Factoring`]: Integer factorization //! - [`FlowShopScheduling`]: Flow Shop Scheduling (meet deadline on m processors) //! - [`Knapsack`]: 0-1 Knapsack (maximize value subject to weight capacity) @@ -13,6 +14,7 @@ //! - [`SubsetSum`]: Find a subset summing to exactly a target value mod bin_packing; +pub(crate) mod conjunctive_boolean_query; pub(crate) mod factoring; mod flow_shop_scheduling; mod knapsack; @@ -24,6 +26,7 @@ pub(crate) mod shortest_common_supersequence; mod subset_sum; pub use bin_packing::BinPacking; +pub use conjunctive_boolean_query::{ConjunctiveBooleanQuery, QueryArg, Relation as CbqRelation}; pub use factoring::Factoring; pub use flow_shop_scheduling::FlowShopScheduling; pub use knapsack::Knapsack; @@ -37,6 +40,7 @@ pub use subset_sum::SubsetSum; #[cfg(feature = "example-db")] pub(crate) fn canonical_model_example_specs() -> Vec { let mut specs = Vec::new(); + specs.extend(conjunctive_boolean_query::canonical_model_example_specs()); specs.extend(factoring::canonical_model_example_specs()); specs.extend(paintshop::canonical_model_example_specs()); specs.extend(sequencing_within_intervals::canonical_model_example_specs()); diff --git a/src/models/mod.rs b/src/models/mod.rs index 072034f02..281abd6f8 100644 --- a/src/models/mod.rs +++ b/src/models/mod.rs @@ -21,8 +21,8 @@ pub use graph::{ TravelingSalesman, UndirectedTwoCommodityIntegralFlow, }; pub use misc::{ - BinPacking, Factoring, FlowShopScheduling, Knapsack, LongestCommonSubsequence, - MinimumTardinessSequencing, PaintShop, SequencingWithinIntervals, ShortestCommonSupersequence, - SubsetSum, + BinPacking, CbqRelation, ConjunctiveBooleanQuery, Factoring, FlowShopScheduling, Knapsack, + LongestCommonSubsequence, MinimumTardinessSequencing, PaintShop, QueryArg, + SequencingWithinIntervals, ShortestCommonSupersequence, SubsetSum, }; pub use set::{ExactCoverBy3Sets, MaximumSetPacking, MinimumSetCovering, SetBasis}; diff --git a/src/unit_tests/models/misc/conjunctive_boolean_query.rs b/src/unit_tests/models/misc/conjunctive_boolean_query.rs new file mode 100644 index 000000000..4bc53fda0 --- /dev/null +++ b/src/unit_tests/models/misc/conjunctive_boolean_query.rs @@ -0,0 +1,140 @@ +use super::*; +use crate::solvers::{BruteForce, Solver}; +use crate::traits::Problem; + +/// Helper to build the issue example instance. +fn issue_example() -> ConjunctiveBooleanQuery { + let relations = vec![ + Relation { + arity: 2, + tuples: vec![vec![0, 3], vec![1, 3], vec![2, 4], vec![3, 4], vec![4, 5]], + }, + Relation { + arity: 3, + tuples: vec![vec![0, 1, 5], vec![1, 2, 5], vec![2, 3, 4], vec![0, 4, 3]], + }, + ]; + let conjuncts = vec![ + (0, vec![QueryArg::Variable(0), QueryArg::Constant(3)]), + (0, vec![QueryArg::Variable(1), QueryArg::Constant(3)]), + ( + 1, + vec![ + QueryArg::Variable(0), + QueryArg::Variable(1), + QueryArg::Constant(5), + ], + ), + ]; + ConjunctiveBooleanQuery::new(6, relations, 2, conjuncts) +} + +#[test] +fn test_conjunctivebooleanquery_basic() { + let problem = issue_example(); + assert_eq!(problem.domain_size(), 6); + assert_eq!(problem.num_relations(), 2); + assert_eq!(problem.num_variables(), 2); + assert_eq!(problem.num_conjuncts(), 3); + assert_eq!(problem.dims(), vec![6, 6]); + assert_eq!( + ::NAME, + "ConjunctiveBooleanQuery" + ); + assert_eq!(::variant(), vec![]); + assert_eq!(problem.relations().len(), 2); + assert_eq!(problem.conjuncts().len(), 3); +} + +#[test] +fn test_conjunctivebooleanquery_evaluate_yes() { + let problem = issue_example(); + // y_0=0, y_1=1: + // conjunct 0: R_0(0, 3) = (0,3) in R_0 -> true + // conjunct 1: R_0(1, 3) = (1,3) in R_0 -> true + // conjunct 2: R_1(0, 1, 5) = (0,1,5) in R_1 -> true + assert!(problem.evaluate(&[0, 1])); +} + +#[test] +fn test_conjunctivebooleanquery_evaluate_no() { + let problem = issue_example(); + // y_0=2, y_1=1: + // conjunct 0: R_0(2, 3) = (2,3) NOT in R_0 (R_0 has (2,4) not (2,3)) + assert!(!problem.evaluate(&[2, 1])); +} + +#[test] +fn test_conjunctivebooleanquery_out_of_range() { + let problem = issue_example(); + // value 6 is out of range for domain_size=6 + assert!(!problem.evaluate(&[6, 0])); +} + +#[test] +fn test_conjunctivebooleanquery_wrong_length() { + let problem = issue_example(); + // too short + assert!(!problem.evaluate(&[0])); + // too long + assert!(!problem.evaluate(&[0, 1, 2])); +} + +#[test] +fn test_conjunctivebooleanquery_brute_force() { + let problem = issue_example(); + let solver = BruteForce::new(); + let solution = solver + .find_satisfying(&problem) + .expect("should find a solution"); + assert!(problem.evaluate(&solution)); +} + +#[test] +fn test_conjunctivebooleanquery_unsatisfiable() { + // domain {0,1}, R_0 = {(0,0)}, query: (exists y_0)(R_0(y_0, y_0) /\ R_0(y_0, c1)) + // First conjunct: (y_0, y_0) in R_0 => y_0=0 + // Second conjunct: (0, 1) in R_0 => false + let relations = vec![Relation { + arity: 2, + tuples: vec![vec![0, 0]], + }]; + let conjuncts = vec![ + (0, vec![QueryArg::Variable(0), QueryArg::Variable(0)]), + (0, vec![QueryArg::Variable(0), QueryArg::Constant(1)]), + ]; + let problem = ConjunctiveBooleanQuery::new(2, relations, 1, conjuncts); + let solver = BruteForce::new(); + assert!(solver.find_satisfying(&problem).is_none()); +} + +#[test] +fn test_conjunctivebooleanquery_serialization() { + let problem = issue_example(); + let json = serde_json::to_value(&problem).unwrap(); + let restored: ConjunctiveBooleanQuery = serde_json::from_value(json).unwrap(); + assert_eq!(restored.domain_size(), problem.domain_size()); + assert_eq!(restored.num_relations(), problem.num_relations()); + assert_eq!(restored.num_variables(), problem.num_variables()); + assert_eq!(restored.num_conjuncts(), problem.num_conjuncts()); +} + +#[test] +fn test_conjunctivebooleanquery_paper_example() { + // Same instance as the issue example — count all satisfying assignments + let problem = issue_example(); + let solver = BruteForce::new(); + let all = solver.find_all_satisfying(&problem); + // (0,1) satisfies; verify count manually: + // For each (y0, y1) in {0..5}x{0..5}: + // need R_0(y0, 3) and R_0(y1, 3) and R_1(y0, y1, 5) + // R_0(y0, 3): y0 in {0,1} (tuples (0,3) and (1,3)) + // R_0(y1, 3): y1 in {0,1} + // R_1(y0, y1, 5): need (y0, y1, 5) in R_1 + // (0,1,5) yes, (0,0,5) no, (1,0,5) no, (1,1,5) no + // Wait — R_1 = {(0,1,5),(1,2,5),(2,3,4),(0,4,3)} + // (0,1,5): yes. (1,2,5): y0=1,y1=2 but need R_0(2,3)=(2,3) not in R_0. + // So only (0,1) works given the R_0 constraint. + assert_eq!(all.len(), 1); + assert_eq!(all[0], vec![0, 1]); +} From c2c13bcc9864310eb6009668255119c52d90e2cb Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Tue, 17 Mar 2026 10:23:42 +0800 Subject: [PATCH 3/8] Regenerate example-db fixtures for CBQ model --- src/example_db/fixtures/examples.json | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/example_db/fixtures/examples.json b/src/example_db/fixtures/examples.json index 6e52883b2..6f6b27a50 100644 --- a/src/example_db/fixtures/examples.json +++ b/src/example_db/fixtures/examples.json @@ -5,6 +5,7 @@ {"problem":"BoundedComponentSpanningForest","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[1,2,null],[2,3,null],[3,4,null],[4,5,null],[5,6,null],[6,7,null],[0,7,null],[1,5,null],[2,6,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null]}},"max_components":3,"max_weight":6,"weights":[2,3,1,2,3,1,2,1]},"samples":[{"config":[0,0,1,1,1,2,2,0],"metric":true}],"optimal":[{"config":[0,0,0,1,1,1,2,2],"metric":true},{"config":[0,0,0,1,1,2,2,2],"metric":true},{"config":[0,0,0,2,2,1,1,1],"metric":true},{"config":[0,0,0,2,2,2,1,1],"metric":true},{"config":[0,0,1,1,1,0,2,2],"metric":true},{"config":[0,0,1,1,1,2,2,0],"metric":true},{"config":[0,0,1,1,1,2,2,2],"metric":true},{"config":[0,0,1,1,2,0,1,1],"metric":true},{"config":[0,0,1,1,2,1,1,0],"metric":true},{"config":[0,0,1,1,2,2,1,0],"metric":true},{"config":[0,0,1,1,2,2,1,1],"metric":true},{"config":[0,0,1,1,2,2,2,0],"metric":true},{"config":[0,0,1,2,2,0,1,1],"metric":true},{"config":[0,0,1,2,2,1,1,0],"metric":true},{"config":[0,0,1,2,2,1,1,1],"metric":true},{"config":[0,0,1,2,2,2,1,0],"metric":true},{"config":[0,0,1,2,2,2,1,1],"metric":true},{"config":[0,0,2,1,1,0,2,2],"metric":true},{"config":[0,0,2,1,1,1,2,0],"metric":true},{"config":[0,0,2,1,1,1,2,2],"metric":true},{"config":[0,0,2,1,1,2,2,0],"metric":true},{"config":[0,0,2,1,1,2,2,2],"metric":true},{"config":[0,0,2,2,1,0,2,2],"metric":true},{"config":[0,0,2,2,1,1,1,0],"metric":true},{"config":[0,0,2,2,1,1,2,0],"metric":true},{"config":[0,0,2,2,1,1,2,2],"metric":true},{"config":[0,0,2,2,1,2,2,0],"metric":true},{"config":[0,0,2,2,2,0,1,1],"metric":true},{"config":[0,0,2,2,2,1,1,0],"metric":true},{"config":[0,0,2,2,2,1,1,1],"metric":true},{"config":[0,1,0,2,2,1,0,0],"metric":true},{"config":[0,1,0,2,2,2,0,0],"metric":true},{"config":[0,1,1,1,2,0,0,0],"metric":true},{"config":[0,1,1,1,2,2,0,0],"metric":true},{"config":[0,1,1,1,2,2,2,0],"metric":true},{"config":[0,1,1,2,2,0,0,0],"metric":true},{"config":[0,1,1,2,2,1,0,0],"metric":true},{"config":[0,1,1,2,2,2,0,0],"metric":true},{"config":[0,1,1,2,2,2,1,0],"metric":true},{"config":[0,1,2,2,2,0,0,0],"metric":true},{"config":[0,1,2,2,2,1,0,0],"metric":true},{"config":[0,1,2,2,2,1,1,0],"metric":true},{"config":[0,2,0,1,1,1,0,0],"metric":true},{"config":[0,2,0,1,1,2,0,0],"metric":true},{"config":[0,2,1,1,1,0,0,0],"metric":true},{"config":[0,2,1,1,1,2,0,0],"metric":true},{"config":[0,2,1,1,1,2,2,0],"metric":true},{"config":[0,2,2,1,1,0,0,0],"metric":true},{"config":[0,2,2,1,1,1,0,0],"metric":true},{"config":[0,2,2,1,1,1,2,0],"metric":true},{"config":[0,2,2,1,1,2,0,0],"metric":true},{"config":[0,2,2,2,1,0,0,0],"metric":true},{"config":[0,2,2,2,1,1,0,0],"metric":true},{"config":[0,2,2,2,1,1,1,0],"metric":true},{"config":[1,0,0,0,2,1,1,1],"metric":true},{"config":[1,0,0,0,2,2,1,1],"metric":true},{"config":[1,0,0,0,2,2,2,1],"metric":true},{"config":[1,0,0,2,2,0,1,1],"metric":true},{"config":[1,0,0,2,2,1,1,1],"metric":true},{"config":[1,0,0,2,2,2,0,1],"metric":true},{"config":[1,0,0,2,2,2,1,1],"metric":true},{"config":[1,0,1,2,2,0,1,1],"metric":true},{"config":[1,0,1,2,2,2,1,1],"metric":true},{"config":[1,0,2,2,2,0,0,1],"metric":true},{"config":[1,0,2,2,2,0,1,1],"metric":true},{"config":[1,0,2,2,2,1,1,1],"metric":true},{"config":[1,1,0,0,0,1,2,2],"metric":true},{"config":[1,1,0,0,0,2,2,1],"metric":true},{"config":[1,1,0,0,0,2,2,2],"metric":true},{"config":[1,1,0,0,2,0,0,1],"metric":true},{"config":[1,1,0,0,2,1,0,0],"metric":true},{"config":[1,1,0,0,2,2,0,0],"metric":true},{"config":[1,1,0,0,2,2,0,1],"metric":true},{"config":[1,1,0,0,2,2,2,1],"metric":true},{"config":[1,1,0,2,2,0,0,0],"metric":true},{"config":[1,1,0,2,2,0,0,1],"metric":true},{"config":[1,1,0,2,2,1,0,0],"metric":true},{"config":[1,1,0,2,2,2,0,0],"metric":true},{"config":[1,1,0,2,2,2,0,1],"metric":true},{"config":[1,1,1,0,0,0,2,2],"metric":true},{"config":[1,1,1,0,0,2,2,2],"metric":true},{"config":[1,1,1,2,2,0,0,0],"metric":true},{"config":[1,1,1,2,2,2,0,0],"metric":true},{"config":[1,1,2,0,0,0,2,1],"metric":true},{"config":[1,1,2,0,0,0,2,2],"metric":true},{"config":[1,1,2,0,0,1,2,2],"metric":true},{"config":[1,1,2,0,0,2,2,1],"metric":true},{"config":[1,1,2,0,0,2,2,2],"metric":true},{"config":[1,1,2,2,0,0,0,1],"metric":true},{"config":[1,1,2,2,0,0,2,1],"metric":true},{"config":[1,1,2,2,0,0,2,2],"metric":true},{"config":[1,1,2,2,0,1,2,2],"metric":true},{"config":[1,1,2,2,0,2,2,1],"metric":true},{"config":[1,1,2,2,2,0,0,0],"metric":true},{"config":[1,1,2,2,2,0,0,1],"metric":true},{"config":[1,1,2,2,2,1,0,0],"metric":true},{"config":[1,2,0,0,0,1,1,1],"metric":true},{"config":[1,2,0,0,0,2,1,1],"metric":true},{"config":[1,2,0,0,0,2,2,1],"metric":true},{"config":[1,2,1,0,0,0,1,1],"metric":true},{"config":[1,2,1,0,0,2,1,1],"metric":true},{"config":[1,2,2,0,0,0,1,1],"metric":true},{"config":[1,2,2,0,0,0,2,1],"metric":true},{"config":[1,2,2,0,0,1,1,1],"metric":true},{"config":[1,2,2,0,0,2,1,1],"metric":true},{"config":[1,2,2,2,0,0,0,1],"metric":true},{"config":[1,2,2,2,0,0,1,1],"metric":true},{"config":[1,2,2,2,0,1,1,1],"metric":true},{"config":[2,0,0,0,1,1,1,2],"metric":true},{"config":[2,0,0,0,1,1,2,2],"metric":true},{"config":[2,0,0,0,1,2,2,2],"metric":true},{"config":[2,0,0,1,1,0,2,2],"metric":true},{"config":[2,0,0,1,1,1,0,2],"metric":true},{"config":[2,0,0,1,1,1,2,2],"metric":true},{"config":[2,0,0,1,1,2,2,2],"metric":true},{"config":[2,0,1,1,1,0,0,2],"metric":true},{"config":[2,0,1,1,1,0,2,2],"metric":true},{"config":[2,0,1,1,1,2,2,2],"metric":true},{"config":[2,0,2,1,1,0,2,2],"metric":true},{"config":[2,0,2,1,1,1,2,2],"metric":true},{"config":[2,1,0,0,0,1,1,2],"metric":true},{"config":[2,1,0,0,0,1,2,2],"metric":true},{"config":[2,1,0,0,0,2,2,2],"metric":true},{"config":[2,1,1,0,0,0,1,2],"metric":true},{"config":[2,1,1,0,0,0,2,2],"metric":true},{"config":[2,1,1,0,0,1,2,2],"metric":true},{"config":[2,1,1,0,0,2,2,2],"metric":true},{"config":[2,1,1,1,0,0,0,2],"metric":true},{"config":[2,1,1,1,0,0,2,2],"metric":true},{"config":[2,1,1,1,0,2,2,2],"metric":true},{"config":[2,1,2,0,0,0,2,2],"metric":true},{"config":[2,1,2,0,0,1,2,2],"metric":true},{"config":[2,2,0,0,0,1,1,1],"metric":true},{"config":[2,2,0,0,0,1,1,2],"metric":true},{"config":[2,2,0,0,0,2,1,1],"metric":true},{"config":[2,2,0,0,1,0,0,2],"metric":true},{"config":[2,2,0,0,1,1,0,0],"metric":true},{"config":[2,2,0,0,1,1,0,2],"metric":true},{"config":[2,2,0,0,1,1,1,2],"metric":true},{"config":[2,2,0,0,1,2,0,0],"metric":true},{"config":[2,2,0,1,1,0,0,0],"metric":true},{"config":[2,2,0,1,1,0,0,2],"metric":true},{"config":[2,2,0,1,1,1,0,0],"metric":true},{"config":[2,2,0,1,1,1,0,2],"metric":true},{"config":[2,2,0,1,1,2,0,0],"metric":true},{"config":[2,2,1,0,0,0,1,1],"metric":true},{"config":[2,2,1,0,0,0,1,2],"metric":true},{"config":[2,2,1,0,0,1,1,1],"metric":true},{"config":[2,2,1,0,0,1,1,2],"metric":true},{"config":[2,2,1,0,0,2,1,1],"metric":true},{"config":[2,2,1,1,0,0,0,2],"metric":true},{"config":[2,2,1,1,0,0,1,1],"metric":true},{"config":[2,2,1,1,0,0,1,2],"metric":true},{"config":[2,2,1,1,0,1,1,2],"metric":true},{"config":[2,2,1,1,0,2,1,1],"metric":true},{"config":[2,2,1,1,1,0,0,0],"metric":true},{"config":[2,2,1,1,1,0,0,2],"metric":true},{"config":[2,2,1,1,1,2,0,0],"metric":true},{"config":[2,2,2,0,0,0,1,1],"metric":true},{"config":[2,2,2,0,0,1,1,1],"metric":true},{"config":[2,2,2,1,1,0,0,0],"metric":true},{"config":[2,2,2,1,1,1,0,0],"metric":true}]}, {"problem":"CircuitSAT","variant":{},"instance":{"circuit":{"assignments":[{"expr":{"op":{"And":[{"op":{"Var":"x1"}},{"op":{"Var":"x2"}}]}},"outputs":["a"]},{"expr":{"op":{"Or":[{"op":{"Var":"x1"}},{"op":{"Var":"x2"}}]}},"outputs":["b"]},{"expr":{"op":{"Xor":[{"op":{"Var":"a"}},{"op":{"Var":"b"}}]}},"outputs":["c"]}]},"variables":["a","b","c","x1","x2"]},"samples":[{"config":[0,1,1,0,1],"metric":true},{"config":[0,1,1,1,0],"metric":true}],"optimal":[{"config":[0,0,0,0,0],"metric":true},{"config":[0,1,1,0,1],"metric":true},{"config":[0,1,1,1,0],"metric":true},{"config":[1,1,0,1,1],"metric":true}]}, {"problem":"ClosestVectorProblem","variant":{"weight":"i32"},"instance":{"basis":[[2,0],[1,2]],"bounds":[{"lower":-2,"upper":4},{"lower":-2,"upper":4}],"target":[2.8,1.5]},"samples":[{"config":[3,3],"metric":{"Valid":0.5385164807134505}}],"optimal":[{"config":[3,3],"metric":{"Valid":0.5385164807134505}}]}, + {"problem":"ConjunctiveBooleanQuery","variant":{},"instance":{"conjuncts":[[0,[{"Variable":0},{"Constant":3}]],[0,[{"Variable":1},{"Constant":3}]],[1,[{"Variable":0},{"Variable":1},{"Constant":5}]]],"domain_size":6,"num_variables":2,"relations":[{"arity":2,"tuples":[[0,3],[1,3],[2,4],[3,4],[4,5]]},{"arity":3,"tuples":[[0,1,5],[1,2,5],[2,3,4],[0,4,3]]}]},"samples":[{"config":[0,1],"metric":true}],"optimal":[{"config":[0,1],"metric":true}]}, {"problem":"DirectedTwoCommodityIntegralFlow","variant":{},"instance":{"capacities":[1,1,1,1,1,1,1,1],"graph":{"inner":{"edge_property":"directed","edges":[[0,2,null],[0,3,null],[1,2,null],[1,3,null],[2,4,null],[2,5,null],[3,4,null],[3,5,null]],"node_holes":[],"nodes":[null,null,null,null,null,null]}},"requirement_1":1,"requirement_2":1,"sink_1":4,"sink_2":5,"source_1":0,"source_2":1},"samples":[{"config":[1,0,0,0,1,0,0,0,0,0,0,1,0,0,0,1],"metric":true}],"optimal":[{"config":[0,0,0,1,0,0,1,0,0,0,1,0,0,1,0,0],"metric":true},{"config":[0,0,0,1,0,0,1,0,0,1,0,0,0,0,0,1],"metric":true},{"config":[0,0,0,1,0,0,1,0,0,1,1,0,0,1,0,1],"metric":true},{"config":[0,0,0,1,0,0,1,0,0,1,1,0,1,0,0,1],"metric":true},{"config":[0,0,0,1,0,0,1,0,1,0,0,0,0,1,0,0],"metric":true},{"config":[0,0,0,1,0,0,1,0,1,0,1,0,1,1,0,0],"metric":true},{"config":[0,0,0,1,0,0,1,0,1,1,0,0,0,1,0,1],"metric":true},{"config":[0,0,0,1,0,0,1,0,1,1,0,0,1,0,0,1],"metric":true},{"config":[0,0,0,1,0,0,1,0,1,1,1,0,1,1,0,1],"metric":true},{"config":[0,0,1,0,1,0,0,0,0,0,0,1,0,0,0,1],"metric":true},{"config":[0,0,1,0,1,0,0,0,0,1,0,0,0,0,0,1],"metric":true},{"config":[0,0,1,0,1,0,0,0,0,1,0,1,0,0,1,1],"metric":true},{"config":[0,0,1,0,1,0,0,0,1,0,0,0,0,1,0,0],"metric":true},{"config":[0,0,1,0,1,0,0,0,1,0,0,1,0,1,0,1],"metric":true},{"config":[0,0,1,0,1,0,0,0,1,0,0,1,0,1,1,0],"metric":true},{"config":[0,0,1,0,1,0,0,0,1,1,0,0,0,1,0,1],"metric":true},{"config":[0,0,1,0,1,0,0,0,1,1,0,0,0,1,1,0],"metric":true},{"config":[0,0,1,0,1,0,0,0,1,1,0,1,0,1,1,1],"metric":true},{"config":[0,0,1,1,0,1,1,0,0,1,0,0,0,0,0,1],"metric":true},{"config":[0,0,1,1,0,1,1,0,1,1,0,0,1,0,0,1],"metric":true},{"config":[0,0,1,1,1,0,0,1,1,0,0,0,0,1,0,0],"metric":true},{"config":[0,0,1,1,1,0,0,1,1,1,0,0,0,1,1,0],"metric":true},{"config":[0,0,1,1,1,0,1,0,0,1,0,0,0,0,0,1],"metric":true},{"config":[0,0,1,1,1,0,1,0,1,0,0,0,0,1,0,0],"metric":true},{"config":[0,0,1,1,1,0,1,0,1,1,0,0,0,1,0,1],"metric":true},{"config":[0,1,0,0,0,0,1,0,0,0,0,1,0,0,0,1],"metric":true},{"config":[0,1,0,0,0,0,1,0,0,0,1,0,0,1,0,0],"metric":true},{"config":[0,1,0,0,0,0,1,0,0,0,1,1,0,1,0,1],"metric":true},{"config":[0,1,0,0,0,0,1,0,0,0,1,1,1,0,0,1],"metric":true},{"config":[0,1,0,0,0,0,1,0,1,0,0,0,0,1,0,0],"metric":true},{"config":[0,1,0,0,0,0,1,0,1,0,0,1,0,1,0,1],"metric":true},{"config":[0,1,0,0,0,0,1,0,1,0,0,1,1,0,0,1],"metric":true},{"config":[0,1,0,0,0,0,1,0,1,0,1,0,1,1,0,0],"metric":true},{"config":[0,1,0,0,0,0,1,0,1,0,1,1,1,1,0,1],"metric":true},{"config":[0,1,0,1,0,0,1,1,0,0,1,0,0,1,0,0],"metric":true},{"config":[0,1,0,1,0,0,1,1,1,0,0,0,0,1,0,0],"metric":true},{"config":[0,1,0,1,0,0,1,1,1,0,1,0,1,1,0,0],"metric":true},{"config":[0,1,1,0,0,1,1,0,0,0,0,1,0,0,0,1],"metric":true},{"config":[0,1,1,0,0,1,1,0,1,0,0,1,1,0,0,1],"metric":true},{"config":[0,1,1,0,1,0,0,1,1,0,0,0,0,1,0,0],"metric":true},{"config":[0,1,1,0,1,0,0,1,1,0,0,1,0,1,1,0],"metric":true},{"config":[0,1,1,0,1,0,1,0,0,0,0,1,0,0,0,1],"metric":true},{"config":[0,1,1,0,1,0,1,0,1,0,0,0,0,1,0,0],"metric":true},{"config":[0,1,1,0,1,0,1,0,1,0,0,1,0,1,0,1],"metric":true},{"config":[0,1,1,1,1,0,1,1,1,0,0,0,0,1,0,0],"metric":true},{"config":[1,0,0,0,1,0,0,0,0,0,0,1,0,0,0,1],"metric":true},{"config":[1,0,0,0,1,0,0,0,0,0,1,0,0,1,0,0],"metric":true},{"config":[1,0,0,0,1,0,0,0,0,0,1,1,0,1,0,1],"metric":true},{"config":[1,0,0,0,1,0,0,0,0,0,1,1,0,1,1,0],"metric":true},{"config":[1,0,0,0,1,0,0,0,0,1,0,0,0,0,0,1],"metric":true},{"config":[1,0,0,0,1,0,0,0,0,1,0,1,0,0,1,1],"metric":true},{"config":[1,0,0,0,1,0,0,0,0,1,1,0,0,1,0,1],"metric":true},{"config":[1,0,0,0,1,0,0,0,0,1,1,0,0,1,1,0],"metric":true},{"config":[1,0,0,0,1,0,0,0,0,1,1,1,0,1,1,1],"metric":true},{"config":[1,0,0,1,0,1,1,0,0,1,0,0,0,0,0,1],"metric":true},{"config":[1,0,0,1,0,1,1,0,0,1,1,0,1,0,0,1],"metric":true},{"config":[1,0,0,1,1,0,0,1,0,0,1,0,0,1,0,0],"metric":true},{"config":[1,0,0,1,1,0,0,1,0,1,1,0,0,1,1,0],"metric":true},{"config":[1,0,0,1,1,0,1,0,0,0,1,0,0,1,0,0],"metric":true},{"config":[1,0,0,1,1,0,1,0,0,1,0,0,0,0,0,1],"metric":true},{"config":[1,0,0,1,1,0,1,0,0,1,1,0,0,1,0,1],"metric":true},{"config":[1,0,1,0,1,1,0,0,0,0,0,1,0,0,0,1],"metric":true},{"config":[1,0,1,0,1,1,0,0,0,1,0,0,0,0,0,1],"metric":true},{"config":[1,0,1,0,1,1,0,0,0,1,0,1,0,0,1,1],"metric":true},{"config":[1,0,1,1,1,1,1,0,0,1,0,0,0,0,0,1],"metric":true},{"config":[1,1,0,0,0,1,1,0,0,0,0,1,0,0,0,1],"metric":true},{"config":[1,1,0,0,0,1,1,0,0,0,1,1,1,0,0,1],"metric":true},{"config":[1,1,0,0,1,0,0,1,0,0,1,0,0,1,0,0],"metric":true},{"config":[1,1,0,0,1,0,0,1,0,0,1,1,0,1,1,0],"metric":true},{"config":[1,1,0,0,1,0,1,0,0,0,0,1,0,0,0,1],"metric":true},{"config":[1,1,0,0,1,0,1,0,0,0,1,0,0,1,0,0],"metric":true},{"config":[1,1,0,0,1,0,1,0,0,0,1,1,0,1,0,1],"metric":true},{"config":[1,1,0,1,1,0,1,1,0,0,1,0,0,1,0,0],"metric":true},{"config":[1,1,1,0,1,1,1,0,0,0,0,1,0,0,0,1],"metric":true}]}, {"problem":"ExactCoverBy3Sets","variant":{},"instance":{"subsets":[[0,1,2],[0,2,4],[3,4,5],[3,5,7],[6,7,8],[1,4,6],[2,5,8]],"universe_size":9},"samples":[{"config":[1,0,1,0,1,0,0],"metric":true}],"optimal":[{"config":[1,0,1,0,1,0,0],"metric":true}]}, {"problem":"Factoring","variant":{},"instance":{"m":2,"n":3,"target":15},"samples":[{"config":[1,1,1,0,1],"metric":{"Valid":0}}],"optimal":[{"config":[1,1,1,0,1],"metric":{"Valid":0}}]}, @@ -52,7 +53,7 @@ {"source":{"problem":"KSatisfiability","variant":{"k":"K2"},"instance":{"clauses":[{"literals":[1,2]},{"literals":[-1,3]},{"literals":[-2,4]},{"literals":[-3,-4]}],"num_vars":4}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[0.0,1.0,-1.0,0.0],[0.0,0.0,0.0,-1.0],[0.0,0.0,0.0,1.0],[0.0,0.0,0.0,0.0]],"num_vars":4}},"solutions":[{"source_config":[0,1,0,1],"target_config":[0,1,0,1]}]}, {"source":{"problem":"KSatisfiability","variant":{"k":"K3"},"instance":{"clauses":[{"literals":[1,2,-3]},{"literals":[-1,3,4]},{"literals":[2,-4,5]},{"literals":[-2,3,-5]},{"literals":[1,-3,5]},{"literals":[-1,-2,4]},{"literals":[3,-4,-5]}],"num_vars":5}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[0.0,4.0,-4.0,0.0,0.0,4.0,-4.0,0.0,0.0,4.0,-4.0,0.0],[0.0,0.0,-2.0,-2.0,0.0,4.0,0.0,4.0,-4.0,0.0,-4.0,0.0],[0.0,0.0,2.0,-2.0,0.0,1.0,4.0,0.0,4.0,-4.0,0.0,4.0],[0.0,0.0,0.0,4.0,0.0,0.0,-1.0,-4.0,0.0,0.0,-1.0,-4.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,-1.0,1.0,-1.0,0.0,1.0],[0.0,0.0,0.0,0.0,0.0,-2.0,0.0,0.0,0.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,3.0,0.0,0.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,3.0,0.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,2.0,0.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,3.0,0.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,7.0,0.0],[0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,2.0]],"num_vars":12}},"solutions":[{"source_config":[0,0,0,0,0],"target_config":[0,0,0,0,0,1,0,0,0,0,0,0]}]}, {"source":{"problem":"KSatisfiability","variant":{"k":"K3"},"instance":{"clauses":[{"literals":[1,2,3]},{"literals":[-1,-2,3]}],"num_vars":3}},"target":{"problem":"SubsetSum","variant":{},"instance":{"sizes":["10010","10001","1010","1001","111","100","10","20","1","2"],"target":"11144"}},"solutions":[{"source_config":[0,0,1],"target_config":[0,1,0,1,1,0,1,1,1,0]}]}, - {"source":{"problem":"KSatisfiability","variant":{"k":"KN"},"instance":{"clauses":[{"literals":[1,-2,3]},{"literals":[-1,3,4]},{"literals":[2,-3,-4]}],"num_vars":4}},"target":{"problem":"Satisfiability","variant":{},"instance":{"clauses":[{"literals":[1,-2,3]},{"literals":[-1,3,4]},{"literals":[2,-3,-4]}],"num_vars":4}},"solutions":[{"source_config":[1,1,1,0],"target_config":[1,1,1,0]}]}, + {"source":{"problem":"KSatisfiability","variant":{"k":"KN"},"instance":{"clauses":[{"literals":[1,-2,3]},{"literals":[-1,3,4]},{"literals":[2,-3,-4]}],"num_vars":4}},"target":{"problem":"Satisfiability","variant":{},"instance":{"clauses":[{"literals":[1,-2,3]},{"literals":[-1,3,4]},{"literals":[2,-3,-4]}],"num_vars":4}},"solutions":[{"source_config":[1,1,1,1],"target_config":[1,1,1,1]}]}, {"source":{"problem":"Knapsack","variant":{},"instance":{"capacity":7,"values":[3,4,5,7],"weights":[2,3,4,5]}},"target":{"problem":"QUBO","variant":{"weight":"f64"},"instance":{"matrix":[[-483.0,240.0,320.0,400.0,80.0,160.0,320.0],[0.0,-664.0,480.0,600.0,120.0,240.0,480.0],[0.0,0.0,-805.0,800.0,160.0,320.0,640.0],[0.0,0.0,0.0,-907.0,200.0,400.0,800.0],[0.0,0.0,0.0,0.0,-260.0,80.0,160.0],[0.0,0.0,0.0,0.0,0.0,-480.0,320.0],[0.0,0.0,0.0,0.0,0.0,0.0,-800.0]],"num_vars":7}},"solutions":[{"source_config":[1,0,0,1],"target_config":[1,0,0,1,0,0,0]}]}, {"source":{"problem":"LongestCommonSubsequence","variant":{},"instance":{"strings":[[65,66,65,67],[66,65,67,65]]}},"target":{"problem":"ILP","variant":{"variable":"bool"},"instance":{"constraints":[{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[1,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[3,1.0],[4,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[5,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[2,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[3,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[5,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[4,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[0,1.0],[2,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[2,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[3,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[1,1.0],[5,1.0]]},{"cmp":"Le","rhs":1.0,"terms":[[4,1.0],[5,1.0]]}],"num_vars":6,"objective":[[0,1.0],[1,1.0],[2,1.0],[3,1.0],[4,1.0],[5,1.0]],"sense":"Maximize"}},"solutions":[{"source_config":[0,1,1,1],"target_config":[0,0,1,1,0,1]}]}, {"source":{"problem":"MaxCut","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"edge_weights":[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}}}},"target":{"problem":"SpinGlass","variant":{"graph":"SimpleGraph","weight":"i32"},"instance":{"couplings":[1,1,1,1,1,1,1,1,1,1,1,1,1,1,1],"fields":[0,0,0,0,0,0,0,0,0,0],"graph":{"inner":{"edge_property":"undirected","edges":[[0,1,null],[0,4,null],[0,5,null],[1,2,null],[1,6,null],[2,3,null],[2,7,null],[3,4,null],[3,8,null],[4,9,null],[5,7,null],[5,8,null],[6,8,null],[6,9,null],[7,9,null]],"node_holes":[],"nodes":[null,null,null,null,null,null,null,null,null,null]}}}},"solutions":[{"source_config":[0,1,0,1,0,1,0,0,0,1],"target_config":[0,1,0,1,0,1,0,0,0,1]}]}, From d06a1d42ebe478dbed038169c1442f5253e1b5b7 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Tue, 17 Mar 2026 10:35:25 +0800 Subject: [PATCH 4/8] Add paper entry for ConjunctiveBooleanQuery (#449) --- docs/paper/reductions.typ | 63 +++++++++++++++++++++++++++++++++++++++ docs/paper/references.bib | 29 ++++++++++++++++++ 2 files changed, 92 insertions(+) diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 01372f7cb..f3842cc17 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -112,6 +112,7 @@ "MinimumTardinessSequencing": [Minimum Tardiness Sequencing], "SequencingWithinIntervals": [Sequencing Within Intervals], "DirectedTwoCommodityIntegralFlow": [Directed Two-Commodity Integral Flow], + "ConjunctiveBooleanQuery": [Conjunctive Boolean Query], ) // Definition label: "def:" — each definition block must have a matching label @@ -2326,6 +2327,68 @@ NP-completeness was established by Garey, Johnson, and Stockmeyer @gareyJohnsonS ) ] +#{ + let x = load-model-example("ConjunctiveBooleanQuery") + let d = x.instance.domain_size + let nv = x.instance.num_variables + let rels = x.instance.relations + let conj = x.instance.conjuncts + let nr = rels.len() + let nc = conj.len() + let sol = x.optimal.at(0) + let assignment = sol.config + [ + #problem-def("ConjunctiveBooleanQuery")[ + Given a finite domain $D = {0, dots, d - 1}$, a collection of relations $R_0, R_1, dots, R_(m-1)$ where each $R_i$ is a set of $a_i$-tuples with entries from $D$, and a conjunctive Boolean query + $ Q = (exists y_0, y_1, dots, y_(l-1))(A_0 and A_1 and dots.c and A_(r-1)) $ + where each _atom_ $A_j$ has the form $R_(i_j)(u_0, u_1, dots)$ with every $u$ in ${y_0, dots, y_(l-1)} union D$, determine whether there exists an assignment to the variables that makes $Q$ true --- i.e., the resolved tuple of every atom belongs to its relation. + ][ + The Conjunctive Boolean Query (CBQ) problem is one of the most fundamental problems in database theory and finite model theory. #cite(, form: "prose") showed that evaluating conjunctive queries is NP-complete by reduction from the Clique problem. CBQ is equivalent to the Constraint Satisfaction Problem (CSP) and to the homomorphism problem for relational structures; this equivalence connects database query evaluation, constraint programming, and graph theory under a single computational framework @kolaitis2000. + + For queries of bounded _hypertree-width_, evaluation becomes polynomial-time @gottlob2002. The general brute-force algorithm enumerates all $d^l$ variable assignments and checks every atom, running in $O(d^l dot r dot max_i a_i)$ time.#footnote[No substantially faster general algorithm is known for arbitrary conjunctive Boolean queries.] + + *Example.* Let $D = {0, dots, #(d - 1)}$ ($d = #d$), with #nr relations: + + #align(center, grid( + columns: nr, + gutter: 1.5em, + ..range(nr).map(ri => { + let rel = rels.at(ri) + let arity = rel.arity + let header = range(arity).map(j => [$c_#j$]) + table( + columns: arity + 1, + align: center, + inset: (x: 4pt, y: 3pt), + table.header([$R_#ri$], ..header), + table.hline(stroke: 0.3pt), + ..rel.tuples.enumerate().map(((ti, tup)) => { + let cells = tup.map(v => [#v]) + ([$tau_#ti$], ..cells) + }).flatten() + ) + }) + )) + + The query has #nv variables $(y_0, y_1)$ and #nc atoms: + #{ + let fmt-arg(a) = { + if "Variable" in a { $y_#(a.Variable)$ } + else { $#(a.Constant)$ } + } + let atoms = conj.enumerate().map(((j, c)) => { + let ri = c.at(0) + let args = c.at(1) + [$A_#j = R_#ri (#args.map(fmt-arg).join($, $))$] + }) + [$ Q = (exists y_0, y_1)(#atoms.join($ and $)) $] + } + + Under the assignment $y_0 = #assignment.at(0)$, $y_1 = #assignment.at(1)$: atom $A_0$ resolves to $(#assignment.at(0), 3) in R_0$ (row $tau_0$), atom $A_1$ resolves to $(#assignment.at(1), 3) in R_0$ (row $tau_1$), and atom $A_2$ resolves to $(#assignment.at(0), #assignment.at(1), 5) in R_1$ (row $tau_0$). All three atoms are satisfied, so $Q$ is true. + ] + ] +} + // Completeness check: warn about problem types in JSON but missing from paper #{ let json-models = { diff --git a/docs/paper/references.bib b/docs/paper/references.bib index 6482b48a2..662421fa7 100644 --- a/docs/paper/references.bib +++ b/docs/paper/references.bib @@ -693,6 +693,35 @@ @article{even1976 doi = {10.1137/0205048} } +@article{chandra1977, + author = {Ashok K. Chandra and Philip M. Merlin}, + title = {Optimal Implementation of Conjunctive Queries in Relational Data Bases}, + journal = {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} +} + +@incollection{kolaitis2000, + 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}, From 4cdbbd716364b850699847491318dac316e6188a Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Tue, 17 Mar 2026 10:51:40 +0800 Subject: [PATCH 5/8] Review fixes: add PartialEq derives, fix bib key kolaitis2000->kolaitis1998 --- docs/paper/reductions.typ | 2 +- docs/paper/references.bib | 2 +- src/models/misc/conjunctive_boolean_query.rs | 6 +++--- src/unit_tests/models/misc/conjunctive_boolean_query.rs | 5 +---- 4 files changed, 6 insertions(+), 9 deletions(-) diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index f3842cc17..e3ad41a2a 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -2343,7 +2343,7 @@ NP-completeness was established by Garey, Johnson, and Stockmeyer @gareyJohnsonS $ Q = (exists y_0, y_1, dots, y_(l-1))(A_0 and A_1 and dots.c and A_(r-1)) $ where each _atom_ $A_j$ has the form $R_(i_j)(u_0, u_1, dots)$ with every $u$ in ${y_0, dots, y_(l-1)} union D$, determine whether there exists an assignment to the variables that makes $Q$ true --- i.e., the resolved tuple of every atom belongs to its relation. ][ - The Conjunctive Boolean Query (CBQ) problem is one of the most fundamental problems in database theory and finite model theory. #cite(, form: "prose") showed that evaluating conjunctive queries is NP-complete by reduction from the Clique problem. CBQ is equivalent to the Constraint Satisfaction Problem (CSP) and to the homomorphism problem for relational structures; this equivalence connects database query evaluation, constraint programming, and graph theory under a single computational framework @kolaitis2000. + The Conjunctive Boolean Query (CBQ) problem is one of the most fundamental problems in database theory and finite model theory. #cite(, form: "prose") showed that evaluating conjunctive queries is NP-complete by reduction from the Clique problem. CBQ is equivalent to the Constraint Satisfaction Problem (CSP) and to the homomorphism problem for relational structures; this equivalence connects database query evaluation, constraint programming, and graph theory under a single computational framework @kolaitis1998. For queries of bounded _hypertree-width_, evaluation becomes polynomial-time @gottlob2002. The general brute-force algorithm enumerates all $d^l$ variable assignments and checks every atom, running in $O(d^l dot r dot max_i a_i)$ time.#footnote[No substantially faster general algorithm is known for arbitrary conjunctive Boolean queries.] diff --git a/docs/paper/references.bib b/docs/paper/references.bib index 662421fa7..1de33b0c5 100644 --- a/docs/paper/references.bib +++ b/docs/paper/references.bib @@ -713,7 +713,7 @@ @article{gottlob2002 doi = {10.1006/jcss.2001.1809} } -@incollection{kolaitis2000, +@incollection{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)}, diff --git a/src/models/misc/conjunctive_boolean_query.rs b/src/models/misc/conjunctive_boolean_query.rs index 4dd9fbe1d..c01db77bc 100644 --- a/src/models/misc/conjunctive_boolean_query.rs +++ b/src/models/misc/conjunctive_boolean_query.rs @@ -32,7 +32,7 @@ inventory::submit! { } /// A relation with fixed arity and a set of tuples over a finite domain. -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)] pub struct Relation { /// The arity (number of columns) of this relation. pub arity: usize, @@ -41,7 +41,7 @@ pub struct Relation { } /// An argument in a conjunctive query atom. -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)] pub enum QueryArg { /// A reference to existential variable `y_i` (0-indexed). Variable(usize), @@ -79,7 +79,7 @@ pub enum QueryArg { /// let solution = solver.find_satisfying(&problem); /// assert!(solution.is_some()); /// ``` -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)] pub struct ConjunctiveBooleanQuery { domain_size: usize, relations: Vec, diff --git a/src/unit_tests/models/misc/conjunctive_boolean_query.rs b/src/unit_tests/models/misc/conjunctive_boolean_query.rs index 4bc53fda0..3da1f3cfc 100644 --- a/src/unit_tests/models/misc/conjunctive_boolean_query.rs +++ b/src/unit_tests/models/misc/conjunctive_boolean_query.rs @@ -113,10 +113,7 @@ fn test_conjunctivebooleanquery_serialization() { let problem = issue_example(); let json = serde_json::to_value(&problem).unwrap(); let restored: ConjunctiveBooleanQuery = serde_json::from_value(json).unwrap(); - assert_eq!(restored.domain_size(), problem.domain_size()); - assert_eq!(restored.num_relations(), problem.num_relations()); - assert_eq!(restored.num_variables(), problem.num_variables()); - assert_eq!(restored.num_conjuncts(), problem.num_conjuncts()); + assert_eq!(restored, problem); } #[test] From 7d438ed84ab50cdaf2b62eb39dee772355740cd1 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Tue, 17 Mar 2026 10:51:57 +0800 Subject: [PATCH 6/8] chore: remove plan file after implementation --- .../2026-03-17-conjunctive-boolean-query.md | 167 ------------------ 1 file changed, 167 deletions(-) delete mode 100644 docs/plans/2026-03-17-conjunctive-boolean-query.md diff --git a/docs/plans/2026-03-17-conjunctive-boolean-query.md b/docs/plans/2026-03-17-conjunctive-boolean-query.md deleted file mode 100644 index 0b5cae988..000000000 --- a/docs/plans/2026-03-17-conjunctive-boolean-query.md +++ /dev/null @@ -1,167 +0,0 @@ -# Plan: [Model] ConjunctiveBooleanQuery (#449) - -## Overview - -Add the **Conjunctive Boolean Query** (CBQ) problem model — a satisfaction problem from database theory (Garey & Johnson A4 SR31). Given a finite domain D, a collection of relations R, and an existentially quantified conjunctive query Q, determine whether Q is true over R and D. - -This is equivalent to the Constraint Satisfaction Problem (CSP) and the Graph Homomorphism problem. NP-complete via reduction from CLIQUE (Chandra & Merlin, 1977). - -**Category:** `misc/` (unique input structure: domain + relations + conjunctive query) - -## Information Checklist - -| # | Item | Value | -|---|------|-------| -| 1 | Problem name | `ConjunctiveBooleanQuery` | -| 2 | Mathematical definition | INSTANCE: Finite domain D, relations R={R_1,...,R_m}, conjunctive query Q = (∃y_1,...,y_l)(A_1 ∧ ... ∧ A_r). QUESTION: Is Q true? | -| 3 | Problem type | Satisfaction (`Metric = bool`) | -| 4 | Type parameters | None | -| 5 | Struct fields | `domain_size: usize`, `relations: Vec`, `num_variables: usize`, `conjuncts: Vec<(usize, Vec)>` | -| 6 | Configuration space | `vec![domain_size; num_variables]` — l variables each over domain D | -| 7 | Feasibility check | For each conjunct (rel_idx, args), substitute variables from config and check tuple membership in the relation | -| 8 | Objective function | N/A (satisfaction) | -| 9 | Best known exact | Brute-force O(|D|^l * r * max_arity). No substantially faster general algorithm known. | -| 10 | Solving strategy | BruteForce (enumerate all |D|^l assignments) | -| 11 | Category | `misc` | -| 12 | Expected outcome | Example: D={0..5}, 2 relations (binary+ternary), query with 2 variables, 3 conjuncts → TRUE, satisfying assignment y_1=0, y_2=1 | - -## Batch 1: Implementation (Steps 1-5.5) - -### Task 1.1: Create model file `src/models/misc/conjunctive_boolean_query.rs` - -Define companion types and the main struct: - -```rust -/// A relation with fixed arity and a set of tuples. -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct Relation { - pub arity: usize, - pub tuples: Vec>, -} - -/// An argument in a conjunctive query: either a bound variable or a domain constant. -#[derive(Debug, Clone, Serialize, Deserialize)] -pub enum QueryArg { - Variable(usize), - Constant(usize), -} - -/// The Conjunctive Boolean Query problem. -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct ConjunctiveBooleanQuery { - domain_size: usize, - relations: Vec, - num_variables: usize, - conjuncts: Vec<(usize, Vec)>, -} -``` - -**Constructor:** `new(domain_size, relations, num_variables, conjuncts)` with validation: -- All relation tuples have correct arity -- All tuple entries < domain_size -- All conjunct relation indices are valid -- All conjunct args reference valid variable indices or constants < domain_size -- Conjunct argument count matches relation arity - -**Getter methods:** `domain_size()`, `num_relations()`, `num_variables()`, `num_conjuncts()`, `relations()`, `conjuncts()` - -**Problem trait impl:** -- `NAME = "ConjunctiveBooleanQuery"` -- `type Metric = bool` -- `variant() -> crate::variant_params![]` -- `dims() -> vec![self.domain_size; self.num_variables]` -- `evaluate(config)`: for each conjunct, resolve args (Variable → config[idx], Constant → value), check if resulting tuple is in the relation - -**SatisfactionProblem impl:** marker trait - -**`declare_variants!`:** -```rust -crate::declare_variants! { - default sat ConjunctiveBooleanQuery => "domain_size ^ num_variables", -} -``` - -**ProblemSchemaEntry:** -```rust -inventory::submit! { - ProblemSchemaEntry { - name: "ConjunctiveBooleanQuery", - display_name: "Conjunctive Boolean Query", - aliases: &["CBQ"], - dimensions: &[], - module_path: module_path!(), - description: "Evaluate a conjunctive Boolean query over a relational database", - fields: &[ - FieldInfo { name: "domain_size", type_name: "usize", description: "Size of the finite domain D" }, - FieldInfo { name: "relations", type_name: "Vec", description: "Collection of relations R" }, - FieldInfo { name: "num_variables", type_name: "usize", description: "Number of existentially quantified variables" }, - FieldInfo { name: "conjuncts", type_name: "Vec<(usize, Vec)>", description: "Query conjuncts: (relation_index, arguments)" }, - ], - } -} -``` - -### Task 1.2: Register in module tree - -1. **`src/models/misc/mod.rs`:** Add `mod conjunctive_boolean_query;` and `pub use conjunctive_boolean_query::{ConjunctiveBooleanQuery, Relation as CbqRelation, QueryArg};` -2. **`src/models/mod.rs`:** Add to misc re-exports -3. **`src/lib.rs`/prelude:** Add ConjunctiveBooleanQuery to prelude if needed - -### Task 1.3: CLI registration - -1. **`problemreductions-cli/src/problem_name.rs`:** Add alias `"cbq" => "ConjunctiveBooleanQuery"` (CBQ is not a well-established abbreviation, so only add lowercase pass-through; the `aliases` in ProblemSchemaEntry handles `CBQ`) -2. **`problemreductions-cli/src/commands/create.rs`:** - - Add CLI flags to `CreateArgs` in `cli.rs`: `--domain-size`, `--relations`, `--conjuncts` - - Add match arm for `"ConjunctiveBooleanQuery"` that parses these flags - - Add to `help_data_flags()` table - - Update `all_data_flags_empty()` if new flags added -3. **`problemreductions-cli/src/cli.rs`:** Add the new flag fields - -### Task 1.4: Add canonical model example to example_db - -Add `canonical_model_example_specs()` to the model file (feature-gated with `example-db`): - -Use the issue's example instance: -- D = {0,...,5}, R_1 (arity 2): {(0,3),(1,3),(2,4),(3,4),(4,5)}, R_2 (arity 3): {(0,1,5),(1,2,5),(2,3,4),(0,4,3)} -- Query: (∃y_1,y_2)(R_1(y_1,3) ∧ R_1(y_2,3) ∧ R_2(y_1,y_2,5)) -- But keep it small enough for brute force (6^2 = 36 configs — fine) - -Register in `src/models/misc/mod.rs`'s `canonical_model_example_specs()`. - -### Task 1.5: Write unit tests `src/unit_tests/models/misc/conjunctive_boolean_query.rs` - -Required tests (≥3): -- `test_conjunctivebooleanquery_basic` — create instance, verify dims, getters, NAME -- `test_conjunctivebooleanquery_evaluate_yes` — verify satisfying assignment y_1=0, y_2=1 -- `test_conjunctivebooleanquery_evaluate_no` — verify non-satisfying assignment -- `test_conjunctivebooleanquery_out_of_range` — variable value ≥ domain_size returns false -- `test_conjunctivebooleanquery_brute_force` — BruteForce finds satisfying assignment -- `test_conjunctivebooleanquery_unsatisfiable` — instance with no solution -- `test_conjunctivebooleanquery_serialization` — round-trip serde JSON -- `test_conjunctivebooleanquery_paper_example` — same instance as paper, verify expected solution and count - -Link test file via `#[cfg(test)] #[path = "../../unit_tests/models/misc/conjunctive_boolean_query.rs"] mod tests;` - -### Task 1.6: Verify build and tests - -```bash -make check # fmt + clippy + test -``` - -## Batch 2: Paper Entry (Step 6) - -### Task 2.1: Write paper entry in `docs/paper/reductions.typ` - -1. Add to `display-name` dict: `"ConjunctiveBooleanQuery": [Conjunctive Boolean Query]` -2. Add `#problem-def("ConjunctiveBooleanQuery")[definition][body]` with: - - Formal definition: domain D, relations R, conjunctive query Q - - Background: classical in database theory, equivalent to CSP and graph homomorphism - - Best known algorithm: brute-force O(|D|^l), cite Chandra & Merlin 1977 - - Example with CeTZ visualization: show the relations as tables, the query structure, and the satisfying assignment - - Evaluation: verify the three conjuncts on (y_1=0, y_2=1) -3. Build: `make paper` - -## Dependencies - -- Batch 2 depends on Batch 1 (needs exports from compiled code) -- No external model dependencies (this is a standalone model) From c8aaf8841d597600d10e555b41217847af1827d5 Mon Sep 17 00:00:00 2001 From: zazabap Date: Thu, 19 Mar 2026 07:59:30 +0000 Subject: [PATCH 7/8] fix: address PR #689 review comments MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Fix BibTeX entry types: chandra1977 @article -> @inproceedings, kolaitis1998 @incollection -> @inproceedings - Support empty relations in CLI parsing (e.g., "2:" produces empty relation) - Pre-validate CLI input before calling ConjunctiveBooleanQuery::new(): tuple arity, domain bounds, relation indices, conjunct arity, constant bounds — returns user-facing errors instead of panicking Co-Authored-By: Claude Opus 4.6 (1M context) --- docs/paper/references.bib | 16 ++--- problemreductions-cli/src/commands/create.rs | 63 ++++++++++++++++---- 2 files changed, 58 insertions(+), 21 deletions(-) diff --git a/docs/paper/references.bib b/docs/paper/references.bib index c94b97cab..3e63f1458 100644 --- a/docs/paper/references.bib +++ b/docs/paper/references.bib @@ -787,13 +787,13 @@ @article{even1976 doi = {10.1137/0205048} } -@article{chandra1977, - author = {Ashok K. Chandra and Philip M. Merlin}, - title = {Optimal Implementation of Conjunctive Queries in Relational Data Bases}, - journal = {Proceedings of the 9th Annual ACM Symposium on Theory of Computing (STOC)}, - pages = {77--90}, - year = {1977}, - doi = {10.1145/800105.803397} +@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, @@ -807,7 +807,7 @@ @article{gottlob2002 doi = {10.1006/jcss.2001.1809} } -@incollection{kolaitis1998, +@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)}, diff --git a/problemreductions-cli/src/commands/create.rs b/problemreductions-cli/src/commands/create.rs index d86458fea..086d09bd0 100644 --- a/problemreductions-cli/src/commands/create.rs +++ b/problemreductions-cli/src/commands/create.rs @@ -2124,6 +2124,7 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> { anyhow::anyhow!("ConjunctiveBooleanQuery requires --conjuncts-spec\n\n{usage}") })?; // Parse relations: "arity:t1,t2|t3,t4;arity:t5,t6,t7|t8,t9,t10" + // An empty tuple list (e.g., "2:") produces an empty relation. let relations: Vec = relations_str .split(';') .map(|rel_str| { @@ -2137,19 +2138,37 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> { .trim() .parse() .map_err(|e| anyhow::anyhow!("Invalid arity '{arity_str}': {e}"))?; - let tuples: Vec> = tuples_str - .split('|') - .map(|t| { - t.trim() - .split(',') - .map(|v| { - v.trim() - .parse::() - .map_err(|e| anyhow::anyhow!("Invalid tuple value: {e}")) - }) - .collect::>>() - }) - .collect::>>()?; + let tuples: Vec> = if tuples_str.trim().is_empty() { + Vec::new() + } else { + tuples_str + .split('|') + .filter(|t| !t.trim().is_empty()) + .map(|t| { + let tuple: Vec = t + .trim() + .split(',') + .map(|v| { + v.trim().parse::().map_err(|e| { + anyhow::anyhow!("Invalid tuple value: {e}") + }) + }) + .collect::>>()?; + if tuple.len() != arity { + bail!( + "Relation tuple has {} entries, expected arity {arity}", + tuple.len() + ); + } + for &val in &tuple { + if val >= domain_size { + bail!("Tuple value {val} >= domain-size {domain_size}"); + } + } + Ok(tuple) + }) + .collect::>>()? + }; Ok(CbqRelation { arity, tuples }) }) .collect::>>()?; @@ -2167,6 +2186,12 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> { let rel_idx: usize = idx_str.trim().parse().map_err(|e| { anyhow::anyhow!("Invalid relation index '{idx_str}': {e}") })?; + if rel_idx >= relations.len() { + bail!( + "Conjunct references relation {rel_idx}, but only {} relations exist", + relations.len() + ); + } let query_args: Vec = args_str .split(',') .map(|a| { @@ -2183,6 +2208,11 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> { let c: usize = rest.parse().map_err(|e| { anyhow::anyhow!("Invalid constant value '{rest}': {e}") })?; + if c >= domain_size { + bail!( + "Constant {c} >= domain-size {domain_size}" + ); + } Ok(QueryArg::Constant(c)) } else { Err(anyhow::anyhow!( @@ -2191,6 +2221,13 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> { } }) .collect::>>()?; + let expected_arity = relations[rel_idx].arity; + if query_args.len() != expected_arity { + bail!( + "Conjunct has {} args, but relation {rel_idx} has arity {expected_arity}", + query_args.len() + ); + } Ok((rel_idx, query_args)) }) .collect::>>()?; From 3ee4efc8a7754926bb6135466c9dc95010fa2fa7 Mon Sep 17 00:00:00 2001 From: zazabap Date: Thu, 19 Mar 2026 08:09:57 +0000 Subject: [PATCH 8/8] fix: add missing CBQ fields to empty_args test helper Co-Authored-By: Claude Opus 4.6 (1M context) --- problemreductions-cli/src/commands/create.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/problemreductions-cli/src/commands/create.rs b/problemreductions-cli/src/commands/create.rs index 086d09bd0..86aa0f090 100644 --- a/problemreductions-cli/src/commands/create.rs +++ b/problemreductions-cli/src/commands/create.rs @@ -3946,6 +3946,9 @@ mod tests { requirements: None, num_workers: None, num_groups: None, + domain_size: None, + relations: None, + conjuncts_spec: None, } }