problemreductions/rules/
ksatisfiability_kclique.rs

1//! Karp's literal-compatibility construction with a universal vertex.
2//!
3//! Use actual literal occurrences, including shorter clauses accepted by
4//! KSatisfiability::new_allow_less. For m clauses and t occurrences, create
5//! max(t,m)+1 vertices and request a clique of size m+1. Vertex t is adjacent
6//! to all literal vertices; remaining padding vertices are isolated. This
7//! uniformly represents empty formulas and formulas containing empty clauses.
8
9use crate::models::formula::KSatisfiability;
10use crate::models::graph::KClique;
11use crate::reduction;
12use crate::rules::traits::{ReduceTo, ReductionResult};
13use crate::topology::SimpleGraph;
14use crate::variant::K3;
15
16/// Literal vertices carry their validated source variable index and polarity.
17#[derive(Debug, Clone)]
18pub struct Reduction3SATToKClique {
19    target: KClique<SimpleGraph>,
20    literal_assignments: Vec<(usize, bool)>,
21    source_num_vars: usize,
22}
23
24impl ReductionResult for Reduction3SATToKClique {
25    type Source = KSatisfiability<K3>;
26    type Target = KClique<SimpleGraph>;
27
28    fn target_problem(&self) -> &Self::Target {
29        &self.target
30    }
31
32    fn extract_solution(
33        &self,
34        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
35    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
36        if !crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?
37            .0
38        {
39            return Err(crate::rules::ExtractionError::invalid(
40                "target selection is not a clique meeting the threshold",
41            ));
42        }
43        // Variables absent from the selected literals are free; choose false.
44        let mut assignment = vec![false; self.source_num_vars];
45        for (&selected, &(variable, positive)) in target_solution[..self.literal_assignments.len()]
46            .iter()
47            .zip(&self.literal_assignments)
48        {
49            if selected {
50                assignment[variable] = positive;
51            }
52        }
53        Ok(assignment)
54    }
55}
56
57#[reduction(
58    transform = upper_bound {
59        num_vertices = "3 * num_clauses + 1",
60        k = "num_clauses + 1",
61        num_edges = "9 * num_clauses^2 + 3 * num_clauses",
62    }
63)]
64impl ReduceTo<KClique<SimpleGraph>> for KSatisfiability<K3> {
65    type Result = Reduction3SATToKClique;
66
67    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
68        let (num_vertices, k) =
69            clique_sizes(self.num_clauses(), self.clauses().iter().map(|c| c.len()))?;
70        // CNFClause::variables performs the formal literal-to-index conversion;
71        // the source constructor has already validated its range and polarity.
72        let positions: Vec<_> = self
73            .clauses()
74            .iter()
75            .enumerate()
76            .flat_map(|(clause, c)| {
77                c.variables()
78                    .into_iter()
79                    .zip(&c.literals)
80                    .map(move |(var, &lit)| (clause, var, lit > 0))
81            })
82            .collect();
83        let mut edges = Vec::new();
84        for (u, &(cu, vu, pu)) in positions.iter().enumerate() {
85            for (v, &(cv, vv, pv)) in positions.iter().enumerate().skip(u + 1) {
86                if cu != cv && (vu != vv || pu == pv) {
87                    edges.push((u, v));
88                }
89            }
90        }
91        let anchor = positions.len();
92        edges.extend((0..anchor).map(|v| (v, anchor)));
93        let target = KClique::new(SimpleGraph::new(num_vertices, edges), k);
94        Ok(Reduction3SATToKClique {
95            target,
96            literal_assignments: positions.into_iter().map(|(_, v, p)| (v, p)).collect(),
97            source_num_vars: self.num_vars(),
98        })
99    }
100}
101
102/// Check occurrence and output counts before allocating the compatibility graph.
103fn clique_sizes(
104    m: usize,
105    lengths: impl IntoIterator<Item = usize>,
106) -> Result<(usize, usize), crate::rules::ReductionError> {
107    let overflow = || {
108        crate::rules::ReductionError::integer_overflow::<KSatisfiability<K3>, KClique<SimpleGraph>>(
109            "counting SAT clique occurrences and auxiliary vertices",
110        )
111    };
112    let t = lengths
113        .into_iter()
114        .try_fold(0usize, |sum, len| sum.checked_add(len))
115        .ok_or_else(overflow)?;
116    let vertices = t.max(m).checked_add(1).ok_or_else(overflow)?;
117    // m+1 <= max(t,m)+1, whose representability was checked above.
118    Ok((vertices, m + 1))
119}
120
121#[cfg(feature = "example-db")]
122pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
123    use crate::export::SolutionPair;
124    use crate::models::formula::CNFClause;
125
126    vec![crate::example_db::specs::RuleExampleSpec {
127        id: "ksatisfiability_to_kclique",
128        build: || {
129            // (x1 ∨ x2 ∨ x3) ∧ (¬x1 ∨ ¬x2 ∨ x3), n=3, m=2
130            let source = KSatisfiability::<K3>::new(
131                3,
132                vec![
133                    CNFClause::new(vec![1, 2, 3]),
134                    CNFClause::new(vec![-1, -2, 3]),
135                ],
136            );
137            // x1=F, x2=F, x3=T satisfies both clauses.
138            // Clause 0: pick literal x3 (position 2) → vertex 2
139            // Clause 1: pick literal ¬x1 (position 0) → vertex 3
140            // Select literal vertices 2 and 3 and the universal vertex 6.
141            crate::example_db::specs::rule_example_with_witness::<_, KClique<SimpleGraph>>(
142                source,
143                SolutionPair {
144                    source_config: serde_json::json!(vec![false, false, true]),
145                    target_config: serde_json::json!(vec![
146                        false, false, true, true, false, false, true
147                    ]),
148                },
149            )
150        },
151    }]
152}
153
154#[cfg(test)]
155#[path = "../unit_tests/rules/ksatisfiability_kclique.rs"]
156mod tests;
problemreductions/rules/ksatisfiability_kclique.rs

problemreductions/rules/
ksatisfiability_kclique.rs
