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

problemreductions/rules/
maximum2satisfiability_ilp.rs
