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

problemreductions/rules/
naesatisfiability_maxcut.rs
