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

problemreductions/rules/
sat_maximumindependentset.rs
