problemreductions/rules/
ksatisfiability_feasibleregisterassignment.rs

1//! Reduction from KSatisfiability (3-SAT) to Feasible Register Assignment.
2//!
3//! This follows Sethi's Reduction 3 / Theorem 5.11:
4//! - Variable leaf pairs `s_pos[k], s_neg[k]` share register `S[k]`
5//! - Each literal occurrence adds `p[i,j], q[i,j], r[i,j], rbar[i,j]`
6//! - `r[i,j]` and `rbar[i,j]` share register `R[i,j]`
7//! - Clause gadgets are linked cyclically through `(q[i,1], rbar[i,2])`,
8//!   `(q[i,2], rbar[i,3])`, `(q[i,3], rbar[i,1])`
9//! - A realization yields a truth assignment by comparing the order of
10//!   `s_pos[k]` and `s_neg[k]`
11
12use crate::models::formula::KSatisfiability;
13use crate::models::misc::FeasibleRegisterAssignment;
14use crate::reduction;
15use crate::rules::traits::{ReduceTo, ReductionResult};
16use crate::variant::K3;
17
18fn s_pos_idx(var: usize) -> usize {
19    var
20}
21
22fn s_neg_idx(num_vars: usize, var: usize) -> usize {
23    num_vars + var
24}
25
26fn literal_base(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize {
27    2 * num_vars + 12 * clause_idx + 4 * literal_pos
28}
29
30fn p_idx(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize {
31    literal_base(num_vars, clause_idx, literal_pos)
32}
33
34fn q_idx(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize {
35    literal_base(num_vars, clause_idx, literal_pos) + 1
36}
37
38fn r_idx(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize {
39    literal_base(num_vars, clause_idx, literal_pos) + 2
40}
41
42fn rbar_idx(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize {
43    literal_base(num_vars, clause_idx, literal_pos) + 3
44}
45
46fn p_register(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize {
47    num_vars + 3 * (3 * clause_idx + literal_pos)
48}
49
50fn q_register(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize {
51    p_register(num_vars, clause_idx, literal_pos) + 1
52}
53
54fn r_register(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize {
55    p_register(num_vars, clause_idx, literal_pos) + 2
56}
57
58#[derive(Debug, Clone)]
59pub struct Reduction3SATToFeasibleRegisterAssignment {
60    target: FeasibleRegisterAssignment,
61    num_vars: usize,
62}
63
64impl ReductionResult for Reduction3SATToFeasibleRegisterAssignment {
65    type Source = KSatisfiability<K3>;
66    type Target = FeasibleRegisterAssignment;
67
68    fn target_problem(&self) -> &Self::Target {
69        &self.target
70    }
71
72    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
73        (0..self.num_vars)
74            .map(|var| {
75                usize::from(
76                    target_solution[s_pos_idx(var)]
77                        < target_solution[s_neg_idx(self.num_vars, var)],
78                )
79            })
80            .collect()
81    }
82}
83
84#[reduction(overhead = {
85    num_vertices = "2 * num_vars + 12 * num_clauses",
86    num_arcs = "15 * num_clauses",
87    num_registers = "num_vars + 9 * num_clauses",
88})]
89impl ReduceTo<FeasibleRegisterAssignment> for KSatisfiability<K3> {
90    type Result = Reduction3SATToFeasibleRegisterAssignment;
91
92    fn reduce_to(&self) -> Self::Result {
93        let num_vars = self.num_vars();
94        let num_clauses = self.num_clauses();
95        let num_vertices = 2 * num_vars + 12 * num_clauses;
96        let num_registers = num_vars + 9 * num_clauses;
97        let mut assignment = vec![0usize; num_vertices];
98        let mut arcs = Vec::with_capacity(15 * num_clauses);
99
100        for var in 0..num_vars {
101            assignment[s_pos_idx(var)] = var;
102            assignment[s_neg_idx(num_vars, var)] = var;
103        }
104
105        for (clause_idx, clause) in self.clauses().iter().enumerate() {
106            for literal_pos in 0..3 {
107                assignment[p_idx(num_vars, clause_idx, literal_pos)] =
108                    p_register(num_vars, clause_idx, literal_pos);
109                assignment[q_idx(num_vars, clause_idx, literal_pos)] =
110                    q_register(num_vars, clause_idx, literal_pos);
111                assignment[r_idx(num_vars, clause_idx, literal_pos)] =
112                    r_register(num_vars, clause_idx, literal_pos);
113                assignment[rbar_idx(num_vars, clause_idx, literal_pos)] =
114                    r_register(num_vars, clause_idx, literal_pos);
115
116                arcs.push((
117                    q_idx(num_vars, clause_idx, literal_pos),
118                    p_idx(num_vars, clause_idx, literal_pos),
119                ));
120                arcs.push((
121                    p_idx(num_vars, clause_idx, literal_pos),
122                    r_idx(num_vars, clause_idx, literal_pos),
123                ));
124            }
125
126            arcs.push((
127                q_idx(num_vars, clause_idx, 0),
128                rbar_idx(num_vars, clause_idx, 1),
129            ));
130            arcs.push((
131                q_idx(num_vars, clause_idx, 1),
132                rbar_idx(num_vars, clause_idx, 2),
133            ));
134            arcs.push((
135                q_idx(num_vars, clause_idx, 2),
136                rbar_idx(num_vars, clause_idx, 0),
137            ));
138
139            for (literal_pos, &literal) in clause.literals.iter().enumerate() {
140                let var = literal.unsigned_abs() as usize - 1;
141                let (literal_leaf, opposite_leaf) = if literal > 0 {
142                    (s_pos_idx(var), s_neg_idx(num_vars, var))
143                } else {
144                    (s_neg_idx(num_vars, var), s_pos_idx(var))
145                };
146                arcs.push((r_idx(num_vars, clause_idx, literal_pos), literal_leaf));
147                arcs.push((rbar_idx(num_vars, clause_idx, literal_pos), opposite_leaf));
148            }
149        }
150
151        Reduction3SATToFeasibleRegisterAssignment {
152            target: FeasibleRegisterAssignment::new(num_vertices, arcs, num_registers, assignment),
153            num_vars,
154        }
155    }
156}
157
158#[cfg(feature = "example-db")]
159pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
160    use crate::export::SolutionPair;
161    use crate::models::algebraic::ILP;
162    use crate::models::formula::CNFClause;
163    use crate::solvers::ILPSolver;
164
165    vec![crate::example_db::specs::RuleExampleSpec {
166        id: "ksatisfiability_to_feasibleregisterassignment",
167        build: || {
168            let source = KSatisfiability::<K3>::new(
169                3,
170                vec![
171                    CNFClause::new(vec![1, -2, 3]),
172                    CNFClause::new(vec![-1, 2, -3]),
173                ],
174            );
175            let to_fra =
176                <KSatisfiability<K3> as ReduceTo<FeasibleRegisterAssignment>>::reduce_to(&source);
177            let to_ilp = <FeasibleRegisterAssignment as ReduceTo<ILP<i32>>>::reduce_to(
178                to_fra.target_problem(),
179            );
180            let ilp_solution = ILPSolver::new()
181                .solve(to_ilp.target_problem())
182                .expect("canonical FRA example must reduce to a feasible ILP");
183            let target_config = to_ilp.extract_solution(&ilp_solution);
184            let source_config = to_fra.extract_solution(&target_config);
185            crate::example_db::specs::assemble_rule_example(
186                &source,
187                to_fra.target_problem(),
188                vec![SolutionPair {
189                    source_config,
190                    target_config,
191                }],
192            )
193        },
194    }]
195}
196
197#[cfg(test)]
198#[path = "../unit_tests/rules/ksatisfiability_feasibleregisterassignment.rs"]
199mod tests;
problemreductions/rules/ksatisfiability_feasibleregisterassignment.rs

problemreductions/rules/
ksatisfiability_feasibleregisterassignment.rs
