problemreductions/rules/
consistencyofdatabasefrequencytables_ilp.rs

1//! Reduction from ConsistencyOfDatabaseFrequencyTables to ILP.
2//!
3//! The reduction uses a binary one-hot encoding:
4//! - `y_{v,a,x}` is 1 iff object `v` receives value `x` for attribute `a`
5//! - `z_{t,v,x,y}` is 1 iff, for table `t`, object `v` realizes cell `(x, y)`
6//!
7//! The pair-count equalities are linearized with standard McCormick constraints.
8
9use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP};
10use crate::models::misc::ConsistencyOfDatabaseFrequencyTables;
11use crate::reduction;
12use crate::rules::ilp_helpers::mccormick_product;
13use crate::rules::traits::{ReduceTo, ReductionResult};
14
15/// Result of reducing ConsistencyOfDatabaseFrequencyTables to ILP.
16#[derive(Debug, Clone)]
17pub struct ReductionCDFTToILP {
18    target: ILP<bool>,
19    source: ConsistencyOfDatabaseFrequencyTables,
20}
21
22impl ReductionCDFTToILP {
23    fn assignment_block_size(&self) -> usize {
24        self.source.attribute_domains().iter().sum()
25    }
26
27    fn attribute_offset(&self, attribute: usize) -> usize {
28        self.source.attribute_domains()[..attribute].iter().sum()
29    }
30
31    fn assignment_var_index(&self, object: usize, attribute: usize, value: usize) -> usize {
32        object * self.assignment_block_size() + self.attribute_offset(attribute) + value
33    }
34
35    fn auxiliary_block_start(&self, table_index: usize) -> usize {
36        self.source.num_objects() * self.assignment_block_size()
37            + self.source.frequency_tables()[..table_index]
38                .iter()
39                .map(|table| self.source.num_objects() * table.num_cells())
40                .sum::<usize>()
41    }
42
43    fn auxiliary_var_index(
44        &self,
45        table_index: usize,
46        object: usize,
47        value_a: usize,
48        value_b: usize,
49    ) -> usize {
50        let table = &self.source.frequency_tables()[table_index];
51        let cols = self.source.attribute_domains()[table.attribute_b()];
52        self.auxiliary_block_start(table_index)
53            + object * table.num_cells()
54            + value_a * cols
55            + value_b
56    }
57
58    /// Encode a satisfying source assignment as a concrete ILP variable vector.
59    #[cfg_attr(not(test), allow(dead_code))]
60    pub(crate) fn encode_source_solution(&self, source_solution: &[usize]) -> Vec<i64> {
61        let mut target_solution = vec![0_i64; self.target.num_vars()];
62        let num_attributes = self.source.num_attributes();
63
64        for object in 0..self.source.num_objects() {
65            for attribute in 0..num_attributes {
66                let source_index = object * num_attributes + attribute;
67                let value = source_solution[source_index];
68                let var = self.assignment_var_index(object, attribute, value);
69                target_solution[var] = 1;
70            }
71        }
72
73        for (table_index, table) in self.source.frequency_tables().iter().enumerate() {
74            for object in 0..self.source.num_objects() {
75                let value_a = source_solution[object * num_attributes + table.attribute_a()];
76                let value_b = source_solution[object * num_attributes + table.attribute_b()];
77                let var = self.auxiliary_var_index(table_index, object, value_a, value_b);
78                target_solution[var] = 1;
79            }
80        }
81
82        target_solution
83    }
84}
85
86impl ReductionResult for ReductionCDFTToILP {
87    type Source = ConsistencyOfDatabaseFrequencyTables;
88    type Target = ILP<bool>;
89
90    fn target_problem(&self) -> &ILP<bool> {
91        &self.target
92    }
93
94    fn extract_solution(
95        &self,
96        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
97    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
98        crate::rules::traits::validate_target_witness(
99            self.target_problem(),
100            target_solution,
101            |value| value.value.is_some(),
102            "target ILP assignment is infeasible",
103        )?;
104
105        Ok({
106            let mut source_solution = Vec::with_capacity(self.source.num_assignment_variables());
107            for object in 0..self.source.num_objects() {
108                for (attribute, &domain_size) in self.source.attribute_domains().iter().enumerate()
109                {
110                    let mut selected = (0..domain_size).filter(|&candidate| {
111                        target_solution[self.assignment_var_index(object, attribute, candidate)]
112                            == 1
113                    });
114                    let value = match (selected.next(), selected.next()) {
115                        (Some(value), None) => value,
116                        (None, _) => {
117                            return Err(crate::rules::ExtractionError::invalid(format!(
118                                "object {object}, attribute {attribute} has no selected value"
119                            )))
120                        }
121                        (Some(_), Some(_)) => {
122                            return Err(crate::rules::ExtractionError::invalid(format!(
123                                "object {object}, attribute {attribute} has multiple selected values"
124                            )))
125                        }
126                    };
127                    source_solution.push(value);
128                }
129            }
130            source_solution
131        })
132    }
133}
134
135#[crate::aggregate_reduction(ilp_feasibility)]
136impl crate::rules::AggregateReductionResult for ReductionCDFTToILP {}
137
138#[reduction(transform = {
139    exact {
140        num_vars = "num_objects * total_domain_size + num_objects * num_frequency_cells",
141        num_constraints = "num_objects * num_attributes + num_known_values + num_frequency_cells + 3 * num_objects * num_frequency_cells",
142        num_nonzeros = "num_objects * total_domain_size + num_known_values + 8 * num_objects * num_frequency_cells",
143    },
144    upper_bound {
145        max_constraint_magnitude_bits = "num_objects + 1",
146    },
147})]
148impl ReduceTo<ILP<bool>> for ConsistencyOfDatabaseFrequencyTables {
149    type Result = ReductionCDFTToILP;
150
151    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
152        let overflow = || {
153            crate::rules::ReductionError::integer_overflow::<Self, ILP<bool>>(
154                "representing the database ILP encoding",
155            )
156        };
157        let assignments = self
158            .num_objects()
159            .checked_mul(self.total_domain_size())
160            .ok_or_else(overflow)?;
161        let auxiliaries = self
162            .num_objects()
163            .checked_mul(self.num_frequency_cells())
164            .ok_or_else(overflow)?;
165        let num_vars = assignments.checked_add(auxiliaries).ok_or_else(overflow)?;
166        let num_constraints = auxiliaries
167            .checked_mul(3)
168            .and_then(|count| count.checked_add(self.num_assignment_variables()))
169            .and_then(|count| count.checked_add(self.num_known_values()))
170            .and_then(|count| count.checked_add(self.num_frequency_cells()))
171            .ok_or_else(overflow)?;
172        let source = self.clone();
173        let helper = ReductionCDFTToILP {
174            target: ILP::empty(),
175            source: source.clone(),
176        };
177
178        let allocation_error = |error| {
179            crate::rules::ReductionError::invalid_target::<Self, ILP<bool>>(format!(
180                "cannot allocate database ILP encoding: {error}"
181            ))
182        };
183        let mut constraints = Vec::new();
184        constraints
185            .try_reserve_exact(num_constraints)
186            .map_err(allocation_error)?;
187
188        for object in 0..source.num_objects() {
189            for (attribute, &domain_size) in source.attribute_domains().iter().enumerate() {
190                let mut terms = Vec::new();
191                terms
192                    .try_reserve_exact(domain_size)
193                    .map_err(allocation_error)?;
194                terms.extend(
195                    (0..domain_size)
196                        .map(|value| (helper.assignment_var_index(object, attribute, value), 1)),
197                );
198                constraints.push(LinearConstraint::eq(terms, 1));
199            }
200        }
201
202        for known_value in source.known_values() {
203            constraints.push(LinearConstraint::eq(
204                vec![(
205                    helper.assignment_var_index(
206                        known_value.object(),
207                        known_value.attribute(),
208                        known_value.value(),
209                    ),
210                    1,
211                )],
212                1,
213            ));
214        }
215
216        for (table_index, table) in source.frequency_tables().iter().enumerate() {
217            let rows = source.attribute_domains()[table.attribute_a()];
218            let cols = source.attribute_domains()[table.attribute_b()];
219
220            for value_a in 0..rows {
221                for value_b in 0..cols {
222                    let count_terms = (0..source.num_objects())
223                        .map(|object| {
224                            (
225                                helper.auxiliary_var_index(table_index, object, value_a, value_b),
226                                1,
227                            )
228                        })
229                        .collect();
230                    let count = table.counts()[value_a][value_b];
231                    constraints.push(LinearConstraint::eq(count_terms, count));
232
233                    for object in 0..source.num_objects() {
234                        let z = helper.auxiliary_var_index(table_index, object, value_a, value_b);
235                        let y_a = helper.assignment_var_index(object, table.attribute_a(), value_a);
236                        let y_b = helper.assignment_var_index(object, table.attribute_b(), value_b);
237
238                        constraints.extend(mccormick_product(z, y_a, y_b));
239                    }
240                }
241            }
242        }
243
244        let target = ILP::new(num_vars, constraints, vec![], ObjectiveSense::Minimize)
245            .map_err(Self::target_construction)?;
246
247        Ok(ReductionCDFTToILP { target, source })
248    }
249}
250
251#[cfg(feature = "example-db")]
252pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
253    use crate::models::misc::{FrequencyTable, KnownValue};
254
255    vec![crate::example_db::specs::RuleExampleSpec {
256        id: "consistencyofdatabasefrequencytables_to_ilp",
257        build: || {
258            let source = ConsistencyOfDatabaseFrequencyTables::new(
259                6,
260                vec![2, 3, 2],
261                vec![
262                    FrequencyTable::new(0, 1, vec![vec![1, 1, 1], vec![1, 1, 1]]),
263                    FrequencyTable::new(1, 2, vec![vec![1, 1], vec![0, 2], vec![1, 1]]),
264                ],
265                vec![
266                    KnownValue::new(0, 0, 0),
267                    KnownValue::new(3, 0, 1),
268                    KnownValue::new(1, 2, 1),
269                ],
270            );
271            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
272        },
273    }]
274}
275
276#[cfg(test)]
277#[path = "../unit_tests/rules/consistencyofdatabasefrequencytables_ilp.rs"]
278mod tests;
problemreductions/rules/consistencyofdatabasefrequencytables_ilp.rs

problemreductions/rules/
consistencyofdatabasefrequencytables_ilp.rs
