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(
31        &self,
32        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
33    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
34        crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
35
36        Ok(target_solution[..self.num_vars]
37            .iter()
38            .map(|&value| value == 1)
39            .collect())
40    }
41}
42
43#[reduction(
44    transform = exact {
45        num_vars = "num_vars + num_clauses",
46        num_constraints = "num_clauses",
47    },
48    unavailable = {
49        num_nonzeros = "the exact target parameter is not represented by this reduction's symbolic transform",
50    }
51)]
52impl ReduceTo<ILP<bool>> for Maximum2Satisfiability {
53    type Result = ReductionMaximum2SatisfiabilityToILP;
54
55    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
56        let n = self.num_vars();
57        let m = self.num_clauses();
58        let num_ilp_vars = n + m;
59
60        // Build one constraint per clause:
61        // For clause j with literals l_1, l_2:
62        //   z_{n+j} <= l_1' + l_2'
63        // where l_i' = y_{var-1} if positive, or (1 - y_{var-1}) if negative.
64        //
65        // Rearranged: z_{n+j} - sum(y_i for positive lit i) + sum(y_i for negative lit i) <= k
66        // where k = number of negated literals in the clause.
67        let constraints: Vec<LinearConstraint> = self
68            .clauses()
69            .iter()
70            .enumerate()
71            .map(|(j, clause)| {
72                let mut terms: Vec<(usize, i64)> = Vec::new();
73                let mut neg_count = 0;
74
75                // z_{n+j} has coefficient +1
76                terms.push((n + j, 1));
77
78                for &lit in &clause.literals {
79                    let var_idx = lit.unsigned_abs() as usize - 1;
80                    if lit > 0 {
81                        // positive literal: subtract y_i
82                        terms.push((var_idx, -1));
83                    } else {
84                        // negative literal: add y_i
85                        terms.push((var_idx, 1));
86                        neg_count += 1;
87                    }
88                }
89
90                LinearConstraint::le(terms, neg_count)
91            })
92            .collect();
93
94        // Objective: maximize sum of z_j indicators
95        let objective: Vec<(usize, i64)> = (0..m).map(|j| (n + j, 1)).collect();
96
97        let target = ILP::new(
98            num_ilp_vars,
99            constraints,
100            objective,
101            ObjectiveSense::Maximize,
102        )
103        .map_err(<Self as ReduceTo<ILP<bool>>>::target_construction)?;
104
105        Ok(ReductionMaximum2SatisfiabilityToILP {
106            target,
107            num_vars: n,
108        })
109    }
110}
111
112#[cfg(feature = "example-db")]
113pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
114    use crate::export::SolutionPair;
115    use crate::models::formula::CNFClause;
116
117    vec![crate::example_db::specs::RuleExampleSpec {
118        id: "maximum2satisfiability_to_ilp",
119        build: || {
120            let source = Maximum2Satisfiability::new(
121                4,
122                vec![
123                    CNFClause::new(vec![1, 2]),
124                    CNFClause::new(vec![1, -2]),
125                    CNFClause::new(vec![-1, 3]),
126                    CNFClause::new(vec![-1, -3]),
127                    CNFClause::new(vec![2, 4]),
128                    CNFClause::new(vec![-3, -4]),
129                    CNFClause::new(vec![3, 4]),
130                ],
131            );
132            // Optimal source config: [1,1,0,1] satisfies 6 of 7 clauses.
133            // ILP target config: first 4 are truth vars, next 7 are clause indicators.
134            // Clause satisfaction with [1,1,0,1] (x1=T, x2=T, x3=F, x4=T):
135            //   C0: (x1 OR x2)     = T  -> z4=1
136            //   C1: (x1 OR ~x2)    = T  -> z5=1
137            //   C2: (~x1 OR x3)    = F  -> z6=0
138            //   C3: (~x1 OR ~x3)   = T  -> z7=1
139            //   C4: (x2 OR x4)     = T  -> z8=1
140            //   C5: (~x3 OR ~x4)   = T  -> z9=1
141            //   C6: (x3 OR x4)     = T  -> z10=1
142            crate::example_db::specs::rule_example_with_witness::<_, ILP<bool>>(
143                source,
144                SolutionPair {
145                    source_config: serde_json::json!(vec![true, true, false, true]),
146                    target_config: serde_json::json!(vec![1, 1, 0, 1, 1, 1, 0, 1, 1, 1, 1]),
147                },
148            )
149        },
150    }]
151}
152
153#[cfg(test)]
154#[path = "../unit_tests/rules/maximum2satisfiability_ilp.rs"]
155mod tests;
problemreductions/rules/maximum2satisfiability_ilp.rs

problemreductions/rules/
maximum2satisfiability_ilp.rs
