problemreductions/models/misc/
integer_expression_membership.rs

1//! Integer Expression Membership problem implementation.
2//!
3//! Given a recursive integer expression tree built from singleton positive integers
4//! combined with union (∪) and Minkowski sum (+) operations, and a target integer K,
5//! decide whether K belongs to the set represented by the expression.
6
7use crate::registry::{FieldInfo, ProblemSchemaEntry};
8use crate::traits::Problem;
9use crate::types::Or;
10use serde::{Deserialize, Serialize};
11
12inventory::submit! {
13    ProblemSchemaEntry {
14        name: "IntegerExpressionMembership",
15        display_name: "Integer Expression Membership",
16        aliases: &[],
17        dimensions: &[],
18        module_path: module_path!(),
19        description: "Decide whether a target integer belongs to the set represented by an expression tree over union and Minkowski sum",
20        fields: &[
21            FieldInfo { name: "expression", type_name: "IntExpr", description: "Recursive expression tree" },
22            FieldInfo { name: "target", type_name: "u64", description: "Target integer K" },
23        ],
24    }
25}
26
27/// A recursive integer expression tree.
28///
29/// Represents a set of positive integers built from:
30/// - `Atom(n)`: the singleton set {n}
31/// - `Union(f, g)`: set union F ∪ G
32/// - `Sum(f, g)`: Minkowski sum {m + n : m ∈ F, n ∈ G}
33#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
34pub enum IntExpr {
35    /// Singleton set {n} for a positive integer n.
36    Atom(u64),
37    /// Set union: F ∪ G.
38    Union(Box<IntExpr>, Box<IntExpr>),
39    /// Minkowski sum: {m + n : m ∈ F, n ∈ G}.
40    Sum(Box<IntExpr>, Box<IntExpr>),
41}
42
43impl IntExpr {
44    /// Returns true if all atoms in the expression are positive (> 0).
45    pub fn all_atoms_positive(&self) -> bool {
46        match self {
47            IntExpr::Atom(n) => *n > 0,
48            IntExpr::Union(l, r) | IntExpr::Sum(l, r) => {
49                l.all_atoms_positive() && r.all_atoms_positive()
50            }
51        }
52    }
53
54    /// Count the total number of nodes in the expression tree.
55    pub fn size(&self) -> usize {
56        match self {
57            IntExpr::Atom(_) => 1,
58            IntExpr::Union(l, r) | IntExpr::Sum(l, r) => 1 + l.size() + r.size(),
59        }
60    }
61
62    /// Count the number of Union nodes in the expression tree.
63    pub fn count_union_nodes(&self) -> usize {
64        match self {
65            IntExpr::Atom(_) => 0,
66            IntExpr::Union(l, r) => 1 + l.count_union_nodes() + r.count_union_nodes(),
67            IntExpr::Sum(l, r) => l.count_union_nodes() + r.count_union_nodes(),
68        }
69    }
70
71    /// Count the number of Atom nodes in the expression tree.
72    pub fn count_atoms(&self) -> usize {
73        match self {
74            IntExpr::Atom(_) => 1,
75            IntExpr::Union(l, r) | IntExpr::Sum(l, r) => l.count_atoms() + r.count_atoms(),
76        }
77    }
78
79    /// Compute the depth of the expression tree (0 for a single Atom).
80    pub fn depth(&self) -> usize {
81        match self {
82            IntExpr::Atom(_) => 0,
83            IntExpr::Union(l, r) | IntExpr::Sum(l, r) => 1 + l.depth().max(r.depth()),
84        }
85    }
86
87    /// Evaluate the expression given union choices from config.
88    ///
89    /// `counter` tracks which union node we are at (DFS order).
90    /// Returns `Some(value)` if the config is valid, `None` otherwise.
91    fn evaluate_with_config(&self, config: &[usize], counter: &mut usize) -> Option<u64> {
92        match self {
93            IntExpr::Atom(n) => Some(*n),
94            IntExpr::Union(left, right) => {
95                let idx = *counter;
96                *counter += 1;
97                if idx >= config.len() {
98                    return None;
99                }
100                match config[idx] {
101                    0 => left.evaluate_with_config(config, counter),
102                    1 => right.evaluate_with_config(config, counter),
103                    _ => None,
104                }
105            }
106            IntExpr::Sum(left, right) => {
107                let l = left.evaluate_with_config(config, counter)?;
108                let r = right.evaluate_with_config(config, counter)?;
109                l.checked_add(r)
110            }
111        }
112    }
113}
114
115/// The Integer Expression Membership problem.
116///
117/// Given an integer expression `e` over union (∪) and Minkowski sum (+)
118/// operations on singleton positive integers, and a target integer `K`,
119/// decide whether `K ∈ eval(e)`.
120///
121/// # Configuration
122///
123/// Each Union node has a binary variable (0 = left, 1 = right).
124/// A configuration assigns a branch choice to every Union node in DFS order.
125/// The expression then collapses to a chain of Sum and Atom nodes,
126/// evaluating to a single integer.
127///
128/// # Example
129///
130/// ```
131/// use problemreductions::models::misc::{IntegerExpressionMembership, IntExpr};
132/// use problemreductions::{Problem, Solver, BruteForce};
133///
134/// // e = (1 ∪ 4) + (3 ∪ 6) + (2 ∪ 5), target K = 12
135/// let expr = IntExpr::Sum(
136///     Box::new(IntExpr::Sum(
137///         Box::new(IntExpr::Union(
138///             Box::new(IntExpr::Atom(1)),
139///             Box::new(IntExpr::Atom(4)),
140///         )),
141///         Box::new(IntExpr::Union(
142///             Box::new(IntExpr::Atom(3)),
143///             Box::new(IntExpr::Atom(6)),
144///         )),
145///     )),
146///     Box::new(IntExpr::Union(
147///         Box::new(IntExpr::Atom(2)),
148///         Box::new(IntExpr::Atom(5)),
149///     )),
150/// );
151/// let problem = IntegerExpressionMembership::new(expr, 12);
152/// let solver = BruteForce::new();
153/// let solution = solver.find_witness(&problem);
154/// assert!(solution.is_some());
155/// ```
156#[derive(Debug, Clone, Serialize, Deserialize)]
157pub struct IntegerExpressionMembership {
158    /// The recursive expression tree.
159    expression: IntExpr,
160    /// The target integer K.
161    target: u64,
162}
163
164impl IntegerExpressionMembership {
165    /// Create a new IntegerExpressionMembership instance.
166    ///
167    /// # Arguments
168    /// * `expression` - The integer expression tree
169    /// * `target` - The target integer K
170    pub fn new(expression: IntExpr, target: u64) -> Self {
171        assert!(target > 0, "target must be a positive integer (got 0)");
172        assert!(
173            expression.all_atoms_positive(),
174            "all Atom values must be positive (> 0)"
175        );
176        Self { expression, target }
177    }
178
179    /// Returns a reference to the expression tree.
180    pub fn expression(&self) -> &IntExpr {
181        &self.expression
182    }
183
184    /// Returns the target integer K.
185    pub fn target(&self) -> u64 {
186        self.target
187    }
188
189    /// Returns the total number of nodes in the expression tree.
190    pub fn expression_size(&self) -> usize {
191        self.expression.size()
192    }
193
194    /// Returns the number of Union nodes in the expression tree.
195    pub fn num_union_nodes(&self) -> usize {
196        self.expression.count_union_nodes()
197    }
198
199    /// Returns the number of Atom nodes in the expression tree.
200    pub fn num_atoms(&self) -> usize {
201        self.expression.count_atoms()
202    }
203
204    /// Returns the depth of the expression tree.
205    pub fn expression_depth(&self) -> usize {
206        self.expression.depth()
207    }
208
209    /// Evaluate the expression for a given config and return the resulting integer.
210    ///
211    /// Returns `Some(value)` if the config is valid, `None` otherwise.
212    pub fn evaluate_config(&self, config: &[usize]) -> Option<u64> {
213        let mut counter = 0;
214        self.expression.evaluate_with_config(config, &mut counter)
215    }
216}
217
218impl Problem for IntegerExpressionMembership {
219    const NAME: &'static str = "IntegerExpressionMembership";
220    type Value = Or;
221
222    fn dims(&self) -> Vec<usize> {
223        vec![2; self.num_union_nodes()]
224    }
225
226    fn evaluate(&self, config: &[usize]) -> Or {
227        Or({
228            if config.len() != self.num_union_nodes() {
229                return Or(false);
230            }
231            if config.iter().any(|&v| v >= 2) {
232                return Or(false);
233            }
234            match self.evaluate_config(config) {
235                Some(value) => value == self.target,
236                None => false,
237            }
238        })
239    }
240
241    fn variant() -> Vec<(&'static str, &'static str)> {
242        crate::variant_params![]
243    }
244}
245
246crate::declare_variants! {
247    default IntegerExpressionMembership => "2^num_union_nodes",
248}
249
250#[cfg(feature = "example-db")]
251pub(crate) fn canonical_model_example_specs() -> Vec<crate::example_db::specs::ModelExampleSpec> {
252    // e = (1 ∪ 4) + (3 ∪ 6) + (2 ∪ 5), K = 12
253    // 3 union nodes → 8 configs. Set = {6, 9, 12, 15}.
254    // Witness: choose right(4), right(6), left(2) → 4+6+2=12, config=[1,1,0]
255    let expr = IntExpr::Sum(
256        Box::new(IntExpr::Sum(
257            Box::new(IntExpr::Union(
258                Box::new(IntExpr::Atom(1)),
259                Box::new(IntExpr::Atom(4)),
260            )),
261            Box::new(IntExpr::Union(
262                Box::new(IntExpr::Atom(3)),
263                Box::new(IntExpr::Atom(6)),
264            )),
265        )),
266        Box::new(IntExpr::Union(
267            Box::new(IntExpr::Atom(2)),
268            Box::new(IntExpr::Atom(5)),
269        )),
270    );
271    vec![crate::example_db::specs::ModelExampleSpec {
272        id: "integer_expression_membership",
273        instance: Box::new(IntegerExpressionMembership::new(expr, 12)),
274        optimal_config: vec![1, 1, 0],
275        optimal_value: serde_json::json!(true),
276    }]
277}
278
279#[cfg(test)]
280#[path = "../../unit_tests/models/misc/integer_expression_membership.rs"]
281mod tests;
problemreductions/models/misc/integer_expression_membership.rs

problemreductions/models/misc/
integer_expression_membership.rs
