problemreductions/rules/
maximum2satisfiability_ilp.rs

1//! Reduction from Maximum 2-Satisfiability (MAX-2-SAT) to ILP.
2//!
3//! The standard MAX-2-SAT formulation maps directly to a binary ILP:
4//! - Variables: one binary variable per Boolean variable (truth assignment)
5//!   plus one binary indicator per clause (satisfaction indicator)
6//! - Constraints: for each clause, the indicator is at most the sum of its
7//!   literal expressions, ensuring z_j = 1 only if the clause is satisfied
8//! - Objective: maximize the sum of clause indicators
9
10use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP};
11use crate::models::formula::Maximum2Satisfiability;
12use crate::reduction;
13use crate::rules::traits::{ReduceTo, ReductionResult};
14
15/// Result of reducing Maximum2Satisfiability to ILP.
16#[derive(Debug, Clone)]
17pub struct ReductionMaximum2SatisfiabilityToILP {
18    target: ILP<bool>,
19    num_vars: usize,
20}
21
22impl ReductionResult for ReductionMaximum2SatisfiabilityToILP {
23    type Source = Maximum2Satisfiability;
24    type Target = ILP<bool>;
25
26    fn target_problem(&self) -> &ILP<bool> {
27        &self.target
28    }
29
30    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
31        target_solution[..self.num_vars].to_vec()
32    }
33}
34
35#[reduction(
36    overhead = {
37        num_vars = "num_vars + num_clauses",
38        num_constraints = "num_clauses",
39    }
40)]
41impl ReduceTo<ILP<bool>> for Maximum2Satisfiability {
42    type Result = ReductionMaximum2SatisfiabilityToILP;
43
44    fn reduce_to(&self) -> Self::Result {
45        let n = self.num_vars();
46        let m = self.num_clauses();
47        let num_ilp_vars = n + m;
48
49        // Build one constraint per clause:
50        // For clause j with literals l_1, l_2:
51        //   z_{n+j} <= l_1' + l_2'
52        // where l_i' = y_{var-1} if positive, or (1 - y_{var-1}) if negative.
53        //
54        // Rearranged: z_{n+j} - sum(y_i for positive lit i) + sum(y_i for negative lit i) <= k
55        // where k = number of negated literals in the clause.
56        let constraints: Vec<LinearConstraint> = self
57            .clauses()
58            .iter()
59            .enumerate()
60            .map(|(j, clause)| {
61                let mut terms: Vec<(usize, f64)> = Vec::new();
62                let mut neg_count = 0i32;
63
64                // z_{n+j} has coefficient +1
65                terms.push((n + j, 1.0));
66
67                for &lit in &clause.literals {
68                    let var_idx = lit.unsigned_abs() as usize - 1;
69                    if lit > 0 {
70                        // positive literal: subtract y_i
71                        terms.push((var_idx, -1.0));
72                    } else {
73                        // negative literal: add y_i
74                        terms.push((var_idx, 1.0));
75                        neg_count += 1;
76                    }
77                }
78
79                LinearConstraint::le(terms, neg_count as f64)
80            })
81            .collect();
82
83        // Objective: maximize sum of z_j indicators
84        let objective: Vec<(usize, f64)> = (0..m).map(|j| (n + j, 1.0)).collect();
85
86        let target = ILP::new(
87            num_ilp_vars,
88            constraints,
89            objective,
90            ObjectiveSense::Maximize,
91        );
92
93        ReductionMaximum2SatisfiabilityToILP {
94            target,
95            num_vars: n,
96        }
97    }
98}
99
100#[cfg(feature = "example-db")]
101pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
102    use crate::export::SolutionPair;
103    use crate::models::formula::CNFClause;
104
105    vec![crate::example_db::specs::RuleExampleSpec {
106        id: "maximum2satisfiability_to_ilp",
107        build: || {
108            let source = Maximum2Satisfiability::new(
109                4,
110                vec![
111                    CNFClause::new(vec![1, 2]),
112                    CNFClause::new(vec![1, -2]),
113                    CNFClause::new(vec![-1, 3]),
114                    CNFClause::new(vec![-1, -3]),
115                    CNFClause::new(vec![2, 4]),
116                    CNFClause::new(vec![-3, -4]),
117                    CNFClause::new(vec![3, 4]),
118                ],
119            );
120            // Optimal source config: [1,1,0,1] satisfies 6 of 7 clauses.
121            // ILP target config: first 4 are truth vars, next 7 are clause indicators.
122            // Clause satisfaction with [1,1,0,1] (x1=T, x2=T, x3=F, x4=T):
123            //   C0: (x1 OR x2)     = T  -> z4=1
124            //   C1: (x1 OR ~x2)    = T  -> z5=1
125            //   C2: (~x1 OR x3)    = F  -> z6=0
126            //   C3: (~x1 OR ~x3)   = T  -> z7=1
127            //   C4: (x2 OR x4)     = T  -> z8=1
128            //   C5: (~x3 OR ~x4)   = T  -> z9=1
129            //   C6: (x3 OR x4)     = T  -> z10=1
130            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
131                source,
132                SolutionPair {
133                    source_config: vec![1, 1, 0, 1],
134                    target_config: vec![1, 1, 0, 1, 1, 1, 0, 1, 1, 1, 1],
135                },
136            )
137        },
138    }]
139}
140
141#[cfg(test)]
142#[path = "../unit_tests/rules/maximum2satisfiability_ilp.rs"]
143mod tests;
problemreductions/rules/maximum2satisfiability_ilp.rs

problemreductions/rules/
maximum2satisfiability_ilp.rs
