problemreductions/rules/
oneinthreesatisfiability_ilp.rs

1//! One binary variable per SAT variable and one equality per exact-one clause.
2
3use crate::models::algebraic::{LinearConstraint, ObjectiveSense, ILP};
4use crate::models::formula::OneInThreeSatisfiability;
5use crate::reduction;
6use crate::rules::traits::{ReduceTo, ReductionResult};
7
8#[derive(Debug, Clone)]
9pub struct ReductionOneInThreeSatisfiabilityToILP {
10    target: ILP<bool>,
11}
12
13impl ReductionResult for ReductionOneInThreeSatisfiabilityToILP {
14    type Source = OneInThreeSatisfiability;
15    type Target = ILP<bool>;
16
17    fn target_problem(&self) -> &Self::Target {
18        &self.target
19    }
20
21    fn extract_solution(&self, solution: &Vec<i64>) -> crate::rules::ExtractionResult<Vec<bool>> {
22        crate::rules::traits::validate_target_witness(
23            self.target_problem(),
24            solution,
25            |value| value.value.is_some(),
26            "target ILP assignment does not satisfy the exact-one clauses",
27        )?;
28        Ok(solution.iter().map(|&value| value == 1).collect())
29    }
30}
31
32#[crate::aggregate_reduction(ilp_feasibility)]
33impl crate::rules::AggregateReductionResult for ReductionOneInThreeSatisfiabilityToILP {}
34
35#[reduction(transform = {
36    exact {
37        num_vars = "num_vars",
38        num_constraints = "num_clauses",
39    },
40    upper_bound {
41        num_nonzeros = "3 * num_clauses",
42        max_constraint_magnitude_bits = "2",
43    },
44})]
45impl ReduceTo<ILP<bool>> for OneInThreeSatisfiability {
46    type Result = ReductionOneInThreeSatisfiabilityToILP;
47
48    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
49        let mut constraints = Vec::new();
50        for clause in self.clauses() {
51            let mut terms = Vec::new();
52            let mut rhs = 1;
53            for (variable, &literal) in clause.variables().into_iter().zip(&clause.literals) {
54                if literal > 0 {
55                    terms.push((variable, 1));
56                } else {
57                    terms.push((variable, -1));
58                    rhs -= 1;
59                }
60            }
61            constraints.push(LinearConstraint::eq(terms, rhs));
62        }
63        let target = ILP::new(
64            self.num_vars(),
65            constraints,
66            vec![],
67            ObjectiveSense::Minimize,
68        )
69        .map_err(Self::target_construction)?;
70        Ok(Self::Result { target })
71    }
72}
73
74#[cfg(feature = "example-db")]
75pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
76    use crate::models::formula::CNFClause;
77    vec![crate::example_db::specs::RuleExampleSpec {
78        id: "oneinthreesatisfiability_to_ilp",
79        build: || {
80            let source = OneInThreeSatisfiability::new(
81                3,
82                vec![
83                    CNFClause::new(vec![1, 2, 3]),
84                    CNFClause::new(vec![-1, -2, 3]),
85                ],
86            );
87            crate::example_db::specs::rule_example_via_ilp::<_, bool>(source)
88        },
89    }]
90}
91
92#[cfg(test)]
93#[path = "../unit_tests/rules/oneinthreesatisfiability_ilp.rs"]
94mod tests;
problemreductions/rules/oneinthreesatisfiability_ilp.rs

problemreductions/rules/
oneinthreesatisfiability_ilp.rs
