problemreductions/rules/
kclique_conjunctivebooleanquery.rs

1//! Reduction from KClique to ConjunctiveBooleanQuery.
2//!
3//! Given a KClique instance (G=(V,E), k):
4//! 1. Domain D = V (n elements, indexed 0..n-1).
5//! 2. Single binary relation R with tuples: for each edge {u,v}∈E, include both
6//!    (u,v) and (v,u). So 2|E| tuples, each of arity 2.
7//! 3. Query: k existential variables, with conjuncts R(y_i, y_j) for all 0≤i<j<k.
8//!    That's k*(k-1)/2 conjuncts.
9//! 4. G has a k-clique if and only if the query evaluates to true.
10
11use crate::models::graph::KClique;
12use crate::models::misc::{CbqRelation, ConjunctiveBooleanQuery, QueryArg};
13use crate::reduction;
14use crate::rules::traits::{ReduceTo, ReductionResult};
15use crate::topology::{Graph, SimpleGraph};
16
17/// Result of reducing KClique to ConjunctiveBooleanQuery.
18#[derive(Debug, Clone)]
19pub struct ReductionKCliqueToCBQ {
20    target: ConjunctiveBooleanQuery,
21    num_vertices: usize,
22}
23
24impl ReductionResult for ReductionKCliqueToCBQ {
25    type Source = KClique<SimpleGraph>;
26    type Target = ConjunctiveBooleanQuery;
27
28    fn target_problem(&self) -> &ConjunctiveBooleanQuery {
29        &self.target
30    }
31
32    /// Extract solution from CBQ back to KClique.
33    ///
34    /// CBQ config: vec of length k, each value is a domain element (vertex index).
35    /// KClique config: binary vec of length n; set config[v]=1 for each v in
36    /// the CBQ assignment.
37    fn extract_solution(
38        &self,
39        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
40    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
41        crate::rules::traits::validate_target_witness(
42            self.target_problem(),
43            target_solution,
44            |value| value.0,
45            "target witness is not satisfying",
46        )?;
47
48        Ok(KClique::<SimpleGraph>::config_from_vertices(
49            self.num_vertices,
50            target_solution,
51        ))
52    }
53}
54
55#[crate::aggregate_reduction(identity)]
56impl crate::rules::AggregateReductionResult for ReductionKCliqueToCBQ {}
57
58#[reduction(
59    transform = exact {
60        domain_size = "num_vertices",
61        num_relations = "1",
62        num_variables = "k",
63        num_conjuncts = "k * (k - 1) / 2",
64    }
65)]
66impl ReduceTo<ConjunctiveBooleanQuery> for KClique<SimpleGraph> {
67    type Result = ReductionKCliqueToCBQ;
68
69    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
70        let n = self.num_vertices();
71        let k = self.k();
72
73        // Build the single binary relation: for each edge {u,v}, include (u,v) and (v,u).
74        let mut tuples = Vec::with_capacity(self.num_edges() * 2);
75        for (u, v) in self.graph().edges() {
76            // A loop must not let distinct clique variables use the same vertex.
77            if u == v {
78                continue;
79            }
80            tuples.push(vec![u, v]);
81            tuples.push(vec![v, u]);
82        }
83        let relation = CbqRelation { arity: 2, tuples };
84
85        // Build conjuncts: R(y_i, y_j) for all 0 <= i < j < k.
86        let mut conjuncts = Vec::with_capacity(k * k.saturating_sub(1) / 2);
87        for i in 0..k {
88            for j in (i + 1)..k {
89                conjuncts.push((0, vec![QueryArg::Variable(i), QueryArg::Variable(j)]));
90            }
91        }
92
93        let target = ConjunctiveBooleanQuery::new(n, vec![relation], k, conjuncts);
94
95        Ok(ReductionKCliqueToCBQ {
96            target,
97            num_vertices: n,
98        })
99    }
100}
101
102#[cfg(feature = "example-db")]
103pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
104    use crate::export::SolutionPair;
105
106    vec![crate::example_db::specs::RuleExampleSpec {
107        id: "kclique_to_conjunctivebooleanquery",
108        build: || {
109            // Triangle (0,1,2) in a 5-vertex graph, k=3 → has 3-clique
110            let source = KClique::new(
111                SimpleGraph::new(5, vec![(0, 1), (0, 2), (1, 2), (2, 3), (3, 4)]),
112                3,
113            );
114            crate::example_db::specs::rule_example_with_witness::<_, ConjunctiveBooleanQuery>(
115                source,
116                SolutionPair {
117                    source_config: serde_json::json!(vec![true, true, true, false, false]),
118                    target_config: serde_json::json!(vec![0, 1, 2]),
119                },
120            )
121        },
122    }]
123}
124
125#[cfg(test)]
126#[path = "../unit_tests/rules/kclique_conjunctivebooleanquery.rs"]
127mod tests;
problemreductions/rules/kclique_conjunctivebooleanquery.rs

problemreductions/rules/
kclique_conjunctivebooleanquery.rs
