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        crate::rules::traits::validate_target_witness(
37            self.target_problem(),
38            target_solution,
39            |value| value.0,
40            "target selection is not a clique meeting the threshold",
41        )?;
42        // Variables absent from the selected literals are free; choose false.
43        let mut assignment = vec![false; self.source_num_vars];
44        for (&selected, &(variable, positive)) in target_solution[..self.literal_assignments.len()]
45            .iter()
46            .zip(&self.literal_assignments)
47        {
48            if selected {
49                assignment[variable] = positive;
50            }
51        }
52        Ok(assignment)
53    }
54}
55
56#[crate::aggregate_reduction(identity)]
57impl crate::rules::AggregateReductionResult for Reduction3SATToKClique {}
58
59#[reduction(
60    transform = upper_bound {
61        num_vertices = "3 * num_clauses + 1",
62        k = "num_clauses + 1",
63        num_edges = "9 * num_clauses^2 + 3 * num_clauses",
64    }
65)]
66impl ReduceTo<KClique<SimpleGraph>> for KSatisfiability<K3> {
67    type Result = Reduction3SATToKClique;
68
69    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
70        let (num_vertices, k) =
71            clique_sizes(self.num_clauses(), self.clauses().iter().map(|c| c.len()))?;
72        // CNFClause::variables performs the formal literal-to-index conversion;
73        // the source constructor has already validated its range and polarity.
74        let positions: Vec<_> = self
75            .clauses()
76            .iter()
77            .enumerate()
78            .flat_map(|(clause, c)| {
79                c.variables()
80                    .into_iter()
81                    .zip(&c.literals)
82                    .map(move |(var, &lit)| (clause, var, lit > 0))
83            })
84            .collect();
85        let mut edges = Vec::new();
86        for (u, &(cu, vu, pu)) in positions.iter().enumerate() {
87            for (v, &(cv, vv, pv)) in positions.iter().enumerate().skip(u + 1) {
88                if cu != cv && (vu != vv || pu == pv) {
89                    edges.push((u, v));
90                }
91            }
92        }
93        let anchor = positions.len();
94        edges.extend((0..anchor).map(|v| (v, anchor)));
95        let target = KClique::new(SimpleGraph::new(num_vertices, edges), k);
96        Ok(Reduction3SATToKClique {
97            target,
98            literal_assignments: positions.into_iter().map(|(_, v, p)| (v, p)).collect(),
99            source_num_vars: self.num_vars(),
100        })
101    }
102}
103
104/// Check occurrence and output counts before allocating the compatibility graph.
105fn clique_sizes(
106    m: usize,
107    lengths: impl IntoIterator<Item = usize>,
108) -> Result<(usize, usize), crate::rules::ReductionError> {
109    let overflow = || {
110        crate::rules::ReductionError::integer_overflow::<KSatisfiability<K3>, KClique<SimpleGraph>>(
111            "counting SAT clique occurrences and auxiliary vertices",
112        )
113    };
114    let t = lengths
115        .into_iter()
116        .try_fold(0usize, |sum, len| sum.checked_add(len))
117        .ok_or_else(overflow)?;
118    let vertices = t.max(m).checked_add(1).ok_or_else(overflow)?;
119    // m+1 <= max(t,m)+1, whose representability was checked above.
120    Ok((vertices, m + 1))
121}
122
123#[cfg(feature = "example-db")]
124pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
125    use crate::export::SolutionPair;
126    use crate::models::formula::CNFClause;
127
128    vec![crate::example_db::specs::RuleExampleSpec {
129        id: "ksatisfiability_to_kclique",
130        build: || {
131            // (x1 ∨ x2 ∨ x3) ∧ (¬x1 ∨ ¬x2 ∨ x3), n=3, m=2
132            let source = KSatisfiability::<K3>::new(
133                3,
134                vec![
135                    CNFClause::new(vec![1, 2, 3]),
136                    CNFClause::new(vec![-1, -2, 3]),
137                ],
138            );
139            // x1=F, x2=F, x3=T satisfies both clauses.
140            // Clause 0: pick literal x3 (position 2) → vertex 2
141            // Clause 1: pick literal ¬x1 (position 0) → vertex 3
142            // Select literal vertices 2 and 3 and the universal vertex 6.
143            crate::example_db::specs::rule_example_with_witness::<_, KClique<SimpleGraph>>(
144                source,
145                SolutionPair {
146                    source_config: serde_json::json!(vec![false, false, true]),
147                    target_config: serde_json::json!(vec![
148                        false, false, true, true, false, false, true
149                    ]),
150                },
151            )
152        },
153    }]
154}
155
156#[cfg(test)]
157#[path = "../unit_tests/rules/ksatisfiability_kclique.rs"]
158mod tests;
problemreductions/rules/ksatisfiability_kclique.rs

problemreductions/rules/
ksatisfiability_kclique.rs
