problemreductions/rules/
naesatisfiability_ilp.rs

1//! Reduction from NAESatisfiability to ILP (Integer Linear Programming).
2//!
3//! Binary variable x_i per Boolean variable. For each clause with literals
4//! l_1, ..., l_k (using substitution: positive literal contributes +x_i,
5//! negative literal contributes -x_i with rhs adjusted by -1 per negative):
6//! - At least one true:  Σ coeff_i * x_i ≥ 1 - neg_count
7//! - At least one false: Σ coeff_i * x_i ≤ |C| - 1 - neg_count
8//!
9//! Objective: empty (feasibility problem).
10
11use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP};
12use crate::models::formula::NAESatisfiability;
13use crate::reduction;
14use crate::rules::traits::{ReduceTo, ReductionResult};
15
16#[derive(Debug, Clone)]
17pub struct ReductionNAESATToILP {
18    target: ILP<bool>,
19}
20
21impl ReductionResult for ReductionNAESATToILP {
22    type Source = NAESatisfiability;
23    type Target = ILP<bool>;
24
25    fn target_problem(&self) -> &ILP<bool> {
26        &self.target
27    }
28
29    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
30        target_solution.to_vec()
31    }
32}
33
34#[reduction(
35    overhead = {
36        num_vars = "num_vars",
37        num_constraints = "2 * num_clauses",
38    }
39)]
40impl ReduceTo<ILP<bool>> for NAESatisfiability {
41    type Result = ReductionNAESATToILP;
42
43    fn reduce_to(&self) -> Self::Result {
44        let num_vars = self.num_vars();
45        let mut constraints = Vec::new();
46
47        for clause in self.clauses() {
48            let clause_size = clause.len();
49            let mut terms: Vec<(usize, f64)> = Vec::with_capacity(clause_size);
50            let mut neg_count: f64 = 0.0;
51
52            for &lit in &clause.literals {
53                // Variables are 1-indexed in CNFClause literals.
54                let var_idx = lit.unsigned_abs() as usize - 1;
55                if lit > 0 {
56                    // Positive literal x_i: coefficient +1
57                    terms.push((var_idx, 1.0));
58                } else {
59                    // Negative literal ¬x_i: substitute (1 - x_i), so coefficient -1
60                    // and adjust rhs by -1 (accumulated in neg_count).
61                    terms.push((var_idx, -1.0));
62                    neg_count += 1.0;
63                }
64            }
65
66            // At least one literal is true: Σ coeff_i * x_i ≥ 1 - neg_count
67            constraints.push(LinearConstraint::ge(terms.clone(), 1.0 - neg_count));
68
69            // At least one literal is false: Σ coeff_i * x_i ≤ |C| - 1 - neg_count
70            constraints.push(LinearConstraint::le(
71                terms,
72                clause_size as f64 - 1.0 - neg_count,
73            ));
74        }
75
76        let target = ILP::new(num_vars, constraints, vec![], ObjectiveSense::Minimize);
77        ReductionNAESATToILP { target }
78    }
79}
80
81#[cfg(feature = "example-db")]
82pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
83    use crate::models::formula::CNFClause;
84    vec![crate::example_db::specs::RuleExampleSpec {
85        id: "naesatisfiability_to_ilp",
86        build: || {
87            // NAE-SAT instance: (x1 ∨ x2 ∨ x3) ∧ (¬x1 ∨ ¬x2 ∨ x3)
88            // Solution x1=T, x2=F, x3=F: clause1 T,F,F (NAE ✓); clause2 F,T,F (NAE ✓)
89            let source = NAESatisfiability::new(
90                3,
91                vec![
92                    CNFClause::new(vec![1, 2, 3]),   // x1 ∨ x2 ∨ x3
93                    CNFClause::new(vec![-1, -2, 3]), // ¬x1 ∨ ¬x2 ∨ x3
94                ],
95            );
96            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
97        },
98    }]
99}
100
101#[cfg(test)]
102#[path = "../unit_tests/rules/naesatisfiability_ilp.rs"]
103mod tests;
problemreductions/rules/naesatisfiability_ilp.rs

problemreductions/rules/
naesatisfiability_ilp.rs
