problemreductions/rules/
ksatisfiability_kclique.rs

1//! Reduction from KSatisfiability (3-SAT) to KClique.
2//!
3//! Classical Karp (1972) reduction. Given a 3-SAT formula with `m` clauses over
4//! `n` variables, construct a graph with `3m` vertices — one per literal position
5//! in each clause. Connect two vertices `(j1, p1)` and `(j2, p2)` if and only if
6//! they belong to different clauses (`j1 ≠ j2`) and their literals are not
7//! contradictory (not `x_i` and `¬x_i`). Set `k = m`.
8//!
9//! A satisfying assignment selects one true literal per clause, forming a clique
10//! of size `m`. Conversely, any `m`-clique picks one non-contradictory literal
11//! per clause, which can be extended to a satisfying assignment.
12//!
13//! Reference: Karp, "Reducibility among combinatorial problems", 1972.
14
15use crate::models::formula::KSatisfiability;
16use crate::models::graph::KClique;
17use crate::reduction;
18use crate::rules::traits::{ReduceTo, ReductionResult};
19use crate::topology::SimpleGraph;
20use crate::variant::K3;
21
22/// Result of reducing KSatisfiability<K3> to KClique<SimpleGraph>.
23#[derive(Debug, Clone)]
24pub struct Reduction3SATToKClique {
25    target: KClique<SimpleGraph>,
26    /// Clauses from the source problem, needed for solution extraction.
27    source_clauses: Vec<Vec<i32>>,
28    source_num_vars: usize,
29}
30
31impl ReductionResult for Reduction3SATToKClique {
32    type Source = KSatisfiability<K3>;
33    type Target = KClique<SimpleGraph>;
34
35    fn target_problem(&self) -> &Self::Target {
36        &self.target
37    }
38
39    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
40        let n = self.source_num_vars;
41        // Start with all variables unset (false = 0).
42        let mut assignment = vec![0usize; n];
43        // Track which variables have been explicitly set by a clique vertex.
44        let mut set = vec![false; n];
45
46        for (v, &val) in target_solution.iter().enumerate() {
47            if val != 1 {
48                continue;
49            }
50            // Vertex v corresponds to clause j, position p.
51            let j = v / 3;
52            let p = v % 3;
53            let lit = self.source_clauses[j][p];
54            let var_idx = (lit.unsigned_abs() as usize) - 1; // 0-indexed
55            if !set[var_idx] {
56                assignment[var_idx] = if lit > 0 { 1 } else { 0 };
57                set[var_idx] = true;
58            }
59        }
60        assignment
61    }
62}
63
64/// Check whether two literals are contradictory (one is the negation of the other).
65fn literals_contradict(lit1: i32, lit2: i32) -> bool {
66    lit1 == -lit2
67}
68
69#[reduction(
70    overhead = {
71        num_vertices = "3 * num_clauses",
72        num_edges = "9 * num_clauses * (num_clauses - 1) / 2",
73        k = "num_clauses",
74    }
75)]
76impl ReduceTo<KClique<SimpleGraph>> for KSatisfiability<K3> {
77    type Result = Reduction3SATToKClique;
78
79    fn reduce_to(&self) -> Self::Result {
80        let m = self.num_clauses();
81        let num_verts = 3 * m;
82
83        // Collect literals for each clause for easy access.
84        let clause_lits: Vec<Vec<i32>> =
85            self.clauses().iter().map(|c| c.literals.clone()).collect();
86
87        // Build edges: connect (j1,p1) and (j2,p2) if j1 != j2 and literals
88        // are not contradictory.
89        let mut edges = Vec::new();
90        for j1 in 0..m {
91            for j2 in (j1 + 1)..m {
92                for p1 in 0..3 {
93                    for p2 in 0..3 {
94                        let lit1 = clause_lits[j1][p1];
95                        let lit2 = clause_lits[j2][p2];
96                        if !literals_contradict(lit1, lit2) {
97                            let v1 = 3 * j1 + p1;
98                            let v2 = 3 * j2 + p2;
99                            edges.push((v1, v2));
100                        }
101                    }
102                }
103            }
104        }
105
106        let graph = SimpleGraph::new(num_verts, edges);
107        let target = KClique::new(graph, m);
108
109        Reduction3SATToKClique {
110            target,
111            source_clauses: clause_lits,
112            source_num_vars: self.num_vars(),
113        }
114    }
115}
116
117#[cfg(feature = "example-db")]
118pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
119    use crate::export::SolutionPair;
120    use crate::models::formula::CNFClause;
121
122    vec![crate::example_db::specs::RuleExampleSpec {
123        id: "ksatisfiability_to_kclique",
124        build: || {
125            // (x1 ∨ x2 ∨ x3) ∧ (¬x1 ∨ ¬x2 ∨ x3), n=3, m=2
126            let source = KSatisfiability::<K3>::new(
127                3,
128                vec![
129                    CNFClause::new(vec![1, 2, 3]),
130                    CNFClause::new(vec![-1, -2, 3]),
131                ],
132            );
133            // x1=F, x2=F, x3=T satisfies both clauses.
134            // Clause 0: pick literal x3 (position 2) → vertex 2
135            // Clause 1: pick literal ¬x1 (position 0) → vertex 3
136            // Target config: 6 vertices, vertices 2 and 3 selected.
137            crate::example_db::specs::rule_example_with_witness::<_, KClique<SimpleGraph>>(
138                source,
139                SolutionPair {
140                    source_config: vec![0, 0, 1],
141                    target_config: vec![0, 0, 1, 1, 0, 0],
142                },
143            )
144        },
145    }]
146}
147
148#[cfg(test)]
149#[path = "../unit_tests/rules/ksatisfiability_kclique.rs"]
150mod tests;
problemreductions/rules/ksatisfiability_kclique.rs

problemreductions/rules/
ksatisfiability_kclique.rs
