problemreductions/rules/
sat_minimumdominatingset.rs

1//! Reduction from Satisfiability (SAT) to MinimumDominatingSet.
2//!
3//! The reduction follows this construction:
4//! 1. For each occurring variable x_i, create a "variable gadget" with 3 vertices:
5//!    - Vertex for positive literal x_i
6//!    - Vertex for negative literal NOT x_i
7//!    - A dummy vertex
8//!      These 3 vertices form a complete triangle (clique).
9//! 2. For each clause C_j, create a clause vertex.
10//! 3. Connect each clause vertex to the literal vertices that appear in that clause.
11//!
12//! A dominating set of size = number of occurring variables corresponds to a satisfying assignment:
13//! - Selecting the positive literal vertex means the variable is true
14//! - Selecting the negative literal vertex means the variable is false
15//! - Selecting the dummy vertex means the variable may be assigned either value
16
17use crate::models::formula::Satisfiability;
18use crate::models::graph::MinimumDominatingSet;
19use crate::reduction;
20use crate::rules::sat_maximumindependentset::BoolVar;
21use crate::rules::traits::{ReduceTo, ReductionResult};
22use crate::topology::SimpleGraph;
23use crate::types::{Min, Or};
24use std::collections::BTreeMap;
25
26/// Result of reducing Satisfiability to MinimumDominatingSet.
27///
28/// This struct contains:
29/// - The target MinimumDominatingSet problem
30/// - The number of literals (variables) in the source SAT problem
31/// - The number of clauses in the source SAT problem
32#[derive(Debug, Clone)]
33pub struct ReductionSATToDS {
34    /// The target MinimumDominatingSet problem.
35    target: MinimumDominatingSet<SimpleGraph, i64>,
36    /// The number of variables in the source SAT problem.
37    num_literals: usize,
38    /// The number of clauses in the source SAT problem.
39    num_clauses: usize,
40    /// Original variable indices mapped to dense triangle indices.
41    variables: BTreeMap<usize, usize>,
42    /// Exact minimum size certifying satisfiability.
43    target_size: i64,
44}
45
46impl ReductionResult for ReductionSATToDS {
47    type Source = Satisfiability;
48    type Target = MinimumDominatingSet<SimpleGraph, i64>;
49
50    fn target_problem(&self) -> &Self::Target {
51        &self.target
52    }
53
54    /// Extract a SAT solution from a MinimumDominatingSet solution.
55    ///
56    /// Validate a dominating set of exactly one vertex per occurring variable.
57    /// Each dense triangle starts with its positive literal; selecting it sets
58    /// that original variable true. Negative, dummy and absent variables decode
59    /// to false. The finite size certificate proves every clause is dominated
60    /// by a selected literal and no clause vertex is selected.
61    fn extract_solution(
62        &self,
63        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
64    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
65        let value =
66            crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
67        let certificate = crate::rules::AggregateReductionResult::extract_value(self, value);
68        if !certificate.0 {
69            return Err(crate::rules::ExtractionError::invalid(
70                "target dominating set does not certify satisfiability",
71            ));
72        }
73
74        let mut assignment = vec![false; self.num_literals];
75        for (&variable, &gadget) in &self.variables {
76            assignment[variable] = target_solution[3 * gadget];
77        }
78
79        Ok(assignment)
80    }
81}
82
83impl crate::rules::AggregateReductionResult for ReductionSATToDS {
84    type Source = Satisfiability;
85    type Target = MinimumDominatingSet<SimpleGraph, i64>;
86
87    fn target_problem(&self) -> &Self::Target {
88        &self.target
89    }
90
91    fn extract_value(&self, target_value: Min<i64>) -> Or {
92        Or(target_value == Min(Some(self.target_size)))
93    }
94}
95
96impl ReductionSATToDS {
97    /// Compute the graph dimensions and exact certificate before allocation.
98    fn target_dimensions(
99        num_variables: usize,
100        num_clauses: usize,
101    ) -> Result<(usize, i64), crate::rules::ReductionError> {
102        let num_vertices = num_variables
103            .checked_mul(3)
104            .and_then(|base| base.checked_add(num_clauses))
105            .ok_or_else(|| {
106                crate::rules::ReductionError::integer_overflow::<
107                    Satisfiability,
108                    MinimumDominatingSet<SimpleGraph, i64>,
109                >("counting dominating-set vertices")
110            })?;
111        // All vertices may be selected, so every count up to this total must
112        // fit the target objective, not only the optimum certificate.
113        <Satisfiability as ReduceTo<MinimumDominatingSet<SimpleGraph, i64>>>::exact_i64(
114            num_vertices,
115            "representing all dominating-set weights",
116        )?;
117        let target_size =
118            <Satisfiability as ReduceTo<MinimumDominatingSet<SimpleGraph, i64>>>::exact_i64(
119                num_variables,
120                "representing the satisfying dominating-set cardinality",
121            )?;
122        Ok((num_vertices, target_size))
123    }
124
125    /// Get the number of literals (variables) in the source SAT problem.
126    pub fn num_literals(&self) -> usize {
127        self.num_literals
128    }
129
130    /// Get the number of clauses in the source SAT problem.
131    pub fn num_clauses(&self) -> usize {
132        self.num_clauses
133    }
134}
135
136#[reduction(
137    aggregate = custom,
138    transform = upper_bound {
139        num_vertices = "3 * num_vars + num_clauses",
140        num_edges = "3 * num_vars + num_literals",
141    }
142)]
143impl ReduceTo<MinimumDominatingSet<SimpleGraph, i64>> for Satisfiability {
144    type Result = ReductionSATToDS;
145
146    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
147        // Absent variables are free in SAT and need no target gadget. Keep
148        // original indices for extraction, and assign dense indices in order.
149        let mut variables: BTreeMap<usize, usize> = self
150            .clauses()
151            .iter()
152            .flat_map(|clause| &clause.literals)
153            .map(|&literal| (BoolVar::from_literal(literal).name, 0))
154            .collect();
155        for (index, gadget) in variables.values_mut().enumerate() {
156            *gadget = index;
157        }
158        let num_variables = variables.len();
159        let num_clauses = self.num_clauses();
160        let (num_vertices, target_size) =
161            ReductionSATToDS::target_dimensions(num_variables, num_clauses)?;
162
163        let mut edges: Vec<(usize, usize)> = Vec::new();
164
165        // Step 1: Create variable gadgets
166        // For each variable i (0-indexed), vertices are at positions:
167        //   3*i: positive literal x_i
168        //   3*i+1: negative literal NOT x_i
169        //   3*i+2: dummy vertex
170        // These form a complete triangle (clique of 3)
171        for i in 0..num_variables {
172            let base = 3 * i;
173            // Add all edges of the triangle
174            edges.push((base, base + 1));
175            edges.push((base, base + 2));
176            edges.push((base + 1, base + 2));
177        }
178
179        // Step 2: Connect clause vertices to literal vertices
180        // Clause j gets vertex at position 3*num_variables + j
181        for (j, clause) in self.clauses().iter().enumerate() {
182            let clause_vertex = 3 * num_variables + j;
183
184            for &lit in &clause.literals {
185                let var = BoolVar::from_literal(lit);
186                // The literal's original index is present in the map because
187                // the map was collected from these same validated clauses.
188                let literal_vertex = 3 * variables[&var.name] + usize::from(var.neg);
189                edges.push((literal_vertex, clause_vertex));
190            }
191        }
192
193        let target = MinimumDominatingSet::new(
194            SimpleGraph::new(num_vertices, edges),
195            vec![1i64; num_vertices],
196        );
197
198        Ok(ReductionSATToDS {
199            target,
200            num_literals: self.num_vars(),
201            num_clauses,
202            variables,
203            target_size,
204        })
205    }
206}
207
208#[cfg(feature = "example-db")]
209pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
210    use crate::export::SolutionPair;
211    use crate::models::formula::CNFClause;
212
213    vec![crate::example_db::specs::RuleExampleSpec {
214        id: "satisfiability_to_minimumdominatingset",
215        build: || {
216            let source = Satisfiability::new(
217                5,
218                vec![
219                    CNFClause::new(vec![1, 2, -3]),
220                    CNFClause::new(vec![-1, 3, 4]),
221                    CNFClause::new(vec![2, -4, 5]),
222                    CNFClause::new(vec![-2, 3, -5]),
223                    CNFClause::new(vec![1, -3, 5]),
224                    CNFClause::new(vec![-1, -2, 4]),
225                    CNFClause::new(vec![3, -4, -5]),
226                ],
227            );
228            crate::example_db::specs::rule_example_with_witness::<
229                _,
230                MinimumDominatingSet<SimpleGraph, i64>,
231            >(
232                source,
233                SolutionPair {
234                    source_config: serde_json::json!(vec![true, false, true, true, true]),
235                    target_config: serde_json::json!(vec![
236                        true, false, false, false, true, false, true, false, false, true, false,
237                        false, true, false, false, false, false, false, false, false, false, false
238                    ]),
239                },
240            )
241        },
242    }]
243}
244
245#[cfg(test)]
246#[path = "../unit_tests/rules/sat_minimumdominatingset.rs"]
247mod tests;
problemreductions/rules/sat_minimumdominatingset.rs

problemreductions/rules/
sat_minimumdominatingset.rs
