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::One;
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: i32) -> 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}
65
66impl ReductionResult for ReductionSATToIS {
67    type Source = Satisfiability;
68    type Target = MaximumIndependentSet<SimpleGraph, One>;
69
70    fn target_problem(&self) -> &Self::Target {
71        &self.target
72    }
73
74    /// Extract a SAT solution from an MaximumIndependentSet solution.
75    ///
76    /// For each selected vertex (representing a literal), we set the corresponding
77    /// variable to make that literal true. Variables not covered by any selected
78    /// literal default to false.
79    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
80        let mut assignment = vec![0usize; self.num_source_variables];
81        let mut covered = vec![false; self.num_source_variables];
82
83        for (vertex_idx, &selected) in target_solution.iter().enumerate() {
84            if selected == 1 {
85                let literal = &self.literals[vertex_idx];
86                // If the literal is positive (neg=false), variable should be true (1)
87                // If the literal is negated (neg=true), variable should be false (0)
88                assignment[literal.name] = if literal.neg { 0 } else { 1 };
89                covered[literal.name] = true;
90            }
91        }
92
93        // Variables not covered can be assigned any value (we use 0)
94        // They are already initialized to 0
95        assignment
96    }
97}
98
99impl ReductionSATToIS {
100    /// Get the number of clauses in the source SAT problem.
101    pub fn num_clauses(&self) -> usize {
102        self.num_clauses
103    }
104
105    /// Get a reference to the literals mapping.
106    pub fn literals(&self) -> &[BoolVar] {
107        &self.literals
108    }
109}
110
111#[reduction(
112    overhead = {
113        num_vertices = "num_literals",
114        num_edges = "num_literals^2",
115    }
116)]
117impl ReduceTo<MaximumIndependentSet<SimpleGraph, One>> for Satisfiability {
118    type Result = ReductionSATToIS;
119
120    fn reduce_to(&self) -> Self::Result {
121        let mut literals: Vec<BoolVar> = Vec::new();
122        let mut edges: Vec<(usize, usize)> = Vec::new();
123        let mut vertex_count = 0;
124
125        // First pass: add vertices for each literal in each clause
126        // and add clique edges within each clause
127        for clause in self.clauses() {
128            let clause_start = vertex_count;
129
130            // Add vertices for each literal in this clause
131            for &lit in &clause.literals {
132                literals.push(BoolVar::from_literal(lit));
133                vertex_count += 1;
134            }
135
136            // Add clique edges within this clause
137            for i in clause_start..vertex_count {
138                for j in (i + 1)..vertex_count {
139                    edges.push((i, j));
140                }
141            }
142        }
143
144        // Second pass: add edges between complementary literals across clauses
145        // Since we only add clique edges within clauses in the first pass,
146        // complementary literals in different clauses won't already have an edge
147        for i in 0..vertex_count {
148            for j in (i + 1)..vertex_count {
149                if literals[i].is_complement(&literals[j]) {
150                    edges.push((i, j));
151                }
152            }
153        }
154
155        let target = MaximumIndependentSet::new(
156            SimpleGraph::new(vertex_count, edges),
157            vec![One; vertex_count],
158        );
159
160        ReductionSATToIS {
161            target,
162            literals,
163            num_source_variables: self.num_vars(),
164            num_clauses: self.num_clauses(),
165        }
166    }
167}
168
169#[cfg(feature = "example-db")]
170pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
171    use crate::export::SolutionPair;
172    use crate::models::formula::CNFClause;
173
174    fn sat_seven_clause_example() -> Satisfiability {
175        Satisfiability::new(
176            5,
177            vec![
178                CNFClause::new(vec![1, 2, -3]),
179                CNFClause::new(vec![-1, 3, 4]),
180                CNFClause::new(vec![2, -4, 5]),
181                CNFClause::new(vec![-2, 3, -5]),
182                CNFClause::new(vec![1, -3, 5]),
183                CNFClause::new(vec![-1, -2, 4]),
184                CNFClause::new(vec![3, -4, -5]),
185            ],
186        )
187    }
188
189    vec![crate::example_db::specs::RuleExampleSpec {
190        id: "satisfiability_to_maximumindependentset",
191        build: || {
192            crate::example_db::specs::rule_example_with_witness::<
193                _,
194                MaximumIndependentSet<SimpleGraph, One>,
195            >(
196                sat_seven_clause_example(),
197                SolutionPair {
198                    source_config: vec![1, 1, 1, 1, 0],
199                    target_config: vec![
200                        1, 0, 0, 0, 1, 0, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0,
201                    ],
202                },
203            )
204        },
205    }]
206}
207
208#[cfg(test)]
209#[path = "../unit_tests/rules/sat_maximumindependentset.rs"]
210mod tests;
problemreductions/rules/sat_maximumindependentset.rs

problemreductions/rules/
sat_maximumindependentset.rs
