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//! Reference: Galil and Megiddo, "Cyclic ordering is NP-complete", 1977.
12
13use crate::models::formula::KSatisfiability;
14use crate::models::misc::CyclicOrdering;
15use crate::reduction;
16use crate::rules::traits::{ReduceTo, ReductionResult};
17use crate::variant::K3;
18
19#[derive(Debug, Clone)]
20pub struct Reduction3SATToCyclicOrdering {
21    target: CyclicOrdering,
22    source_num_vars: usize,
23}
24
25impl ReductionResult for Reduction3SATToCyclicOrdering {
26    type Source = KSatisfiability<K3>;
27    type Target = CyclicOrdering;
28
29    fn target_problem(&self) -> &Self::Target {
30        &self.target
31    }
32
33    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
34        (0..self.source_num_vars)
35            .map(|var_idx| {
36                let (alpha, beta, gamma) = variable_triple(var_idx);
37                usize::from(!is_cyclic_order(
38                    target_solution[alpha],
39                    target_solution[beta],
40                    target_solution[gamma],
41                ))
42            })
43            .collect()
44    }
45}
46
47fn variable_triple(var_idx: usize) -> (usize, usize, usize) {
48    let base = 3 * var_idx;
49    (base, base + 1, base + 2)
50}
51
52fn literal_triple(literal: i32) -> (usize, usize, usize) {
53    let (alpha, beta, gamma) = variable_triple((literal.unsigned_abs() as usize) - 1);
54    if literal > 0 {
55        (alpha, beta, gamma)
56    } else {
57        (alpha, gamma, beta)
58    }
59}
60
61#[allow(clippy::nonminimal_bool)]
62fn is_cyclic_order(a: usize, b: usize, c: usize) -> bool {
63    (a < b && b < c) || (b < c && c < a) || (c < a && a < b)
64}
65
66#[reduction(
67    overhead = {
68        num_elements = "3 * num_vars + 5 * num_clauses",
69        num_triples = "10 * num_clauses",
70    }
71)]
72impl ReduceTo<CyclicOrdering> for KSatisfiability<K3> {
73    type Result = Reduction3SATToCyclicOrdering;
74
75    fn reduce_to(&self) -> Self::Result {
76        let num_vars = self.num_vars();
77        let num_clauses = self.num_clauses();
78        let num_elements = 3 * num_vars + 5 * num_clauses;
79        let mut triples = Vec::with_capacity(10 * num_clauses);
80
81        for (clause_idx, clause) in self.clauses().iter().enumerate() {
82            let (a, b, c) = literal_triple(clause.literals[0]);
83            let (d, e, f) = literal_triple(clause.literals[1]);
84            let (g, h, i) = literal_triple(clause.literals[2]);
85
86            let base = 3 * num_vars + 5 * clause_idx;
87            let j = base;
88            let k = base + 1;
89            let l = base + 2;
90            let m = base + 3;
91            let n = base + 4;
92
93            triples.extend([
94                (a, c, j),
95                (b, j, k),
96                (c, k, l),
97                (d, f, j),
98                (e, j, l),
99                (f, l, m),
100                (g, i, k),
101                (h, k, m),
102                (i, m, n),
103                (n, m, l),
104            ]);
105        }
106
107        Reduction3SATToCyclicOrdering {
108            target: CyclicOrdering::new(num_elements, triples),
109            source_num_vars: num_vars,
110        }
111    }
112}
113
114#[cfg(feature = "example-db")]
115pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
116    use crate::export::SolutionPair;
117    use crate::models::formula::CNFClause;
118
119    vec![crate::example_db::specs::RuleExampleSpec {
120        id: "ksatisfiability_to_cyclicordering",
121        build: || {
122            crate::example_db::specs::rule_example_with_witness::<_, CyclicOrdering>(
123                KSatisfiability::<K3>::new(3, vec![CNFClause::new(vec![1, 2, 3])]),
124                SolutionPair {
125                    source_config: vec![1, 1, 1],
126                    target_config: vec![0, 11, 1, 9, 12, 10, 6, 13, 7, 2, 3, 4, 8, 5],
127                },
128            )
129        },
130    }]
131}
132
133#[cfg(test)]
134#[path = "../unit_tests/rules/ksatisfiability_cyclicordering.rs"]
135mod tests;
problemreductions/rules/ksatisfiability_cyclicordering.rs

problemreductions/rules/
ksatisfiability_cyclicordering.rs
