problemreductions/rules/
satisfiability_maximum2satisfiability.rs

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

problemreductions/rules/
satisfiability_maximum2satisfiability.rs
