problemreductions/rules/
ksatisfiability_cyclicordering.rs

1//! Reduction from KSatisfiability (3-SAT) to CyclicOrdering.
2//!
3//! Galil and Megiddo's construction associates each variable with three
4//! elements `(alpha_i, beta_i, gamma_i)`. A satisfying assignment is encoded by
5//! which of the two cyclic orientations `(alpha_i, beta_i, gamma_i)` and
6//! `(alpha_i, gamma_i, beta_i)` is derived by the final cyclic order. Each
7//! clause contributes five fresh auxiliary elements and ten cyclic-ordering
8//! triples enforcing that at least one literal orientation must be the
9//! "true" one.
10//!
11//! Before applying the gadget, remove tautologies and repeated literals,
12//! compact occurring variables, and expand short clauses with fresh variables.
13//! Each resulting clause has three distinct variables in global index order.
14//! This is the hypothesis needed to combine the paper's local cyclic orders.
15//! Empty clauses and empty conjunctions map to fixed NO and YES targets.
16//!
17//! Reference: Galil and Megiddo, "Cyclic ordering is NP-complete", 1977.
18
19use crate::models::formula::KSatisfiability;
20use crate::models::misc::CyclicOrdering;
21use crate::reduction;
22use crate::rules::sat_helpers::SatVariableAllocator;
23use crate::rules::traits::{ReduceTo, ReductionResult};
24use crate::variant::K3;
25use std::collections::BTreeSet;
26
27#[derive(Debug, Clone)]
28pub struct Reduction3SATToCyclicOrdering {
29    target: CyclicOrdering,
30    source_num_vars: usize,
31    source_variables: Vec<usize>,
32}
33
34impl ReductionResult for Reduction3SATToCyclicOrdering {
35    type Source = KSatisfiability<K3>;
36    type Target = CyclicOrdering;
37
38    fn target_problem(&self) -> &Self::Target {
39        &self.target
40    }
41
42    fn extract_solution(
43        &self,
44        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
45    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
46        let value =
47            crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
48        if !value.0 {
49            return Err(crate::rules::ExtractionError::invalid(
50                "target configuration is not a feasible cyclic ordering",
51            ));
52        }
53        let mut assignment = vec![false; self.source_num_vars];
54        for (compact, &original) in self.source_variables.iter().enumerate() {
55            let (alpha, beta, gamma) = variable_triple(compact);
56            assignment[original] = !is_cyclic_order(
57                target_solution[alpha],
58                target_solution[beta],
59                target_solution[gamma],
60            );
61        }
62        Ok(assignment)
63    }
64}
65
66fn variable_triple(var_idx: usize) -> (usize, usize, usize) {
67    let base = 3 * var_idx;
68    (base, base + 1, base + 2)
69}
70
71fn literal_triple(literal: i64) -> (usize, usize, usize) {
72    let (alpha, beta, gamma) = variable_triple(
73        usize::try_from(literal.unsigned_abs()).expect("normalized literal indices fit usize") - 1,
74    );
75    if literal > 0 {
76        (alpha, beta, gamma)
77    } else {
78        (alpha, gamma, beta)
79    }
80}
81
82#[allow(clippy::nonminimal_bool)]
83fn is_cyclic_order(a: usize, b: usize, c: usize) -> bool {
84    (a < b && b < c) || (b < c && c < a) || (c < a && a < b)
85}
86
87/// Three distinct, globally ordered variables per clause are required by
88/// Galil--Megiddo's simultaneous-extension argument (Corollary 2).
89struct NormalizedFormula {
90    source_variables: Vec<usize>,
91    num_vars: usize,
92    clauses: Vec<[i64; 3]>,
93}
94
95fn normalize(
96    source: &KSatisfiability<K3>,
97) -> Result<NormalizedFormula, crate::rules::ReductionError> {
98    let mut clauses = Vec::new();
99    let mut variables = BTreeSet::new();
100    for clause in source.clauses() {
101        let mut literals = clause.literals.clone();
102        literals.sort_unstable_by_key(|literal| (literal.unsigned_abs(), *literal));
103        literals.dedup();
104        if literals.windows(2).any(|pair| pair[0] == -pair[1]) {
105            continue;
106        }
107        for literal in &literals {
108            variables.insert(
109                usize::try_from(literal.unsigned_abs()).expect("native SAT indices fit usize") - 1,
110            );
111        }
112        clauses.push(literals);
113    }
114    let source_variables: Vec<_> = variables.into_iter().collect();
115    let mut variables =
116        SatVariableAllocator::new("KSatisfiability -> CyclicOrdering", source_variables.len())
117            .map_err(<KSatisfiability<K3> as ReduceTo<CyclicOrdering>>::target_construction)?;
118    let mut normalized = Vec::new();
119    for clause in clauses {
120        let literals: Vec<_> = clause
121            .iter()
122            .map(|literal| {
123                let original = usize::try_from(literal.unsigned_abs())
124                    .expect("native SAT indices fit usize")
125                    - 1;
126                let compact = source_variables
127                    .binary_search(&original)
128                    .expect("all retained variables were collected")
129                    + 1;
130                let index = i64::try_from(compact)
131                    .expect("compaction cannot increase a valid source variable index");
132                if *literal > 0 {
133                    index
134                } else {
135                    -index
136                }
137            })
138            .collect();
139        match *literals.as_slice() {
140            [a, b, c] => normalized.push([a, b, c]),
141            [a, b] => {
142                let u = variables.allocate()
143                    .map_err(<KSatisfiability<K3> as ReduceTo<CyclicOrdering>>::target_construction)?;
144                normalized.extend([[a, b, u], [a, b, -u]]);
145            }
146            [a] => {
147                let u = variables.allocate()
148                    .map_err(<KSatisfiability<K3> as ReduceTo<CyclicOrdering>>::target_construction)?;
149                let v = variables.allocate()
150                    .map_err(<KSatisfiability<K3> as ReduceTo<CyclicOrdering>>::target_construction)?;
151                normalized.extend([[a, u, v], [a, u, -v], [a, -u, v], [a, -u, -v]]);
152            }
153            _ => unreachable!("empty clauses are handled before normalization; native clauses have at most three literals"),
154        }
155    }
156    // Original compact indices precede all fresh indices. Every emitted
157    // clause is therefore already sorted by absolute variable index.
158    Ok(NormalizedFormula {
159        source_variables,
160        num_vars: variables.num_vars(),
161        clauses: normalized,
162    })
163}
164
165#[reduction(
166    transform = upper_bound {
167        num_elements = "3 * num_vars + 26 * num_clauses + 3",
168        num_triples = "40 * num_clauses + 2",
169    }
170)]
171impl ReduceTo<CyclicOrdering> for KSatisfiability<K3> {
172    type Result = Reduction3SATToCyclicOrdering;
173
174    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
175        if self
176            .clauses()
177            .iter()
178            .any(|clause| clause.literals.is_empty())
179        {
180            return Ok(Reduction3SATToCyclicOrdering {
181                target: CyclicOrdering::try_new(3, vec![(0, 1, 2), (0, 2, 1)])
182                    .map_err(<Self as ReduceTo<CyclicOrdering>>::target_construction)?,
183                source_num_vars: self.num_vars(),
184                source_variables: Vec::new(),
185            });
186        }
187        let normalized = normalize(self)?;
188        let num_vars = normalized.num_vars;
189        let num_clauses = normalized.clauses.len();
190        let overflow = |operation| {
191            crate::rules::ReductionError::integer_overflow::<Self, CyclicOrdering>(operation)
192        };
193        let variable_elements = num_vars
194            .checked_mul(3)
195            .ok_or_else(|| overflow("counting variable elements"))?;
196        let clause_elements = num_clauses
197            .checked_mul(5)
198            .ok_or_else(|| overflow("counting clause elements"))?;
199        let num_elements = variable_elements
200            .checked_add(clause_elements)
201            .ok_or_else(|| overflow("counting target elements"))?
202            .max(1);
203        let num_triples = num_clauses
204            .checked_mul(10)
205            .ok_or_else(|| overflow("counting target triples"))?;
206        let mut triples = Vec::with_capacity(num_triples);
207
208        for (clause_idx, clause) in normalized.clauses.iter().enumerate() {
209            let (a, b, c) = literal_triple(clause[0]);
210            let (d, e, f) = literal_triple(clause[1]);
211            let (g, h, i) = literal_triple(clause[2]);
212
213            let base = variable_elements + 5 * clause_idx;
214            let j = base;
215            let k = base + 1;
216            let l = base + 2;
217            let m = base + 3;
218            let n = base + 4;
219
220            triples.extend([
221                (a, c, j),
222                (b, j, k),
223                (c, k, l),
224                (d, f, j),
225                (e, j, l),
226                (f, l, m),
227                (g, i, k),
228                (h, k, m),
229                (i, m, n),
230                (n, m, l),
231            ]);
232        }
233
234        Ok(Reduction3SATToCyclicOrdering {
235            target: CyclicOrdering::try_new(num_elements, triples)
236                .map_err(<Self as ReduceTo<CyclicOrdering>>::target_construction)?,
237            source_num_vars: self.num_vars(),
238            source_variables: normalized.source_variables,
239        })
240    }
241}
242
243#[cfg(feature = "example-db")]
244pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
245    use crate::export::SolutionPair;
246    use crate::models::formula::CNFClause;
247
248    vec![crate::example_db::specs::RuleExampleSpec {
249        id: "ksatisfiability_to_cyclicordering",
250        build: || {
251            crate::example_db::specs::rule_example_with_witness::<_, CyclicOrdering>(
252                KSatisfiability::<K3>::new(3, vec![CNFClause::new(vec![1, 2, 3])]),
253                SolutionPair {
254                    source_config: serde_json::json!(vec![true, true, true]),
255                    target_config: serde_json::json!(vec![
256                        0, 11, 1, 9, 12, 10, 6, 13, 7, 2, 3, 4, 8, 5
257                    ]),
258                },
259            )
260        },
261    }]
262}
263
264#[cfg(test)]
265#[path = "../unit_tests/rules/ksatisfiability_cyclicordering.rs"]
266mod tests;
problemreductions/rules/ksatisfiability_cyclicordering.rs

problemreductions/rules/
ksatisfiability_cyclicordering.rs
