problemreductions/rules/
naesatisfiability_maxcut.rs

1//! Reduction from NAESatisfiability to MaxCut.
2//!
3//! Long NAE clauses are first expanded into a chain of ternary clauses with
4//! fresh variables. Binary clauses contribute one unit edge, ternary clauses
5//! contribute a unit triangle. A positive-weight edge separates each variable
6//! from its negation. A cut certifies a source witness exactly when it attains
7//! the sum of these componentwise upper bounds.
8//!
9//! The NAE clause-chain construction is described by Jackson,
10//! "Flexible constraint satisfiability and a problem in semigroup theory",
11//! Section 4, arXiv:1512.03127. The triangle construction is the classical
12//! NAE-3SAT to MaxCut reduction (Garey and Johnson, ND16).
13
14use crate::models::formula::NAESatisfiability;
15use crate::models::graph::MaxCut;
16use crate::reduction;
17use crate::rules::traits::{ReduceTo, ReductionResult};
18use crate::topology::SimpleGraph;
19
20/// Result of reducing NAESatisfiability to MaxCut.
21#[derive(Debug, Clone)]
22pub struct ReductionNAESATToMaxCut {
23    target: MaxCut<SimpleGraph, i64>,
24    source_num_vars: usize,
25    feasible_cut: i64,
26}
27
28impl ReductionResult for ReductionNAESATToMaxCut {
29    type Source = NAESatisfiability;
30    type Target = MaxCut<SimpleGraph, i64>;
31
32    fn target_problem(&self) -> &Self::Target {
33        &self.target
34    }
35
36    /// Extract a NAE-SAT assignment from a MaxCut partition.
37    ///
38    /// Variable x_i is assigned based on vertex 2*i: if it is in set 0
39    /// (config[2*i] == 0), set x_i = false (config value 0); if in set 1,
40    /// set x_i = true (config value 1).
41    fn extract_solution(
42        &self,
43        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
44    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
45        let value =
46            crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
47        if !crate::rules::AggregateReductionResult::extract_value(self, value).0 {
48            return Err(crate::rules::ExtractionError::invalid(
49                "target cut does not certify a satisfying NAE assignment",
50            ));
51        }
52
53        Ok({
54            (0..self.source_num_vars)
55                .map(|i| target_solution[2 * i])
56                .collect()
57        })
58    }
59}
60
61impl crate::rules::AggregateReductionResult for ReductionNAESATToMaxCut {
62    type Source = NAESatisfiability;
63    type Target = MaxCut<SimpleGraph, i64>;
64
65    fn target_problem(&self) -> &Self::Target {
66        &self.target
67    }
68
69    fn extract_value(&self, value: crate::types::Max<i64>) -> crate::types::Or {
70        crate::types::Or(value.0 == Some(self.feasible_cut))
71    }
72}
73
74/// Dimensions, variable-edge weight, and certificate for legal clause lengths.
75fn nae_maxcut_parameters(
76    n: usize,
77    lengths: impl ExactSizeIterator<Item = usize>,
78) -> Result<(usize, usize, i64, i64), crate::rules::ReductionError> {
79    let overflow = |operation| {
80        crate::rules::ReductionError::integer_overflow::<NAESatisfiability, MaxCut<SimpleGraph, i64>>(
81            operation,
82        )
83    };
84    let weight = i64::try_from(lengths.len())
85        .ok()
86        .and_then(|m| m.checked_add(1))
87        .ok_or_else(|| overflow("computing the variable-edge weight"))?;
88    let mut variables = n;
89    let mut clause_edges = 0usize;
90    let mut clause_cap = 0usize;
91    for length in lengths {
92        // Source construction guarantees length >= 2.
93        let (auxiliary, edges, cap) = if length == 2 {
94            (0, 1, 1)
95        } else {
96            let triangles = length - 2;
97            (
98                length - 3,
99                triangles
100                    .checked_mul(3)
101                    .ok_or_else(|| overflow("counting clause edges"))?,
102                triangles
103                    .checked_mul(2)
104                    .ok_or_else(|| overflow("counting clause cut capacity"))?,
105            )
106        };
107        variables = variables
108            .checked_add(auxiliary)
109            .ok_or_else(|| overflow("counting auxiliary variables"))?;
110        clause_edges = clause_edges
111            .checked_add(edges)
112            .ok_or_else(|| overflow("counting all clause edges"))?;
113        clause_cap = clause_cap
114            .checked_add(cap)
115            .ok_or_else(|| overflow("counting all clause cut capacities"))?;
116    }
117    let vertices = variables
118        .checked_mul(2)
119        .ok_or_else(|| overflow("counting literal vertices"))?;
120    let edges = variables
121        .checked_add(clause_edges)
122        .ok_or_else(|| overflow("counting target edges"))?;
123    let variable_weight = i64::try_from(variables)
124        .ok()
125        .and_then(|q| q.checked_mul(weight))
126        .ok_or_else(|| overflow("summing variable-edge weights"))?;
127    // All weights are nonnegative: bounding their total bounds every cut sum.
128    variable_weight
129        .checked_add(
130            i64::try_from(clause_edges).map_err(|_| overflow("converting clause-edge count"))?,
131        )
132        .ok_or_else(|| overflow("summing all target edge weights"))?;
133    let feasible_cut = variable_weight
134        .checked_add(
135            i64::try_from(clause_cap).map_err(|_| overflow("converting clause cut capacity"))?,
136        )
137        .ok_or_else(|| overflow("computing the NAE cut certificate"))?;
138    // SimpleGraph uses petgraph's default index domain for nodes and edges.
139    petgraph::graph::DefaultIx::try_from(vertices)
140        .map_err(|_| overflow("representing target vertex indices"))?;
141    petgraph::graph::DefaultIx::try_from(edges)
142        .map_err(|_| overflow("representing target edge indices"))?;
143    Ok((vertices, edges, weight, feasible_cut))
144}
145
146#[reduction(
147    aggregate = custom,
148    transform = upper_bound {
149        num_vertices = "2 * (num_vars + num_literals - 2 * num_clauses)",
150        num_edges = "num_vars + 4 * num_literals - 7 * num_clauses",
151    }
152)]
153impl ReduceTo<MaxCut<SimpleGraph, i64>> for NAESatisfiability {
154    type Result = ReductionNAESATToMaxCut;
155
156    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
157        let (total_vertices, total_edges, weight, feasible_cut) =
158            nae_maxcut_parameters(self.num_vars(), self.clauses().iter().map(|c| c.len()))?;
159        let total_variables = total_vertices / 2;
160        let mut edges = Vec::with_capacity(total_edges);
161        let mut weights = Vec::with_capacity(total_edges);
162        for i in 0..total_variables {
163            edges.push((2 * i, 2 * i + 1));
164            weights.push(weight);
165        }
166
167        let mut next_auxiliary = self.num_vars();
168        for clause in self.clauses() {
169            let literals: Vec<_> = clause
170                .literals
171                .iter()
172                .map(|&literal| {
173                    let index = usize::try_from(literal.unsigned_abs()).map_err(|_| {
174                        crate::rules::ReductionError::integer_overflow::<
175                            NAESatisfiability,
176                            MaxCut<SimpleGraph, i64>,
177                        >("converting a literal index")
178                    })? - 1;
179                    // Validated literals are in 1..=n, and 2*total_variables was checked.
180                    Ok(2 * index + usize::from(literal < 0))
181                })
182                .collect::<Result<_, crate::rules::ReductionError>>()?;
183            if literals.len() == 2 {
184                edges.push((literals[0], literals[1]));
185                weights.push(1);
186            } else {
187                let mut first = literals[0];
188                for &middle in &literals[1..literals.len() - 2] {
189                    let auxiliary = 2 * next_auxiliary;
190                    next_auxiliary += 1;
191                    edges.extend([(first, middle), (first, auxiliary), (middle, auxiliary)]);
192                    weights.extend([1; 3]);
193                    first = auxiliary + 1;
194                }
195                let second = literals[literals.len() - 2];
196                let third = literals[literals.len() - 1];
197                edges.extend([(first, second), (first, third), (second, third)]);
198                weights.extend([1; 3]);
199            }
200        }
201
202        Ok(ReductionNAESATToMaxCut {
203            target: MaxCut::new(SimpleGraph::new(total_vertices, edges), weights),
204            source_num_vars: self.num_vars(),
205            feasible_cut,
206        })
207    }
208}
209
210#[cfg(feature = "example-db")]
211pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
212    use crate::export::SolutionPair;
213    use crate::models::formula::CNFClause;
214
215    vec![crate::example_db::specs::RuleExampleSpec {
216        id: "naesatisfiability_to_maxcut",
217        build: || {
218            // 3 variables, 2 clauses:
219            //   C1 = (x1, x2, ~x3)
220            //   C2 = (~x1, x3, x2)
221            // NAE-satisfying: x1=T, x2=F, x3=T
222            let source = NAESatisfiability::new(
223                3,
224                vec![
225                    CNFClause::new(vec![1, 2, -3]),
226                    CNFClause::new(vec![-1, 3, 2]),
227                ],
228            );
229            crate::example_db::specs::rule_example_with_witness::<_, MaxCut<SimpleGraph, i64>>(
230                source,
231                SolutionPair {
232                    // x1=T(1), x2=F(0), x3=T(1)
233                    source_config: serde_json::json!(vec![true, false, true]),
234                    // Vertices: x1(0)=1, ~x1(1)=0, x2(2)=0, ~x2(3)=1, x3(4)=1, ~x3(5)=0
235                    // All variable edges cross (weight M=3 each) -> 3*3=9
236                    // C1=(x1,x2,~x3): vertices 0,2,5 -> sides {1},{0,0} -> edges (0,2) crosses, (0,5) crosses, (2,5) doesn't -> +2
237                    // C2=(~x1,x3,x2): vertices 1,4,2 -> sides {0},{1,0} -> edges (1,4) crosses, (1,2) doesn't, (4,2) crosses -> +2
238                    // Total = 9 + 2 + 2 = 13
239                    target_config: serde_json::json!(vec![true, false, false, true, true, false]),
240                },
241            )
242        },
243    }]
244}
245
246#[cfg(test)]
247#[path = "../unit_tests/rules/naesatisfiability_maxcut.rs"]
248mod tests;
problemreductions/rules/naesatisfiability_maxcut.rs

problemreductions/rules/
naesatisfiability_maxcut.rs
