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::sat_helpers::SatVariableAllocator;
6use crate::rules::traits::{ReduceTo, ReductionResult};
7use crate::types::{Max, Or};
8
9/// Result of reducing SAT to MAX-2-SAT.
10#[derive(Debug, Clone)]
11pub struct ReductionSatisfiabilityToMaximum2Satisfiability {
12    target: Maximum2Satisfiability,
13    source_num_vars: usize,
14    target_score: i64,
15}
16
17impl ReductionResult for ReductionSatisfiabilityToMaximum2Satisfiability {
18    type Source = Satisfiability;
19    type Target = Maximum2Satisfiability;
20
21    fn target_problem(&self) -> &Self::Target {
22        &self.target
23    }
24
25    fn extract_solution(
26        &self,
27        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
28    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
29        let value =
30            crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
31        let certificate = crate::rules::AggregateReductionResult::extract_value(self, value);
32        if !certificate.0 {
33            return Err(crate::rules::ExtractionError::invalid(
34                "target assignment does not certify satisfiability",
35            ));
36        }
37
38        Ok(target_solution[..self.source_num_vars].to_vec())
39    }
40}
41
42impl crate::rules::AggregateReductionResult for ReductionSatisfiabilityToMaximum2Satisfiability {
43    type Source = Satisfiability;
44    type Target = Maximum2Satisfiability;
45
46    fn target_problem(&self) -> &Self::Target {
47        &self.target
48    }
49
50    fn extract_value(&self, value: Max<i64>) -> Or {
51        Or(value == Max(Some(self.target_score)))
52    }
53}
54
55fn add_normalized_clause(
56    clause: &CNFClause,
57    variables: &mut SatVariableAllocator,
58    normalized: &mut Vec<CNFClause>,
59) -> Result<(), crate::registry::ConstructionError> {
60    match clause.len() {
61        0 => {
62            let y = variables.allocate()?;
63            normalized.push(CNFClause::new(vec![y, y, y]));
64            normalized.push(CNFClause::new(vec![-y, -y, -y]));
65        }
66        1 => {
67            let l1 = clause.literals[0];
68            let allocated = variables.allocate_many(2)?;
69            let y = allocated[0];
70            let z = allocated[1];
71            normalized.push(CNFClause::new(vec![l1, y, z]));
72            normalized.push(CNFClause::new(vec![l1, y, -z]));
73            normalized.push(CNFClause::new(vec![l1, -y, z]));
74            normalized.push(CNFClause::new(vec![l1, -y, -z]));
75        }
76        2 => {
77            let l1 = clause.literals[0];
78            let l2 = clause.literals[1];
79            let y = variables.allocate()?;
80            normalized.push(CNFClause::new(vec![l1, l2, y]));
81            normalized.push(CNFClause::new(vec![l1, l2, -y]));
82        }
83        3 => normalized.push(clause.clone()),
84        k => {
85            let literals = &clause.literals;
86            let y_vars = variables.allocate_many(k - 3)?;
87
88            normalized.push(CNFClause::new(vec![literals[0], literals[1], y_vars[0]]));
89            for i in 1..k - 3 {
90                normalized.push(CNFClause::new(vec![
91                    -y_vars[i - 1],
92                    literals[i + 1],
93                    y_vars[i],
94                ]));
95            }
96            normalized.push(CNFClause::new(vec![
97                -y_vars[y_vars.len() - 1],
98                literals[k - 2],
99                literals[k - 1],
100            ]));
101        }
102    }
103    Ok(())
104}
105
106fn add_gjs_gadget(clause: &CNFClause, w: i64, target_clauses: &mut Vec<CNFClause>) {
107    let a = clause.literals[0];
108    let b = clause.literals[1];
109    let c = clause.literals[2];
110
111    target_clauses.push(CNFClause::new(vec![a, a]));
112    target_clauses.push(CNFClause::new(vec![b, b]));
113    target_clauses.push(CNFClause::new(vec![c, c]));
114    target_clauses.push(CNFClause::new(vec![w, w]));
115    target_clauses.push(CNFClause::new(vec![-a, -b]));
116    target_clauses.push(CNFClause::new(vec![-b, -c]));
117    target_clauses.push(CNFClause::new(vec![-a, -c]));
118    target_clauses.push(CNFClause::new(vec![a, -w]));
119    target_clauses.push(CNFClause::new(vec![b, -w]));
120    target_clauses.push(CNFClause::new(vec![c, -w]));
121}
122
123#[reduction(
124    aggregate = custom,
125    transform = upper_bound {
126        num_vars = "num_vars + 2 * num_literals + 4 * num_clauses",
127        num_clauses = "10 * (num_literals + 3 * num_clauses)",
128    }
129)]
130impl ReduceTo<Maximum2Satisfiability> for Satisfiability {
131    type Result = ReductionSatisfiabilityToMaximum2Satisfiability;
132
133    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
134        let mut normalized = Vec::new();
135        let mut variables =
136            SatVariableAllocator::new("Satisfiability -> Maximum2Satisfiability", self.num_vars())
137                .map_err(
138                    crate::rules::ReductionError::construction::<
139                        Satisfiability,
140                        Maximum2Satisfiability,
141                    >,
142                )?;
143
144        for clause in self.clauses() {
145            add_normalized_clause(clause, &mut variables, &mut normalized).map_err(
146                crate::rules::ReductionError::construction::<
147                    Satisfiability,
148                    Maximum2Satisfiability,
149                >,
150            )?;
151        }
152
153        let capacity =
154            normalized.len().checked_mul(10).ok_or_else(|| {
155                crate::rules::ReductionError::integer_overflow::<
156                    Satisfiability,
157                    Maximum2Satisfiability,
158                >("computing the target clause count")
159            })?;
160        let clause_count = <Self as ReduceTo<Maximum2Satisfiability>>::exact_i64(
161            capacity,
162            "representing every satisfied-clause count",
163        )?;
164        // capacity=10*M. The target value is at most 10*M, and each
165        // normalized clause contributes at most seven satisfied clauses.
166        // Dividing first guarantees this exact score stays within i64.
167        let target_score = (clause_count / 10) * 7;
168        let mut target_clauses = Vec::with_capacity(capacity);
169        for clause in &normalized {
170            let w =
171                variables.allocate().map_err(
172                    crate::rules::ReductionError::construction::<
173                        Satisfiability,
174                        Maximum2Satisfiability,
175                    >,
176                )?;
177            add_gjs_gadget(clause, w, &mut target_clauses);
178        }
179
180        let target = Maximum2Satisfiability::try_new(variables.num_vars(), target_clauses)
181            .map_err(<Self as ReduceTo<Maximum2Satisfiability>>::target_construction)?;
182
183        Ok(ReductionSatisfiabilityToMaximum2Satisfiability {
184            target,
185            source_num_vars: self.num_vars(),
186            target_score,
187        })
188    }
189}
190
191#[cfg(feature = "example-db")]
192pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
193    use crate::export::SolutionPair;
194
195    vec![crate::example_db::specs::RuleExampleSpec {
196        id: "satisfiability_to_maximum2satisfiability",
197        build: || {
198            let source = Satisfiability::new(
199                3,
200                vec![CNFClause::new(vec![1, -2, 3]), CNFClause::new(vec![-1, 2])],
201            );
202            crate::example_db::specs::rule_example_with_witness::<_, Maximum2Satisfiability>(
203                source,
204                SolutionPair {
205                    source_config: serde_json::json!(vec![true, true, true]),
206                    target_config: serde_json::json!(vec![
207                        true, true, true, false, true, false, true
208                    ]),
209                },
210            )
211        },
212    }]
213}
214
215#[cfg(test)]
216#[path = "../unit_tests/rules/satisfiability_maximum2satisfiability.rs"]
217mod tests;
problemreductions/rules/satisfiability_maximum2satisfiability.rs

problemreductions/rules/
satisfiability_maximum2satisfiability.rs
