problemreductions/rules/
ksatisfiability_oneinthreesatisfiability.rs

1//! Reduction from KSatisfiability (3-SAT) to One-In-Three Satisfiability.
2
3use crate::models::formula::{CNFClause, KSatisfiability, OneInThreeSatisfiability};
4use crate::reduction;
5use crate::rules::traits::{ReduceTo, ReductionResult};
6use crate::variant::K3;
7
8#[derive(Debug, Clone)]
9pub struct Reduction3SATToOneInThreeSAT {
10    source_num_vars: usize,
11    target: OneInThreeSatisfiability,
12}
13
14impl ReductionResult for Reduction3SATToOneInThreeSAT {
15    type Source = KSatisfiability<K3>;
16    type Target = OneInThreeSatisfiability;
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
27#[reduction(overhead = {
28    num_vars = "num_vars + 2 + 6 * num_clauses",
29    num_clauses = "1 + 5 * num_clauses",
30})]
31impl ReduceTo<OneInThreeSatisfiability> for KSatisfiability<K3> {
32    type Result = Reduction3SATToOneInThreeSAT;
33
34    fn reduce_to(&self) -> Self::Result {
35        let source_num_vars = self.num_vars();
36        let z_false = source_num_vars as i32 + 1;
37        let z_true = source_num_vars as i32 + 2;
38        let mut next_var = source_num_vars as i32 + 3;
39
40        let mut clauses = Vec::with_capacity(1 + 5 * self.num_clauses());
41        clauses.push(CNFClause::new(vec![z_false, z_false, z_true]));
42
43        for clause in self.clauses() {
44            let [l1, l2, l3] = clause.literals.as_slice() else {
45                unreachable!("K3 clauses must have exactly three literals");
46            };
47            let a = next_var;
48            let b = next_var + 1;
49            let c = next_var + 2;
50            let d = next_var + 3;
51            let e = next_var + 4;
52            let f = next_var + 5;
53            next_var += 6;
54
55            clauses.push(CNFClause::new(vec![*l1, a, d]));
56            clauses.push(CNFClause::new(vec![*l2, b, d]));
57            clauses.push(CNFClause::new(vec![a, b, e]));
58            clauses.push(CNFClause::new(vec![c, d, f]));
59            clauses.push(CNFClause::new(vec![*l3, c, z_false]));
60        }
61
62        let target = OneInThreeSatisfiability::new((next_var - 1) as usize, clauses);
63
64        Reduction3SATToOneInThreeSAT {
65            source_num_vars,
66            target,
67        }
68    }
69}
70
71#[cfg(feature = "example-db")]
72pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
73    use crate::export::SolutionPair;
74
75    vec![crate::example_db::specs::RuleExampleSpec {
76        id: "ksatisfiability_to_oneinthreesatisfiability",
77        build: || {
78            let source = KSatisfiability::<K3>::new(3, vec![CNFClause::new(vec![1, 2, 3])]);
79            crate::example_db::specs::rule_example_with_witness::<_, OneInThreeSatisfiability>(
80                source,
81                SolutionPair {
82                    source_config: vec![0, 0, 1],
83                    target_config: vec![0, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0],
84                },
85            )
86        },
87    }]
88}
89
90#[cfg(test)]
91#[path = "../unit_tests/rules/ksatisfiability_oneinthreesatisfiability.rs"]
92mod tests;
problemreductions/rules/ksatisfiability_oneinthreesatisfiability.rs

problemreductions/rules/
ksatisfiability_oneinthreesatisfiability.rs
