problemreductions/rules/
sat_maximumindependentset.rs

1//! Reduction from Satisfiability (SAT) to MaximumIndependentSet.
2//!
3//! The reduction creates one vertex for each literal occurrence in each clause.
4//! Edges are added:
5//! 1. Between all literals within the same clause (forming a clique per clause)
6//! 2. Between complementary literals (x and NOT x) across different clauses
7//!
8//! A satisfying assignment corresponds to an independent set of size = num_clauses,
9//! where we pick exactly one literal from each clause.
10
11use crate::models::formula::Satisfiability;
12use crate::models::graph::MaximumIndependentSet;
13use crate::reduction;
14use crate::rules::traits::{ReduceTo, ReductionResult};
15use crate::topology::SimpleGraph;
16use crate::types::{Max, One, Or};
17
18/// A literal in the SAT problem, representing a variable or its negation.
19#[derive(Debug, Clone, PartialEq, Eq)]
20pub struct BoolVar {
21    /// The variable name/index (0-indexed).
22    pub name: usize,
23    /// Whether this literal is negated.
24    pub neg: bool,
25}
26
27impl BoolVar {
28    /// Create a new literal.
29    pub fn new(name: usize, neg: bool) -> Self {
30        Self { name, neg }
31    }
32
33    /// Create a literal from a signed integer (1-indexed, as in DIMACS format).
34    /// Positive means the variable, negative means its negation.
35    pub fn from_literal(lit: i64) -> Self {
36        let name = lit.unsigned_abs() as usize - 1; // Convert to 0-indexed
37        let neg = lit < 0;
38        Self { name, neg }
39    }
40
41    /// Check if this literal is the complement of another.
42    pub fn is_complement(&self, other: &BoolVar) -> bool {
43        self.name == other.name && self.neg != other.neg
44    }
45}
46
47/// Result of reducing Satisfiability to MaximumIndependentSet.
48///
49/// This struct contains:
50/// - The target MaximumIndependentSet problem
51/// - A mapping from vertex indices to literals
52/// - The list of source variable indices
53/// - The number of clauses in the original SAT problem
54#[derive(Debug, Clone)]
55pub struct ReductionSATToIS {
56    /// The target MaximumIndependentSet problem.
57    target: MaximumIndependentSet<SimpleGraph, One>,
58    /// Mapping from vertex index to the literal it represents.
59    literals: Vec<BoolVar>,
60    /// The number of variables in the source SAT problem.
61    num_source_variables: usize,
62    /// The number of clauses in the source SAT problem.
63    num_clauses: usize,
64    /// Exact independent-set cardinality certifying satisfiability.
65    target_size: i64,
66}
67
68impl ReductionResult for ReductionSATToIS {
69    type Source = Satisfiability;
70    type Target = MaximumIndependentSet<SimpleGraph, One>;
71
72    fn target_problem(&self) -> &Self::Target {
73        &self.target
74    }
75
76    /// Extract a SAT solution from an MaximumIndependentSet solution.
77    ///
78    /// For each selected vertex (representing a literal), we set the corresponding
79    /// variable to make that literal true. Variables not covered by any selected
80    /// literal default to false.
81    fn extract_solution(
82        &self,
83        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
84    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
85        let value =
86            crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
87        let certificate = crate::rules::AggregateReductionResult::extract_value(self, value);
88        if !certificate.0 {
89            return Err(crate::rules::ExtractionError::invalid(
90                "target independent set does not certify satisfiability",
91            ));
92        }
93
94        let mut assignment = vec![false; self.num_source_variables];
95        for (literal, &selected) in self.literals.iter().zip(target_solution) {
96            if selected {
97                assignment[literal.name] = !literal.neg;
98            }
99        }
100        Ok(assignment)
101    }
102}
103
104impl crate::rules::AggregateReductionResult for ReductionSATToIS {
105    type Source = Satisfiability;
106    type Target = MaximumIndependentSet<SimpleGraph, One>;
107
108    fn target_problem(&self) -> &Self::Target {
109        &self.target
110    }
111
112    fn extract_value(&self, target_value: Max<i64>) -> Or {
113        Or(target_value == Max(Some(self.target_size)))
114    }
115}
116
117impl ReductionSATToIS {
118    /// Get the number of clauses in the source SAT problem.
119    pub fn num_clauses(&self) -> usize {
120        self.num_clauses
121    }
122
123    /// Get a reference to the literals mapping.
124    pub fn literals(&self) -> &[BoolVar] {
125        &self.literals
126    }
127}
128
129#[reduction(
130    aggregate = custom,
131    transform = upper_bound {
132        num_vertices = "num_literals",
133        num_edges = "num_literals^2",
134    }
135)]
136impl ReduceTo<MaximumIndependentSet<SimpleGraph, One>> for Satisfiability {
137    type Result = ReductionSATToIS;
138
139    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
140        let target_size = <Self as ReduceTo<MaximumIndependentSet<SimpleGraph, One>>>::exact_i64(
141            self.num_clauses(),
142            "representing the satisfying independent-set cardinality",
143        )?;
144        let mut literals: Vec<BoolVar> = Vec::new();
145        let mut edges: Vec<(usize, usize)> = Vec::new();
146
147        // First pass: add vertices for each literal in each clause
148        // and add clique edges within each clause
149        for clause in self.clauses() {
150            let clause_start = literals.len();
151
152            // Add vertices for each literal in this clause
153            for &lit in &clause.literals {
154                literals.push(BoolVar::from_literal(lit));
155            }
156
157            let vertex_count = literals.len();
158            // Add clique edges within this clause
159            for i in clause_start..vertex_count {
160                for j in (i + 1)..vertex_count {
161                    edges.push((i, j));
162                }
163            }
164        }
165
166        let vertex_count = literals.len();
167        // Add complementary-literal edges. Within a clause these may duplicate
168        // clique edges, which does not change independent-set feasibility.
169        for i in 0..vertex_count {
170            for j in (i + 1)..vertex_count {
171                if literals[i].is_complement(&literals[j]) {
172                    edges.push((i, j));
173                }
174            }
175        }
176
177        let target = MaximumIndependentSet::new(
178            SimpleGraph::new(vertex_count, edges),
179            vec![One; vertex_count],
180        );
181
182        Ok(ReductionSATToIS {
183            target,
184            literals,
185            num_source_variables: self.num_vars(),
186            num_clauses: self.num_clauses(),
187            target_size,
188        })
189    }
190}
191
192#[cfg(feature = "example-db")]
193pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
194    use crate::export::SolutionPair;
195    use crate::models::formula::CNFClause;
196
197    fn sat_seven_clause_example() -> Satisfiability {
198        Satisfiability::new(
199            5,
200            vec![
201                CNFClause::new(vec![1, 2, -3]),
202                CNFClause::new(vec![-1, 3, 4]),
203                CNFClause::new(vec![2, -4, 5]),
204                CNFClause::new(vec![-2, 3, -5]),
205                CNFClause::new(vec![1, -3, 5]),
206                CNFClause::new(vec![-1, -2, 4]),
207                CNFClause::new(vec![3, -4, -5]),
208            ],
209        )
210    }
211
212    vec![crate::example_db::specs::RuleExampleSpec {
213        id: "satisfiability_to_maximumindependentset",
214        build: || {
215            crate::example_db::specs::rule_example_with_witness::<
216                _,
217                MaximumIndependentSet<SimpleGraph, One>,
218            >(
219                sat_seven_clause_example(),
220                SolutionPair {
221                    source_config: serde_json::json!(vec![true, true, true, true, false]),
222                    target_config: serde_json::json!(vec![
223                        true, false, false, false, true, false, true, false, false, false, false,
224                        true, true, false, false, false, false, true, true, false, false
225                    ]),
226                },
227            )
228        },
229    }]
230}
231
232#[cfg(test)]
233#[path = "../unit_tests/rules/sat_maximumindependentset.rs"]
234mod tests;
problemreductions/rules/sat_maximumindependentset.rs

problemreductions/rules/
sat_maximumindependentset.rs
