diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 10b5cce8..7a75c7c1 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -164,6 +164,7 @@ "FlowShopScheduling": [Flow Shop Scheduling], "JobShopScheduling": [Job-Shop Scheduling], "GroupingBySwapping": [Grouping by Swapping], + "IntegerExpressionMembership": [Integer Expression Membership], "MinimumCutIntoBoundedSets": [Minimum Cut Into Bounded Sets], "MinimumDummyActivitiesPert": [Minimum Dummy Activities in PERT Networks], "MinimumSumMulticenter": [Minimum Sum Multicenter], @@ -6810,6 +6811,69 @@ A classical NP-complete problem from Garey and Johnson @garey1979[Ch.~3, p.~76], ] } +#{ + let x = load-model-example("IntegerExpressionMembership") + [ + #problem-def("IntegerExpressionMembership")[ + Given a recursive integer expression $e$ over union ($union$) and Minkowski sum ($+$) operations on singleton positive integers, and a target $K in NN^+$, determine whether $K in "eval"(e)$, where $"eval"("Atom"(n)) = \{n\}$, $"eval"(F union G) = "eval"(F) union "eval"(G)$, and $"eval"(F + G) = \{m + n : m in "eval"(F), n in "eval"(G)\}$. + ][ + Integer Expression Membership asks whether a specific integer is reachable by selecting one branch at each union node in a recursive expression tree. Each configuration assigns a binary choice (left or right) at every union node in depth-first order; with all unions resolved, the expression reduces to a chain of sums and atoms that evaluates to a single integer.#footnote[No algorithm improving on brute-force enumeration of all $2^u$ union-branch combinations (where $u$ is the number of union nodes) is known for the general case.] + + *Example.* Consider $e = (1 union 4) + (3 union 6) + (2 union 5)$ with $K = 12$. There are $u = 3$ union nodes, giving $2^3 = 8$ configurations. The reachable set is $\{6, 9, 12, 15\}$. Since $12 in \{6, 9, 12, 15\}$, the answer is YES. One witness: choose right ($4$), right ($6$), left ($2$) at the three union nodes, giving $4 + 6 + 2 = 12 = K$. + + #pred-commands( + "pred create --example " + problem-spec(x) + " -o iem.json", + "pred solve iem.json --solver brute-force", + "pred evaluate iem.json --config " + x.optimal_config.map(str).join(","), + ) + + #figure( + canvas(length: 0.7cm, { + import draw: * + // Draw expression tree: Sum( Sum( Union(1,4), Union(3,6) ), Union(2,5) ) + let node-r = 0.45 + let level-gap = 1.5 + let spread = 2.0 + // Root: Sum (level 0) + circle((0, 0), radius: node-r, name: "root", fill: rgb("#e8f0fe")) + content("root", text(8pt, $+$)) + // Left child: Sum (level 1) + circle((-spread, -level-gap), radius: node-r, name: "lsum", fill: rgb("#e8f0fe")) + content("lsum", text(8pt, $+$)) + line("root.south-west", "lsum.north", mark: (end: "straight")) + // Right child: Union (level 1) + circle((spread, -level-gap), radius: node-r, name: "ru", fill: rgb("#fce8e6")) + content("ru", text(8pt, $union$)) + line("root.south-east", "ru.north", mark: (end: "straight")) + // Left-Left: Union (level 2) + circle((-spread - 1.2, -2 * level-gap), radius: node-r, name: "llu", fill: rgb("#fce8e6")) + content("llu", text(8pt, $union$)) + line("lsum.south-west", "llu.north", mark: (end: "straight")) + // Left-Right: Union (level 2) + circle((-spread + 1.2, -2 * level-gap), radius: node-r, name: "lru", fill: rgb("#fce8e6")) + content("lru", text(8pt, $union$)) + line("lsum.south-east", "lru.north", mark: (end: "straight")) + // Leaves (level 3) + let leaf-spread = 0.7 + for (parent, vals, xoff) in ( + ("llu", (1, 4), -spread - 1.2), + ("lru", (3, 6), -spread + 1.2), + ("ru", (2, 5), spread), + ) { + circle((xoff - leaf-spread, -3 * level-gap), radius: node-r, name: parent + "l", fill: rgb("#e6f4ea")) + content(parent + "l", text(8pt, str(vals.at(0)))) + line(parent + ".south-west", (parent + "l") + ".north", mark: (end: "straight")) + circle((xoff + leaf-spread, -3 * level-gap), radius: node-r, name: parent + "r", fill: rgb("#e6f4ea")) + content(parent + "r", text(8pt, str(vals.at(1)))) + line(parent + ".south-east", (parent + "r") + ".north", mark: (end: "straight")) + } + }), + caption: [Expression tree $e = (1 union 4) + (3 union 6) + (2 union 5)$ with target $K = 12$. Blue nodes are sums ($+$), red nodes are unions ($union$), green leaves are atoms. Choosing right at the first two unions and left at the third yields $4 + 6 + 2 = 12$.], + ) + ] + ] +} + #{ let x = load-model-example("FeasibleBasisExtension") let A = x.instance.matrix diff --git a/problemreductions-cli/src/cli.rs b/problemreductions-cli/src/cli.rs index a80e073f..91efd062 100644 --- a/problemreductions-cli/src/cli.rs +++ b/problemreductions-cli/src/cli.rs @@ -319,6 +319,7 @@ Flags by problem type: D2CIF --arcs, --capacities, --source-1, --sink-1, --source-2, --sink-2, --requirement-1, --requirement-2 MinimumDummyActivitiesPert --arcs [--num-vertices] CBQ --domain-size, --relations, --conjuncts-spec + IntegerExpressionMembership --expression (JSON), --target ILP, CircuitSAT (via reduction only) Geometry graph variants (use slash notation, e.g., MIS/KingsSubgraph): @@ -758,6 +759,9 @@ pub struct CreateArgs { /// Target string for StringToStringCorrection (comma-separated symbol indices, e.g., "0,1,3,2") #[arg(long)] pub target_string: Option, + /// Expression tree for IntegerExpressionMembership (JSON, e.g., '{"Sum":[{"Atom":1},{"Atom":2}]}') + #[arg(long)] + pub expression: Option, /// Coefficient a for QuadraticDiophantineEquations (coefficient of x²) #[arg(long)] pub coeff_a: Option, diff --git a/problemreductions-cli/src/commands/create.rs b/problemreductions-cli/src/commands/create.rs index b24c3347..1e2a87a1 100644 --- a/problemreductions-cli/src/commands/create.rs +++ b/problemreductions-cli/src/commands/create.rs @@ -23,15 +23,15 @@ use problemreductions::models::graph::{ use problemreductions::models::misc::{ AdditionalKey, BinPacking, BoyceCoddNormalFormViolation, CapacityAssignment, CbqRelation, ConjunctiveBooleanQuery, ConsistencyOfDatabaseFrequencyTables, EnsembleComputation, - ExpectedRetrievalCost, FlowShopScheduling, FrequencyTable, GroupingBySwapping, - JobShopScheduling, KnownValue, KthLargestMTuple, LongestCommonSubsequence, - MinimumTardinessSequencing, MultiprocessorScheduling, PaintShop, PartiallyOrderedKnapsack, - ProductionPlanning, QueryArg, RectilinearPictureCompression, ResourceConstrainedScheduling, - SchedulingToMinimizeWeightedCompletionTime, SchedulingWithIndividualDeadlines, - SequencingToMinimizeMaximumCumulativeCost, SequencingToMinimizeWeightedCompletionTime, - SequencingToMinimizeWeightedTardiness, SequencingWithReleaseTimesAndDeadlines, - SequencingWithinIntervals, ShortestCommonSupersequence, StringToStringCorrection, SubsetSum, - SumOfSquaresPartition, ThreePartition, TimetableDesign, + ExpectedRetrievalCost, FlowShopScheduling, FrequencyTable, GroupingBySwapping, IntExpr, + IntegerExpressionMembership, JobShopScheduling, KnownValue, KthLargestMTuple, + LongestCommonSubsequence, MinimumTardinessSequencing, MultiprocessorScheduling, PaintShop, + PartiallyOrderedKnapsack, ProductionPlanning, QueryArg, RectilinearPictureCompression, + ResourceConstrainedScheduling, SchedulingToMinimizeWeightedCompletionTime, + SchedulingWithIndividualDeadlines, SequencingToMinimizeMaximumCumulativeCost, + SequencingToMinimizeWeightedCompletionTime, SequencingToMinimizeWeightedTardiness, + SequencingWithReleaseTimesAndDeadlines, SequencingWithinIntervals, ShortestCommonSupersequence, + StringToStringCorrection, SubsetSum, SumOfSquaresPartition, ThreePartition, TimetableDesign, }; use problemreductions::models::BiconnectivityAugmentation; use problemreductions::prelude::*; @@ -193,6 +193,7 @@ fn all_data_flags_empty(args: &CreateArgs) -> bool { && args.domain_size.is_none() && args.relations.is_none() && args.conjuncts_spec.is_none() + && args.expression.is_none() && args.deps.is_none() && args.query.is_none() && args.coeff_a.is_none() @@ -735,6 +736,9 @@ fn example_for(canonical: &str, graph_type: Option<&str>) -> &'static str { } "IntegerKnapsack" => "--sizes 3,4,5,2,7 --values 4,5,7,3,9 --capacity 15", "SubsetSum" => "--sizes 3,7,1,8,2,4 --target 11", + "IntegerExpressionMembership" => { + "--expression '{\"Sum\":[{\"Sum\":[{\"Union\":[{\"Atom\":1},{\"Atom\":4}]},{\"Union\":[{\"Atom\":3},{\"Atom\":6}]}]},{\"Union\":[{\"Atom\":2},{\"Atom\":5}]}]}' --target 12" + } "ThreePartition" => "--sizes 4,5,6,4,6,5 --bound 15", "KthLargestMTuple" => "--sets \"2,5,8;3,6;1,4,7\" --k 14 --bound 12", "QuadraticDiophantineEquations" => "--coeff-a 3 --coeff-b 5 --coeff-c 53", @@ -2401,6 +2405,34 @@ pub fn create(args: &CreateArgs, out: &OutputConfig) -> Result<()> { ) } + // IntegerExpressionMembership + "IntegerExpressionMembership" => { + let usage = "Usage: pred create IntegerExpressionMembership --expression '{\"Sum\":[{\"Atom\":1},{\"Atom\":2}]}' --target 3"; + let expr_str = args.expression.as_deref().ok_or_else(|| { + anyhow::anyhow!( + "IntegerExpressionMembership requires --expression and --target\n\n{usage}" + ) + })?; + let target = args.target.as_deref().ok_or_else(|| { + anyhow::anyhow!("IntegerExpressionMembership requires --target\n\n{usage}") + })?; + let target: u64 = target + .parse() + .context("IntegerExpressionMembership --target must be a positive integer")?; + if target == 0 { + anyhow::bail!("IntegerExpressionMembership --target must be > 0"); + } + let expr: IntExpr = serde_json::from_str(expr_str) + .context("IntegerExpressionMembership --expression must be valid JSON representing an IntExpr tree")?; + if !expr.all_atoms_positive() { + anyhow::bail!("IntegerExpressionMembership --expression must contain only positive integers (all Atom values > 0)"); + } + ( + ser(IntegerExpressionMembership::new(expr, target))?, + resolved_variant.clone(), + ) + } + // ThreePartition "ThreePartition" => { let sizes_str = args.sizes.as_deref().ok_or_else(|| { @@ -7804,6 +7836,7 @@ mod tests { storage: None, quantifiers: None, homologous_pairs: None, + expression: None, coeff_a: None, coeff_b: None, rhs: None, diff --git a/src/models/misc/integer_expression_membership.rs b/src/models/misc/integer_expression_membership.rs new file mode 100644 index 00000000..0e47f300 --- /dev/null +++ b/src/models/misc/integer_expression_membership.rs @@ -0,0 +1,281 @@ +//! Integer Expression Membership problem implementation. +//! +//! Given a recursive integer expression tree built from singleton positive integers +//! combined with union (∪) and Minkowski sum (+) operations, and a target integer K, +//! decide whether K belongs to the set represented by the expression. + +use crate::registry::{FieldInfo, ProblemSchemaEntry}; +use crate::traits::Problem; +use crate::types::Or; +use serde::{Deserialize, Serialize}; + +inventory::submit! { + ProblemSchemaEntry { + name: "IntegerExpressionMembership", + display_name: "Integer Expression Membership", + aliases: &[], + dimensions: &[], + module_path: module_path!(), + description: "Decide whether a target integer belongs to the set represented by an expression tree over union and Minkowski sum", + fields: &[ + FieldInfo { name: "expression", type_name: "IntExpr", description: "Recursive expression tree" }, + FieldInfo { name: "target", type_name: "u64", description: "Target integer K" }, + ], + } +} + +/// A recursive integer expression tree. +/// +/// Represents a set of positive integers built from: +/// - `Atom(n)`: the singleton set {n} +/// - `Union(f, g)`: set union F ∪ G +/// - `Sum(f, g)`: Minkowski sum {m + n : m ∈ F, n ∈ G} +#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)] +pub enum IntExpr { + /// Singleton set {n} for a positive integer n. + Atom(u64), + /// Set union: F ∪ G. + Union(Box, Box), + /// Minkowski sum: {m + n : m ∈ F, n ∈ G}. + Sum(Box, Box), +} + +impl IntExpr { + /// Returns true if all atoms in the expression are positive (> 0). + pub fn all_atoms_positive(&self) -> bool { + match self { + IntExpr::Atom(n) => *n > 0, + IntExpr::Union(l, r) | IntExpr::Sum(l, r) => { + l.all_atoms_positive() && r.all_atoms_positive() + } + } + } + + /// Count the total number of nodes in the expression tree. + pub fn size(&self) -> usize { + match self { + IntExpr::Atom(_) => 1, + IntExpr::Union(l, r) | IntExpr::Sum(l, r) => 1 + l.size() + r.size(), + } + } + + /// Count the number of Union nodes in the expression tree. + pub fn count_union_nodes(&self) -> usize { + match self { + IntExpr::Atom(_) => 0, + IntExpr::Union(l, r) => 1 + l.count_union_nodes() + r.count_union_nodes(), + IntExpr::Sum(l, r) => l.count_union_nodes() + r.count_union_nodes(), + } + } + + /// Count the number of Atom nodes in the expression tree. + pub fn count_atoms(&self) -> usize { + match self { + IntExpr::Atom(_) => 1, + IntExpr::Union(l, r) | IntExpr::Sum(l, r) => l.count_atoms() + r.count_atoms(), + } + } + + /// Compute the depth of the expression tree (0 for a single Atom). + pub fn depth(&self) -> usize { + match self { + IntExpr::Atom(_) => 0, + IntExpr::Union(l, r) | IntExpr::Sum(l, r) => 1 + l.depth().max(r.depth()), + } + } + + /// Evaluate the expression given union choices from config. + /// + /// `counter` tracks which union node we are at (DFS order). + /// Returns `Some(value)` if the config is valid, `None` otherwise. + fn evaluate_with_config(&self, config: &[usize], counter: &mut usize) -> Option { + match self { + IntExpr::Atom(n) => Some(*n), + IntExpr::Union(left, right) => { + let idx = *counter; + *counter += 1; + if idx >= config.len() { + return None; + } + match config[idx] { + 0 => left.evaluate_with_config(config, counter), + 1 => right.evaluate_with_config(config, counter), + _ => None, + } + } + IntExpr::Sum(left, right) => { + let l = left.evaluate_with_config(config, counter)?; + let r = right.evaluate_with_config(config, counter)?; + l.checked_add(r) + } + } + } +} + +/// The Integer Expression Membership problem. +/// +/// Given an integer expression `e` over union (∪) and Minkowski sum (+) +/// operations on singleton positive integers, and a target integer `K`, +/// decide whether `K ∈ eval(e)`. +/// +/// # Configuration +/// +/// Each Union node has a binary variable (0 = left, 1 = right). +/// A configuration assigns a branch choice to every Union node in DFS order. +/// The expression then collapses to a chain of Sum and Atom nodes, +/// evaluating to a single integer. +/// +/// # Example +/// +/// ``` +/// use problemreductions::models::misc::{IntegerExpressionMembership, IntExpr}; +/// use problemreductions::{Problem, Solver, BruteForce}; +/// +/// // e = (1 ∪ 4) + (3 ∪ 6) + (2 ∪ 5), target K = 12 +/// let expr = IntExpr::Sum( +/// Box::new(IntExpr::Sum( +/// Box::new(IntExpr::Union( +/// Box::new(IntExpr::Atom(1)), +/// Box::new(IntExpr::Atom(4)), +/// )), +/// Box::new(IntExpr::Union( +/// Box::new(IntExpr::Atom(3)), +/// Box::new(IntExpr::Atom(6)), +/// )), +/// )), +/// Box::new(IntExpr::Union( +/// Box::new(IntExpr::Atom(2)), +/// Box::new(IntExpr::Atom(5)), +/// )), +/// ); +/// let problem = IntegerExpressionMembership::new(expr, 12); +/// let solver = BruteForce::new(); +/// let solution = solver.find_witness(&problem); +/// assert!(solution.is_some()); +/// ``` +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct IntegerExpressionMembership { + /// The recursive expression tree. + expression: IntExpr, + /// The target integer K. + target: u64, +} + +impl IntegerExpressionMembership { + /// Create a new IntegerExpressionMembership instance. + /// + /// # Arguments + /// * `expression` - The integer expression tree + /// * `target` - The target integer K + pub fn new(expression: IntExpr, target: u64) -> Self { + assert!(target > 0, "target must be a positive integer (got 0)"); + assert!( + expression.all_atoms_positive(), + "all Atom values must be positive (> 0)" + ); + Self { expression, target } + } + + /// Returns a reference to the expression tree. + pub fn expression(&self) -> &IntExpr { + &self.expression + } + + /// Returns the target integer K. + pub fn target(&self) -> u64 { + self.target + } + + /// Returns the total number of nodes in the expression tree. + pub fn expression_size(&self) -> usize { + self.expression.size() + } + + /// Returns the number of Union nodes in the expression tree. + pub fn num_union_nodes(&self) -> usize { + self.expression.count_union_nodes() + } + + /// Returns the number of Atom nodes in the expression tree. + pub fn num_atoms(&self) -> usize { + self.expression.count_atoms() + } + + /// Returns the depth of the expression tree. + pub fn expression_depth(&self) -> usize { + self.expression.depth() + } + + /// Evaluate the expression for a given config and return the resulting integer. + /// + /// Returns `Some(value)` if the config is valid, `None` otherwise. + pub fn evaluate_config(&self, config: &[usize]) -> Option { + let mut counter = 0; + self.expression.evaluate_with_config(config, &mut counter) + } +} + +impl Problem for IntegerExpressionMembership { + const NAME: &'static str = "IntegerExpressionMembership"; + type Value = Or; + + fn dims(&self) -> Vec { + vec![2; self.num_union_nodes()] + } + + fn evaluate(&self, config: &[usize]) -> Or { + Or({ + if config.len() != self.num_union_nodes() { + return Or(false); + } + if config.iter().any(|&v| v >= 2) { + return Or(false); + } + match self.evaluate_config(config) { + Some(value) => value == self.target, + None => false, + } + }) + } + + fn variant() -> Vec<(&'static str, &'static str)> { + crate::variant_params![] + } +} + +crate::declare_variants! { + default IntegerExpressionMembership => "2^num_union_nodes", +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_model_example_specs() -> Vec { + // e = (1 ∪ 4) + (3 ∪ 6) + (2 ∪ 5), K = 12 + // 3 union nodes → 8 configs. Set = {6, 9, 12, 15}. + // Witness: choose right(4), right(6), left(2) → 4+6+2=12, config=[1,1,0] + let expr = IntExpr::Sum( + Box::new(IntExpr::Sum( + Box::new(IntExpr::Union( + Box::new(IntExpr::Atom(1)), + Box::new(IntExpr::Atom(4)), + )), + Box::new(IntExpr::Union( + Box::new(IntExpr::Atom(3)), + Box::new(IntExpr::Atom(6)), + )), + )), + Box::new(IntExpr::Union( + Box::new(IntExpr::Atom(2)), + Box::new(IntExpr::Atom(5)), + )), + ); + vec![crate::example_db::specs::ModelExampleSpec { + id: "integer_expression_membership", + instance: Box::new(IntegerExpressionMembership::new(expr, 12)), + optimal_config: vec![1, 1, 0], + optimal_value: serde_json::json!(true), + }] +} + +#[cfg(test)] +#[path = "../../unit_tests/models/misc/integer_expression_membership.rs"] +mod tests; diff --git a/src/models/misc/mod.rs b/src/models/misc/mod.rs index bfa891ea..e77eba84 100644 --- a/src/models/misc/mod.rs +++ b/src/models/misc/mod.rs @@ -9,6 +9,7 @@ //! - [`ConjunctiveQueryFoldability`]: Conjunctive Query Foldability //! - [`ExpectedRetrievalCost`]: Allocate records to circular sectors within a latency bound //! - [`Factoring`]: Integer factorization +//! - [`IntegerExpressionMembership`]: Membership in a set defined by an integer expression tree //! - [`FlowShopScheduling`]: Flow Shop Scheduling (meet deadline on m processors) //! - [`GroupingBySwapping`]: Group equal symbols into contiguous blocks by adjacent swaps //! - [`JobShopScheduling`]: Minimize makespan with per-job processor routes @@ -75,6 +76,7 @@ pub(crate) mod expected_retrieval_cost; pub(crate) mod factoring; mod flow_shop_scheduling; mod grouping_by_swapping; +pub(crate) mod integer_expression_membership; mod job_shop_scheduling; mod knapsack; mod kth_largest_m_tuple; @@ -119,6 +121,7 @@ pub use expected_retrieval_cost::ExpectedRetrievalCost; pub use factoring::Factoring; pub use flow_shop_scheduling::FlowShopScheduling; pub use grouping_by_swapping::GroupingBySwapping; +pub use integer_expression_membership::{IntExpr, IntegerExpressionMembership}; pub use job_shop_scheduling::JobShopScheduling; pub use knapsack::Knapsack; pub use kth_largest_m_tuple::KthLargestMTuple; @@ -188,6 +191,7 @@ pub(crate) fn canonical_model_example_specs() -> Vec IntExpr { + IntExpr::Sum( + Box::new(IntExpr::Sum( + Box::new(IntExpr::Union( + Box::new(IntExpr::Atom(1)), + Box::new(IntExpr::Atom(4)), + )), + Box::new(IntExpr::Union( + Box::new(IntExpr::Atom(3)), + Box::new(IntExpr::Atom(6)), + )), + )), + Box::new(IntExpr::Union( + Box::new(IntExpr::Atom(2)), + Box::new(IntExpr::Atom(5)), + )), + ) +} + +#[test] +fn test_integer_expression_membership_creation() { + let expr = example_expr(); + let problem = IntegerExpressionMembership::new(expr.clone(), 12); + assert_eq!(problem.target(), 12); + assert_eq!(problem.num_union_nodes(), 3); + assert_eq!(problem.num_atoms(), 6); + assert_eq!(problem.expression_size(), 11); // 6 atoms + 3 unions + 2 sums + assert_eq!(problem.expression_depth(), 3); + assert_eq!(problem.dims(), vec![2, 2, 2]); + assert_eq!( + ::NAME, + "IntegerExpressionMembership" + ); + assert_eq!(::variant(), vec![]); +} + +#[test] +fn test_integer_expression_membership_evaluate_satisfying() { + let problem = IntegerExpressionMembership::new(example_expr(), 12); + // config [1,1,0]: choose 4, 6, 2 → 4+6+2=12 + assert!(problem.evaluate(&[1, 1, 0])); + // config [0,1,1]: choose 1, 6, 5 → 1+6+5=12 + assert!(problem.evaluate(&[0, 1, 1])); +} + +#[test] +fn test_integer_expression_membership_evaluate_unsatisfying() { + let problem = IntegerExpressionMembership::new(example_expr(), 12); + // config [0,0,0]: choose 1, 3, 2 → 1+3+2=6 ≠ 12 + assert!(!problem.evaluate(&[0, 0, 0])); + // config [1,0,0]: choose 4, 3, 2 → 4+3+2=9 ≠ 12 + assert!(!problem.evaluate(&[1, 0, 0])); + // config [1,1,1]: choose 4, 6, 5 → 4+6+5=15 ≠ 12 + assert!(!problem.evaluate(&[1, 1, 1])); +} + +#[test] +fn test_integer_expression_membership_evaluate_wrong_config() { + let problem = IntegerExpressionMembership::new(example_expr(), 12); + // Wrong length + assert!(!problem.evaluate(&[0, 0])); + assert!(!problem.evaluate(&[0, 0, 0, 0])); + // Invalid value + assert!(!problem.evaluate(&[2, 0, 0])); +} + +#[test] +fn test_integer_expression_membership_brute_force() { + let problem = IntegerExpressionMembership::new(example_expr(), 12); + let solver = BruteForce::new(); + let solution = solver + .find_witness(&problem) + .expect("should find a solution"); + assert!(problem.evaluate(&solution)); +} + +#[test] +fn test_integer_expression_membership_brute_force_all() { + let problem = IntegerExpressionMembership::new(example_expr(), 12); + let solver = BruteForce::new(); + let solutions = solver.find_all_witnesses(&problem); + // K=12 can be reached by [0,1,1] (1+6+5), [1,0,1] (4+3+5), [1,1,0] (4+6+2) + assert_eq!(solutions.len(), 3); + for sol in &solutions { + assert!(problem.evaluate(sol)); + } +} + +#[test] +fn test_integer_expression_membership_unsatisfiable() { + // Target 100 is unreachable from {1,4}+{3,6}+{2,5} (max is 15) + let problem = IntegerExpressionMembership::new(example_expr(), 100); + let solver = BruteForce::new(); + assert!(solver.find_witness(&problem).is_none()); +} + +#[test] +fn test_integer_expression_membership_single_atom() { + let expr = IntExpr::Atom(42); + let problem = IntegerExpressionMembership::new(expr, 42); + assert_eq!(problem.num_union_nodes(), 0); + assert_eq!(problem.dims(), Vec::::new()); + assert!(problem.evaluate(&[])); // empty config, atom == target +} + +#[test] +fn test_integer_expression_membership_single_atom_miss() { + let expr = IntExpr::Atom(42); + let problem = IntegerExpressionMembership::new(expr, 7); + assert!(!problem.evaluate(&[])); // 42 ≠ 7 +} + +#[test] +fn test_integer_expression_membership_simple_union() { + // (3 ∪ 7), target = 7 + let expr = IntExpr::Union(Box::new(IntExpr::Atom(3)), Box::new(IntExpr::Atom(7))); + let problem = IntegerExpressionMembership::new(expr, 7); + assert_eq!(problem.num_union_nodes(), 1); + assert_eq!(problem.dims(), vec![2]); + assert!(!problem.evaluate(&[0])); // 3 ≠ 7 + assert!(problem.evaluate(&[1])); // 7 == 7 +} + +#[test] +fn test_integer_expression_membership_simple_sum() { + // Atom(3) + Atom(5), target = 8 + let expr = IntExpr::Sum(Box::new(IntExpr::Atom(3)), Box::new(IntExpr::Atom(5))); + let problem = IntegerExpressionMembership::new(expr, 8); + assert_eq!(problem.num_union_nodes(), 0); + assert!(problem.evaluate(&[])); // 3+5=8 +} + +#[test] +fn test_integer_expression_membership_serialization() { + let expr = IntExpr::Union(Box::new(IntExpr::Atom(1)), Box::new(IntExpr::Atom(4))); + let problem = IntegerExpressionMembership::new(expr, 4); + let json = serde_json::to_value(&problem).unwrap(); + let restored: IntegerExpressionMembership = serde_json::from_value(json).unwrap(); + assert_eq!(restored.target(), 4); + assert_eq!(restored.num_union_nodes(), 1); + assert!(restored.evaluate(&[1])); // choose 4 +} + +#[test] +fn test_integer_expression_membership_evaluate_config() { + let problem = IntegerExpressionMembership::new(example_expr(), 12); + assert_eq!(problem.evaluate_config(&[1, 1, 0]), Some(12)); // 4+6+2 + assert_eq!(problem.evaluate_config(&[0, 0, 0]), Some(6)); // 1+3+2 + assert_eq!(problem.evaluate_config(&[1, 1, 1]), Some(15)); // 4+6+5 + assert_eq!(problem.evaluate_config(&[0, 0, 1]), Some(9)); // 1+3+5 +} + +#[test] +fn test_integer_expression_membership_paper_example() { + // e = (1 ∪ 4) + (3 ∪ 6) + (2 ∪ 5), K = 12 + // Set = {6, 9, 12, 15} + // Witness: config [1, 1, 0] → 4+6+2 = 12 + let problem = IntegerExpressionMembership::new(example_expr(), 12); + + // Verify the claimed witness + assert_eq!(problem.evaluate_config(&[1, 1, 0]), Some(12)); + assert!(problem.evaluate(&[1, 1, 0])); + + // Verify all 8 configs produce the set {6, 9, 12, 15} + let mut values: Vec = Vec::new(); + for c0 in 0..2 { + for c1 in 0..2 { + for c2 in 0..2 { + values.push(problem.evaluate_config(&[c0, c1, c2]).unwrap()); + } + } + } + values.sort(); + values.dedup(); + assert_eq!(values, vec![6, 9, 12, 15]); + + // Brute force confirms 3 satisfying configs for K=12: + // [0,1,1] (1+6+5), [1,0,1] (4+3+5), [1,1,0] (4+6+2) + let solver = BruteForce::new(); + let solutions = solver.find_all_witnesses(&problem); + assert_eq!(solutions.len(), 3); +} + +#[test] +fn test_integer_expression_membership_nested_unions() { + // ((1 ∪ 2) ∪ 3), target = 2 + let expr = IntExpr::Union( + Box::new(IntExpr::Union( + Box::new(IntExpr::Atom(1)), + Box::new(IntExpr::Atom(2)), + )), + Box::new(IntExpr::Atom(3)), + ); + let problem = IntegerExpressionMembership::new(expr, 2); + assert_eq!(problem.num_union_nodes(), 2); + // DFS order: outer union (idx 0), inner union (idx 1) + // [0, 0] → left of outer → left of inner → 1 + // [0, 1] → left of outer → right of inner → 2 + // [1, _] → right of outer → 3 (inner union not visited) + assert!(!problem.evaluate(&[0, 0])); // 1 ≠ 2 + assert!(problem.evaluate(&[0, 1])); // 2 == 2 + assert!(!problem.evaluate(&[1, 0])); // 3 ≠ 2 + assert!(!problem.evaluate(&[1, 1])); // 3 ≠ 2 +} + +#[test] +fn test_integer_expression_membership_overflow_safe() { + // Two atoms that sum to > u64::MAX should evaluate to Or(false), not panic. + let expr = IntExpr::Sum( + Box::new(IntExpr::Atom(u64::MAX)), + Box::new(IntExpr::Atom(1)), + ); + let problem = IntegerExpressionMembership::new(expr, 42); + // The only config is [] (no union nodes). The sum overflows → None → Or(false). + assert!(!problem.evaluate(&[])); +} + +#[test] +#[should_panic(expected = "all Atom values must be positive")] +fn test_integer_expression_membership_zero_atom_rejected() { + let expr = IntExpr::Atom(0); + IntegerExpressionMembership::new(expr, 1); +} + +#[test] +#[should_panic(expected = "target must be a positive integer")] +fn test_integer_expression_membership_zero_target_rejected() { + let expr = IntExpr::Atom(1); + IntegerExpressionMembership::new(expr, 0); +}