diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index a37708de..c4954975 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -130,6 +130,7 @@ "SumOfSquaresPartition": [Sum of Squares Partition], "SequencingWithinIntervals": [Sequencing Within Intervals], "DirectedTwoCommodityIntegralFlow": [Directed Two-Commodity Integral Flow], + "ConjunctiveBooleanQuery": [Conjunctive Boolean Query], "RectilinearPictureCompression": [Rectilinear Picture Compression], "StringToStringCorrection": [String-to-String Correction], ) @@ -3268,6 +3269,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 @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.] + + *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. + ] + ] +} + #{ let x = load-model-example("ConsecutiveOnesSubmatrix") let A = x.instance.matrix diff --git a/docs/paper/references.bib b/docs/paper/references.bib index da6f3e5e..995f7573 100644 --- a/docs/paper/references.bib +++ b/docs/paper/references.bib @@ -809,6 +809,35 @@ @article{even1976 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}, diff --git a/problemreductions-cli/src/cli.rs b/problemreductions-cli/src/cli.rs index 39ae83f2..d781a560 100644 --- a/problemreductions-cli/src/cli.rs +++ b/problemreductions-cli/src/cli.rs @@ -269,6 +269,7 @@ Flags by problem type: SCS --strings, --bound [--alphabet-size] StringToStringCorrection --source-string, --target-string, --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): @@ -518,6 +519,15 @@ pub struct CreateArgs { /// Alphabet size for LCS, SCS, or StringToStringCorrection (optional; inferred from the input strings 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, /// Functional dependencies (semicolon-separated, each dep is lhs>rhs with comma-separated indices, e.g., "0,1>2,3;2,3>0,1") #[arg(long)] pub deps: Option, diff --git a/problemreductions-cli/src/commands/create.rs b/problemreductions-cli/src/commands/create.rs index def73462..0f701dba 100644 --- a/problemreductions-cli/src/commands/create.rs +++ b/problemreductions-cli/src/commands/create.rs @@ -13,10 +13,11 @@ use problemreductions::models::graph::{ MinimumMultiwayCut, MultipleChoiceBranching, SteinerTree, StrongConnectivityAugmentation, }; use problemreductions::models::misc::{ - BinPacking, FlowShopScheduling, LongestCommonSubsequence, MinimumTardinessSequencing, - MultiprocessorScheduling, PaintShop, PartiallyOrderedKnapsack, RectilinearPictureCompression, - SequencingWithReleaseTimesAndDeadlines, SequencingWithinIntervals, - ShortestCommonSupersequence, StringToStringCorrection, SubsetSum, SumOfSquaresPartition, + BinPacking, CbqRelation, ConjunctiveBooleanQuery, FlowShopScheduling, LongestCommonSubsequence, + MinimumTardinessSequencing, MultiprocessorScheduling, PaintShop, PartiallyOrderedKnapsack, + QueryArg, RectilinearPictureCompression, SequencingWithReleaseTimesAndDeadlines, + SequencingWithinIntervals, ShortestCommonSupersequence, StringToStringCorrection, SubsetSum, + SumOfSquaresPartition, }; use problemreductions::models::BiconnectivityAugmentation; use problemreductions::prelude::*; @@ -110,6 +111,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() && args.deps.is_none() && args.query.is_none() } @@ -356,6 +360,9 @@ fn example_for(canonical: &str, graph_type: Option<&str>) -> &'static str { "--num-attributes 6 --dependencies \"0,1>2;0,2>3;1,3>4;2,4>5\" --k 2" } "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\"" + } "StringToStringCorrection" => { "--source-string \"0,1,2,3,1,0\" --target-string \"0,1,3,2,1\" --bound 2" } @@ -2106,6 +2113,137 @@ 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" + // An empty tuple list (e.g., "2:") produces an empty relation. + 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> = 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::>>()?; + // 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}") + })?; + 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| { + 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}") + })?; + if c >= domain_size { + bail!( + "Constant {c} >= domain-size {domain_size}" + ); + } + Ok(QueryArg::Constant(c)) + } else { + Err(anyhow::anyhow!( + "Invalid query arg '{a}': expected vN (variable) or cN (constant)" + )) + } + }) + .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::>>()?; + ( + ser(ConjunctiveBooleanQuery::new( + domain_size, + relations, + num_vars_inferred, + conjuncts, + ))?, + resolved_variant.clone(), + ) + } + // PartiallyOrderedKnapsack "PartiallyOrderedKnapsack" => { let sizes_str = args.sizes.as_deref().ok_or_else(|| { @@ -3858,6 +3996,9 @@ mod tests { requirements: None, num_workers: None, num_groups: None, + domain_size: None, + relations: None, + conjuncts_spec: None, } } diff --git a/src/lib.rs b/src/lib.rs index ac2c767c..b85e6061 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -59,9 +59,9 @@ pub mod prelude { UndirectedTwoCommodityIntegralFlow, }; pub use crate::models::misc::{ - BinPacking, Factoring, FlowShopScheduling, Knapsack, LongestCommonSubsequence, - MinimumTardinessSequencing, MultiprocessorScheduling, PaintShop, - RectilinearPictureCompression, SequencingWithReleaseTimesAndDeadlines, + BinPacking, CbqRelation, ConjunctiveBooleanQuery, Factoring, FlowShopScheduling, Knapsack, + LongestCommonSubsequence, MinimumTardinessSequencing, MultiprocessorScheduling, PaintShop, + QueryArg, RectilinearPictureCompression, SequencingWithReleaseTimesAndDeadlines, SequencingWithinIntervals, ShortestCommonSupersequence, StaffScheduling, StringToStringCorrection, SubsetSum, SumOfSquaresPartition, }; diff --git a/src/models/misc/conjunctive_boolean_query.rs b/src/models/misc/conjunctive_boolean_query.rs new file mode 100644 index 00000000..9dd0631f --- /dev/null +++ b/src/models/misc/conjunctive_boolean_query.rs @@ -0,0 +1,269 @@ +//! 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, PartialEq, 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, PartialEq, 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, PartialEq, 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", + // D={0..5}, 2 relations (binary R0, ternary R1), 3 atoms, 2 variables. + // Satisfying assignment: y0=0, y1=1. + instance: Box::new(ConjunctiveBooleanQuery::new( + 6, + 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]], + }, + ], + 2, + 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), + ], + ), + ], + )), + optimal_config: vec![0, 1], + optimal_value: serde_json::json!(true), + }] +} + +#[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 ad6aef19..bc45dbda 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) @@ -20,6 +21,7 @@ //! - [`SumOfSquaresPartition`]: Partition integers into K groups minimizing sum of squared group sums mod bin_packing; +pub(crate) mod conjunctive_boolean_query; pub(crate) mod factoring; mod flow_shop_scheduling; mod knapsack; @@ -39,6 +41,7 @@ mod subset_sum; pub(crate) mod sum_of_squares_partition; 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; @@ -60,6 +63,7 @@ pub use sum_of_squares_partition::SumOfSquaresPartition; #[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(longest_common_subsequence::canonical_model_example_specs()); specs.extend(multiprocessor_scheduling::canonical_model_example_specs()); diff --git a/src/models/mod.rs b/src/models/mod.rs index c6828711..7bc3d196 100644 --- a/src/models/mod.rs +++ b/src/models/mod.rs @@ -26,9 +26,9 @@ pub use graph::{ }; pub use misc::PartiallyOrderedKnapsack; pub use misc::{ - BinPacking, Factoring, FlowShopScheduling, Knapsack, LongestCommonSubsequence, - MinimumTardinessSequencing, MultiprocessorScheduling, PaintShop, - PrecedenceConstrainedScheduling, RectilinearPictureCompression, + BinPacking, CbqRelation, ConjunctiveBooleanQuery, Factoring, FlowShopScheduling, Knapsack, + LongestCommonSubsequence, MinimumTardinessSequencing, MultiprocessorScheduling, PaintShop, + PrecedenceConstrainedScheduling, QueryArg, RectilinearPictureCompression, SequencingWithReleaseTimesAndDeadlines, SequencingWithinIntervals, ShortestCommonSupersequence, StaffScheduling, StringToStringCorrection, SubsetSum, SumOfSquaresPartition, }; 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 00000000..3da1f3cf --- /dev/null +++ b/src/unit_tests/models/misc/conjunctive_boolean_query.rs @@ -0,0 +1,137 @@ +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, problem); +} + +#[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]); +} diff --git a/src/unit_tests/models/misc/partially_ordered_knapsack.rs b/src/unit_tests/models/misc/partially_ordered_knapsack.rs index 8a7f5364..013dff32 100644 --- a/src/unit_tests/models/misc/partially_ordered_knapsack.rs +++ b/src/unit_tests/models/misc/partially_ordered_knapsack.rs @@ -188,7 +188,12 @@ fn test_partially_ordered_knapsack_invalid_precedence() { #[test] #[should_panic(expected = "precedences contain a cycle")] fn test_partially_ordered_knapsack_cycle() { - PartiallyOrderedKnapsack::new(vec![1, 2, 3], vec![1, 2, 3], vec![(0, 1), (1, 2), (2, 0)], 10); + PartiallyOrderedKnapsack::new( + vec![1, 2, 3], + vec![1, 2, 3], + vec![(0, 1), (1, 2), (2, 0)], + 10, + ); } #[test]