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

problemreductions/rules/
sat_minimumdominatingset.rs
