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        crate::rules::traits::validate_target_witness(
47            self.target_problem(),
48            target_solution,
49            |value| value.0,
50            "target configuration is not a feasible cyclic ordering",
51        )?;
52        let mut assignment = vec![false; self.source_num_vars];
53        for (compact, &original) in self.source_variables.iter().enumerate() {
54            let (alpha, beta, gamma) = variable_triple(compact);
55            assignment[original] = !is_cyclic_order(
56                target_solution[alpha],
57                target_solution[beta],
58                target_solution[gamma],
59            );
60        }
61        Ok(assignment)
62    }
63}
64
65fn variable_triple(var_idx: usize) -> (usize, usize, usize) {
66    let base = 3 * var_idx;
67    (base, base + 1, base + 2)
68}
69
70fn literal_triple(literal: i64) -> (usize, usize, usize) {
71    let (alpha, beta, gamma) = variable_triple(
72        usize::try_from(literal.unsigned_abs()).expect("normalized literal indices fit usize") - 1,
73    );
74    if literal > 0 {
75        (alpha, beta, gamma)
76    } else {
77        (alpha, gamma, beta)
78    }
79}
80
81#[allow(clippy::nonminimal_bool)]
82fn is_cyclic_order(a: usize, b: usize, c: usize) -> bool {
83    (a < b && b < c) || (b < c && c < a) || (c < a && a < b)
84}
85
86/// Three distinct, globally ordered variables per clause are required by
87/// Galil--Megiddo's simultaneous-extension argument (Corollary 2).
88struct NormalizedFormula {
89    source_variables: Vec<usize>,
90    num_vars: usize,
91    clauses: Vec<[i64; 3]>,
92}
93
94fn normalize(
95    source: &KSatisfiability<K3>,
96) -> Result<NormalizedFormula, crate::rules::ReductionError> {
97    let mut clauses = Vec::new();
98    let mut variables = BTreeSet::new();
99    for clause in source.clauses() {
100        let mut literals = clause.literals.clone();
101        literals.sort_unstable_by_key(|literal| (literal.unsigned_abs(), *literal));
102        literals.dedup();
103        if literals.windows(2).any(|pair| pair[0] == -pair[1]) {
104            continue;
105        }
106        for literal in &literals {
107            variables.insert(
108                usize::try_from(literal.unsigned_abs()).expect("native SAT indices fit usize") - 1,
109            );
110        }
111        clauses.push(literals);
112    }
113    let source_variables: Vec<_> = variables.into_iter().collect();
114    let mut variables =
115        SatVariableAllocator::new("KSatisfiability -> CyclicOrdering", source_variables.len())
116            .map_err(<KSatisfiability<K3> as ReduceTo<CyclicOrdering>>::target_construction)?;
117    let mut normalized = Vec::new();
118    for clause in clauses {
119        let literals: Vec<_> = clause
120            .iter()
121            .map(|literal| {
122                let original = usize::try_from(literal.unsigned_abs())
123                    .expect("native SAT indices fit usize")
124                    - 1;
125                let compact = source_variables
126                    .binary_search(&original)
127                    .expect("all retained variables were collected")
128                    + 1;
129                let index = i64::try_from(compact)
130                    .expect("compaction cannot increase a valid source variable index");
131                if *literal > 0 {
132                    index
133                } else {
134                    -index
135                }
136            })
137            .collect();
138        match *literals.as_slice() {
139            [a, b, c] => normalized.push([a, b, c]),
140            [a, b] => {
141                let u = variables.allocate()
142                    .map_err(<KSatisfiability<K3> as ReduceTo<CyclicOrdering>>::target_construction)?;
143                normalized.extend([[a, b, u], [a, b, -u]]);
144            }
145            [a] => {
146                let u = variables.allocate()
147                    .map_err(<KSatisfiability<K3> as ReduceTo<CyclicOrdering>>::target_construction)?;
148                let v = variables.allocate()
149                    .map_err(<KSatisfiability<K3> as ReduceTo<CyclicOrdering>>::target_construction)?;
150                normalized.extend([[a, u, v], [a, u, -v], [a, -u, v], [a, -u, -v]]);
151            }
152            _ => unreachable!("empty clauses are handled before normalization; native clauses have at most three literals"),
153        }
154    }
155    // Original compact indices precede all fresh indices. Every emitted
156    // clause is therefore already sorted by absolute variable index.
157    Ok(NormalizedFormula {
158        source_variables,
159        num_vars: variables.num_vars(),
160        clauses: normalized,
161    })
162}
163
164#[crate::aggregate_reduction(identity)]
165impl crate::rules::AggregateReductionResult for Reduction3SATToCyclicOrdering {}
166
167#[reduction(
168    transform = upper_bound {
169        num_elements = "3 * num_vars + 26 * num_clauses + 3",
170        num_triples = "40 * num_clauses + 2",
171    }
172)]
173impl ReduceTo<CyclicOrdering> for KSatisfiability<K3> {
174    type Result = Reduction3SATToCyclicOrdering;
175
176    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
177        if self
178            .clauses()
179            .iter()
180            .any(|clause| clause.literals.is_empty())
181        {
182            return Ok(Reduction3SATToCyclicOrdering {
183                target: CyclicOrdering::try_new(3, vec![(0, 1, 2), (0, 2, 1)])
184                    .map_err(<Self as ReduceTo<CyclicOrdering>>::target_construction)?,
185                source_num_vars: self.num_vars(),
186                source_variables: Vec::new(),
187            });
188        }
189        let normalized = normalize(self)?;
190        let num_vars = normalized.num_vars;
191        let num_clauses = normalized.clauses.len();
192        let overflow = |operation| {
193            crate::rules::ReductionError::integer_overflow::<Self, CyclicOrdering>(operation)
194        };
195        let variable_elements = num_vars
196            .checked_mul(3)
197            .ok_or_else(|| overflow("counting variable elements"))?;
198        let clause_elements = num_clauses
199            .checked_mul(5)
200            .ok_or_else(|| overflow("counting clause elements"))?;
201        let num_elements = variable_elements
202            .checked_add(clause_elements)
203            .ok_or_else(|| overflow("counting target elements"))?
204            .max(1);
205        let num_triples = num_clauses
206            .checked_mul(10)
207            .ok_or_else(|| overflow("counting target triples"))?;
208        let mut triples = Vec::with_capacity(num_triples);
209
210        for (clause_idx, clause) in normalized.clauses.iter().enumerate() {
211            let (a, b, c) = literal_triple(clause[0]);
212            let (d, e, f) = literal_triple(clause[1]);
213            let (g, h, i) = literal_triple(clause[2]);
214
215            let base = variable_elements + 5 * clause_idx;
216            let j = base;
217            let k = base + 1;
218            let l = base + 2;
219            let m = base + 3;
220            let n = base + 4;
221
222            triples.extend([
223                (a, c, j),
224                (b, j, k),
225                (c, k, l),
226                (d, f, j),
227                (e, j, l),
228                (f, l, m),
229                (g, i, k),
230                (h, k, m),
231                (i, m, n),
232                (n, m, l),
233            ]);
234        }
235
236        Ok(Reduction3SATToCyclicOrdering {
237            target: CyclicOrdering::try_new(num_elements, triples)
238                .map_err(<Self as ReduceTo<CyclicOrdering>>::target_construction)?,
239            source_num_vars: self.num_vars(),
240            source_variables: normalized.source_variables,
241        })
242    }
243}
244
245#[cfg(feature = "example-db")]
246pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
247    use crate::export::SolutionPair;
248    use crate::models::formula::CNFClause;
249
250    vec![crate::example_db::specs::RuleExampleSpec {
251        id: "ksatisfiability_to_cyclicordering",
252        build: || {
253            crate::example_db::specs::rule_example_with_witness::<_, CyclicOrdering>(
254                KSatisfiability::<K3>::new(3, vec![CNFClause::new(vec![1, 2, 3])]),
255                SolutionPair {
256                    source_config: serde_json::json!(vec![true, true, true]),
257                    target_config: serde_json::json!(vec![
258                        0, 11, 1, 9, 12, 10, 6, 13, 7, 2, 3, 4, 8, 5
259                    ]),
260                },
261            )
262        },
263    }]
264}
265
266#[cfg(test)]
267#[path = "../unit_tests/rules/ksatisfiability_cyclicordering.rs"]
268mod tests;
problemreductions/rules/ksatisfiability_cyclicordering.rs

problemreductions/rules/
ksatisfiability_cyclicordering.rs
