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(
30        &self,
31        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
32    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
33        crate::rules::traits::validate_target_witness(
34            self.target_problem(),
35            target_solution,
36            |value| value.value.is_some(),
37            "target ILP assignment is infeasible",
38        )?;
39
40        Ok(target_solution.iter().map(|&value| value == 1).collect())
41    }
42}
43
44#[crate::aggregate_reduction(ilp_feasibility)]
45impl crate::rules::AggregateReductionResult for ReductionNAESATToILP {}
46
47// Each clause emits two rows. Repeated variables merge and opposite
48// literals cancel, so support is at most twice the summed distinct variables.
49// This retains both the dense 2*n*c cap and the occurrence 2*L cap.
50#[reduction(transform = {
51    exact {
52        num_vars = "num_vars",
53        num_constraints = "2 * num_clauses",
54    },
55    upper_bound {
56        max_constraint_magnitude_bits = "num_literals + 1",
57        num_nonzeros = "2 * num_clause_variables",
58    },
59})]
60impl ReduceTo<ILP<bool>> for NAESatisfiability {
61    type Result = ReductionNAESATToILP;
62
63    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
64        let num_vars = self.num_vars();
65        let mut constraints = Vec::new();
66
67        for clause in self.clauses() {
68            let clause_size = clause.len();
69            let mut terms: Vec<(usize, i64)> = Vec::with_capacity(clause_size);
70            let clause_size =
71                <Self as ReduceTo<ILP<bool>>>::exact_i64(clause_size, "encoding a clause size")?;
72            let mut neg_count: i64 = 0;
73
74            for &lit in &clause.literals {
75                // Variables are 1-indexed in CNFClause literals.
76                let var_idx = lit.unsigned_abs() as usize - 1;
77                if lit > 0 {
78                    // Positive literal x_i: coefficient +1
79                    terms.push((var_idx, 1));
80                } else {
81                    // Negative literal ¬x_i: substitute (1 - x_i), so coefficient -1
82                    // and adjust rhs by -1 (accumulated in neg_count).
83                    terms.push((var_idx, -1));
84                    neg_count += 1;
85                }
86            }
87
88            // At least one literal is true: Σ coeff_i * x_i ≥ 1 - neg_count
89            constraints.push(LinearConstraint::ge(terms.clone(), 1 - neg_count));
90
91            // At least one literal is false: Σ coeff_i * x_i ≤ |C| - 1 - neg_count
92            constraints.push(LinearConstraint::le(terms, clause_size - 1 - neg_count));
93        }
94
95        let target = ILP::new(num_vars, constraints, vec![], ObjectiveSense::Minimize)
96            .map_err(<Self as ReduceTo<ILP<bool>>>::target_construction)?;
97        Ok(ReductionNAESATToILP { target })
98    }
99}
100
101#[cfg(feature = "example-db")]
102pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
103    use crate::models::formula::CNFClause;
104    vec![crate::example_db::specs::RuleExampleSpec {
105        id: "naesatisfiability_to_ilp",
106        build: || {
107            // NAE-SAT instance: (x1 ∨ x2 ∨ x3) ∧ (¬x1 ∨ ¬x2 ∨ x3)
108            // Solution x1=T, x2=F, x3=F: clause1 T,F,F (NAE ✓); clause2 F,T,F (NAE ✓)
109            let source = NAESatisfiability::new(
110                3,
111                vec![
112                    CNFClause::new(vec![1, 2, 3]),   // x1 ∨ x2 ∨ x3
113                    CNFClause::new(vec![-1, -2, 3]), // ¬x1 ∨ ¬x2 ∨ x3
114                ],
115            );
116            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
117        },
118    }]
119}
120
121#[cfg(test)]
122#[path = "../unit_tests/rules/naesatisfiability_ilp.rs"]
123mod tests;
problemreductions/rules/naesatisfiability_ilp.rs

problemreductions/rules/
naesatisfiability_ilp.rs
