problemreductions/rules/
satisfiability_maximum2satisfiability.rs

1//! Reduction from Satisfiability to Maximum 2-Satisfiability.
2
3use crate::models::formula::{CNFClause, Maximum2Satisfiability, Satisfiability};
4use crate::reduction;
5use crate::rules::traits::{ReduceTo, ReductionResult};
6
7/// Result of reducing SAT to MAX-2-SAT.
8#[derive(Debug, Clone)]
9pub struct ReductionSatisfiabilityToMaximum2Satisfiability {
10    target: Maximum2Satisfiability,
11    source_num_vars: usize,
12}
13
14impl ReductionResult for ReductionSatisfiabilityToMaximum2Satisfiability {
15    type Source = Satisfiability;
16    type Target = Maximum2Satisfiability;
17
18    fn target_problem(&self) -> &Self::Target {
19        &self.target
20    }
21
22    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
23        target_solution[..self.source_num_vars].to_vec()
24    }
25}
26
27fn add_normalized_clause(clause: &CNFClause, next_var: &mut i32, normalized: &mut Vec<CNFClause>) {
28    match clause.len() {
29        0 => {
30            let y = *next_var;
31            *next_var += 1;
32            normalized.push(CNFClause::new(vec![y, y, y]));
33            normalized.push(CNFClause::new(vec![-y, -y, -y]));
34        }
35        1 => {
36            let l1 = clause.literals[0];
37            let y = *next_var;
38            let z = *next_var + 1;
39            *next_var += 2;
40            normalized.push(CNFClause::new(vec![l1, y, z]));
41            normalized.push(CNFClause::new(vec![l1, y, -z]));
42            normalized.push(CNFClause::new(vec![l1, -y, z]));
43            normalized.push(CNFClause::new(vec![l1, -y, -z]));
44        }
45        2 => {
46            let l1 = clause.literals[0];
47            let l2 = clause.literals[1];
48            let y = *next_var;
49            *next_var += 1;
50            normalized.push(CNFClause::new(vec![l1, l2, y]));
51            normalized.push(CNFClause::new(vec![l1, l2, -y]));
52        }
53        3 => normalized.push(clause.clone()),
54        k => {
55            let literals = &clause.literals;
56            let y_vars: Vec<i32> = (*next_var..*next_var + (k as i32 - 3)).collect();
57            *next_var += k as i32 - 3;
58
59            normalized.push(CNFClause::new(vec![literals[0], literals[1], y_vars[0]]));
60            for i in 1..k - 3 {
61                normalized.push(CNFClause::new(vec![
62                    -y_vars[i - 1],
63                    literals[i + 1],
64                    y_vars[i],
65                ]));
66            }
67            normalized.push(CNFClause::new(vec![
68                -y_vars[y_vars.len() - 1],
69                literals[k - 2],
70                literals[k - 1],
71            ]));
72        }
73    }
74}
75
76fn add_gjs_gadget(clause: &CNFClause, w: i32, target_clauses: &mut Vec<CNFClause>) {
77    let a = clause.literals[0];
78    let b = clause.literals[1];
79    let c = clause.literals[2];
80
81    target_clauses.push(CNFClause::new(vec![a, a]));
82    target_clauses.push(CNFClause::new(vec![b, b]));
83    target_clauses.push(CNFClause::new(vec![c, c]));
84    target_clauses.push(CNFClause::new(vec![w, w]));
85    target_clauses.push(CNFClause::new(vec![-a, -b]));
86    target_clauses.push(CNFClause::new(vec![-b, -c]));
87    target_clauses.push(CNFClause::new(vec![-a, -c]));
88    target_clauses.push(CNFClause::new(vec![a, -w]));
89    target_clauses.push(CNFClause::new(vec![b, -w]));
90    target_clauses.push(CNFClause::new(vec![c, -w]));
91}
92
93#[reduction(
94    overhead = {
95        num_vars = "num_vars + 2 * num_literals + 4 * num_clauses",
96        num_clauses = "10 * (num_literals + 3 * num_clauses)",
97    }
98)]
99impl ReduceTo<Maximum2Satisfiability> for Satisfiability {
100    type Result = ReductionSatisfiabilityToMaximum2Satisfiability;
101
102    fn reduce_to(&self) -> Self::Result {
103        let mut normalized = Vec::new();
104        let mut next_var = self.num_vars() as i32 + 1;
105
106        for clause in self.clauses() {
107            add_normalized_clause(clause, &mut next_var, &mut normalized);
108        }
109
110        let mut target_clauses = Vec::with_capacity(normalized.len() * 10);
111        for clause in &normalized {
112            let w = next_var;
113            next_var += 1;
114            add_gjs_gadget(clause, w, &mut target_clauses);
115        }
116
117        let target = Maximum2Satisfiability::new((next_var - 1) as usize, target_clauses);
118
119        ReductionSatisfiabilityToMaximum2Satisfiability {
120            target,
121            source_num_vars: self.num_vars(),
122        }
123    }
124}
125
126#[cfg(feature = "example-db")]
127pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
128    use crate::export::SolutionPair;
129
130    vec![crate::example_db::specs::RuleExampleSpec {
131        id: "satisfiability_to_maximum2satisfiability",
132        build: || {
133            let source = Satisfiability::new(
134                3,
135                vec![CNFClause::new(vec![1, -2, 3]), CNFClause::new(vec![-1, 2])],
136            );
137            crate::example_db::specs::rule_example_with_witness::<_, Maximum2Satisfiability>(
138                source,
139                SolutionPair {
140                    source_config: vec![1, 1, 1],
141                    target_config: vec![1, 1, 1, 0, 1, 0, 1],
142                },
143            )
144        },
145    }]
146}
147
148#[cfg(test)]
149#[path = "../unit_tests/rules/satisfiability_maximum2satisfiability.rs"]
150mod tests;
problemreductions/rules/satisfiability_maximum2satisfiability.rs

problemreductions/rules/
satisfiability_maximum2satisfiability.rs
