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 (STOC 1973):
4//! Nonempty short clauses are padded by literal repetition, an empty clause
5//! maps to a fixed infeasible DAG, and appearing variables are compacted with
6//! an inverse map. No ordering or distinct-variable hypothesis is needed.
7//! - Variable leaf pairs `s_pos[k], s_neg[k]` share register `S[k]`
8//! - Each literal occurrence adds `p[i,j], q[i,j], r[i,j], rbar[i,j]`
9//! - `r[i,j]` and `rbar[i,j]` share register `R[i,j]`
10//! - Clause gadgets are linked cyclically through `(q[i,1], rbar[i,2])`,
11//!   `(q[i,2], rbar[i,3])`, `(q[i,3], rbar[i,1])`
12//! - A realization yields a truth assignment by comparing the order of
13//!   `s_pos[k]` and `s_neg[k]`
14
15use crate::models::formula::KSatisfiability;
16use crate::models::misc::FeasibleRegisterAssignment;
17use crate::reduction;
18use crate::rules::traits::{ReduceTo, ReductionResult};
19use crate::variant::K3;
20use std::collections::BTreeSet;
21
22fn s_pos_idx(var: usize) -> usize {
23    var
24}
25
26fn s_neg_idx(num_vars: usize, var: usize) -> usize {
27    num_vars + var
28}
29
30fn literal_base(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize {
31    2 * num_vars + 12 * clause_idx + 4 * literal_pos
32}
33
34fn p_idx(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize {
35    literal_base(num_vars, clause_idx, literal_pos)
36}
37
38fn q_idx(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize {
39    literal_base(num_vars, clause_idx, literal_pos) + 1
40}
41
42fn r_idx(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize {
43    literal_base(num_vars, clause_idx, literal_pos) + 2
44}
45
46fn rbar_idx(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize {
47    literal_base(num_vars, clause_idx, literal_pos) + 3
48}
49
50fn p_register(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize {
51    num_vars + 3 * (3 * clause_idx + literal_pos)
52}
53
54fn q_register(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize {
55    p_register(num_vars, clause_idx, literal_pos) + 1
56}
57
58fn r_register(num_vars: usize, clause_idx: usize, literal_pos: usize) -> usize {
59    p_register(num_vars, clause_idx, literal_pos) + 2
60}
61
62#[derive(Debug, Clone)]
63pub struct Reduction3SATToFeasibleRegisterAssignment {
64    target: FeasibleRegisterAssignment,
65    num_vars: usize,
66    source_variables: Vec<usize>,
67}
68
69impl ReductionResult for Reduction3SATToFeasibleRegisterAssignment {
70    type Source = KSatisfiability<K3>;
71    type Target = FeasibleRegisterAssignment;
72
73    fn target_problem(&self) -> &Self::Target {
74        &self.target
75    }
76
77    fn extract_solution(
78        &self,
79        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
80    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
81        let value =
82            crate::rules::traits::validate_target_solution(self.target_problem(), target_solution)?;
83        if !value.0 {
84            return Err(crate::rules::ExtractionError::invalid(
85                "target configuration is not a feasible register assignment realization",
86            ));
87        }
88        let mut assignment = vec![false; self.num_vars];
89        let compact_vars = self.source_variables.len();
90        for (compact, &original) in self.source_variables.iter().enumerate() {
91            assignment[original] = target_solution[s_pos_idx(compact)]
92                < target_solution[s_neg_idx(compact_vars, compact)];
93        }
94        Ok(assignment)
95    }
96}
97
98#[reduction(
99    transform = upper_bound {
100        num_vertices = "2 * num_vars + 12 * num_clauses",
101        num_arcs = "15 * num_clauses",
102        num_registers = "num_vars + 9 * num_clauses",
103        num_same_register_pairs = "num_vars + 3 * num_clauses",
104    }
105)]
106impl ReduceTo<FeasibleRegisterAssignment> for KSatisfiability<K3> {
107    type Result = Reduction3SATToFeasibleRegisterAssignment;
108
109    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
110        if self
111            .clauses()
112            .iter()
113            .any(|clause| clause.literals.is_empty())
114        {
115            // Both predecessors must remain live until vertex 2, but they
116            // share a register. This acyclic target has no realization.
117            return Ok(Reduction3SATToFeasibleRegisterAssignment {
118                target: FeasibleRegisterAssignment::new(3, vec![(2, 0), (2, 1)], 2, vec![0, 0, 1]),
119                num_vars: self.num_vars(),
120                source_variables: Vec::new(),
121            });
122        }
123        let source_variables: Vec<_> = self
124            .clauses()
125            .iter()
126            .flat_map(|clause| clause.literals.iter())
127            .map(|literal| {
128                usize::try_from(literal.unsigned_abs()).expect("native SAT indices fit usize") - 1
129            })
130            .collect::<BTreeSet<_>>()
131            .into_iter()
132            .collect();
133        let num_vars = source_variables.len();
134        let num_clauses = self.num_clauses();
135        let overflow = |operation| {
136            crate::rules::ReductionError::integer_overflow::<Self, FeasibleRegisterAssignment>(
137                operation,
138            )
139        };
140        let variable_vertices = num_vars
141            .checked_mul(2)
142            .ok_or_else(|| overflow("counting variable leaves"))?;
143        let clause_vertices = num_clauses
144            .checked_mul(12)
145            .ok_or_else(|| overflow("counting clause vertices"))?;
146        let num_vertices = variable_vertices
147            .checked_add(clause_vertices)
148            .ok_or_else(|| overflow("counting target vertices"))?;
149        let clause_registers = num_clauses
150            .checked_mul(9)
151            .ok_or_else(|| overflow("counting clause registers"))?;
152        let num_registers = num_vars
153            .checked_add(clause_registers)
154            .ok_or_else(|| overflow("counting target registers"))?;
155        let num_arcs = num_clauses
156            .checked_mul(15)
157            .ok_or_else(|| overflow("counting target arcs"))?;
158        let mut assignment = vec![0usize; num_vertices];
159        let mut arcs = Vec::with_capacity(num_arcs);
160
161        for var in 0..num_vars {
162            assignment[s_pos_idx(var)] = var;
163            assignment[s_neg_idx(num_vars, var)] = var;
164        }
165
166        for (clause_idx, clause) in self.clauses().iter().enumerate() {
167            // Repetition preserves a nonempty disjunction. Every occurrence
168            // keeps its own gadget and register pair, even for repeated literals.
169            let mut literals = clause.literals.clone();
170            literals.resize(3, literals[0]);
171            for literal_pos in 0..3 {
172                assignment[p_idx(num_vars, clause_idx, literal_pos)] =
173                    p_register(num_vars, clause_idx, literal_pos);
174                assignment[q_idx(num_vars, clause_idx, literal_pos)] =
175                    q_register(num_vars, clause_idx, literal_pos);
176                assignment[r_idx(num_vars, clause_idx, literal_pos)] =
177                    r_register(num_vars, clause_idx, literal_pos);
178                assignment[rbar_idx(num_vars, clause_idx, literal_pos)] =
179                    r_register(num_vars, clause_idx, literal_pos);
180
181                arcs.push((
182                    q_idx(num_vars, clause_idx, literal_pos),
183                    p_idx(num_vars, clause_idx, literal_pos),
184                ));
185                arcs.push((
186                    p_idx(num_vars, clause_idx, literal_pos),
187                    r_idx(num_vars, clause_idx, literal_pos),
188                ));
189            }
190
191            arcs.push((
192                q_idx(num_vars, clause_idx, 0),
193                rbar_idx(num_vars, clause_idx, 1),
194            ));
195            arcs.push((
196                q_idx(num_vars, clause_idx, 1),
197                rbar_idx(num_vars, clause_idx, 2),
198            ));
199            arcs.push((
200                q_idx(num_vars, clause_idx, 2),
201                rbar_idx(num_vars, clause_idx, 0),
202            ));
203
204            for (literal_pos, &literal) in literals.iter().enumerate() {
205                let original = usize::try_from(literal.unsigned_abs())
206                    .expect("native SAT indices fit usize")
207                    - 1;
208                let var = source_variables
209                    .binary_search(&original)
210                    .expect("all appearing variables were collected");
211                let (literal_leaf, opposite_leaf) = if literal > 0 {
212                    (s_pos_idx(var), s_neg_idx(num_vars, var))
213                } else {
214                    (s_neg_idx(num_vars, var), s_pos_idx(var))
215                };
216                arcs.push((r_idx(num_vars, clause_idx, literal_pos), literal_leaf));
217                arcs.push((rbar_idx(num_vars, clause_idx, literal_pos), opposite_leaf));
218            }
219        }
220
221        Ok(Reduction3SATToFeasibleRegisterAssignment {
222            target: FeasibleRegisterAssignment::new(num_vertices, arcs, num_registers, assignment),
223            num_vars: self.num_vars(),
224            source_variables,
225        })
226    }
227}
228
229#[cfg(feature = "example-db")]
230pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
231    use crate::export::SolutionPair;
232    use crate::models::algebraic::ILP;
233    use crate::models::formula::CNFClause;
234    use crate::solvers::ILPSolver;
235
236    vec![crate::example_db::specs::RuleExampleSpec {
237        id: "ksatisfiability_to_feasibleregisterassignment",
238        build: || {
239            let source = KSatisfiability::<K3>::new(
240                3,
241                vec![
242                    CNFClause::new(vec![1, -2, 3]),
243                    CNFClause::new(vec![-1, 2, -3]),
244                ],
245            );
246            let to_fra =
247                <KSatisfiability<K3> as ReduceTo<FeasibleRegisterAssignment>>::reduce_to(&source)
248                    .expect("reduction should succeed");
249            let to_ilp = <FeasibleRegisterAssignment as ReduceTo<ILP<i64>>>::reduce_to(
250                to_fra.target_problem(),
251            )
252            .expect("reduction should succeed");
253            let ilp_solution = ILPSolver::new()
254                .solve(to_ilp.target_problem())
255                .expect("canonical FRA example must reduce to a feasible ILP");
256            let target_config = to_ilp.extract_solution(&ilp_solution).unwrap();
257            let source_config = to_fra.extract_solution(&target_config).unwrap();
258            crate::example_db::specs::assemble_rule_example(
259                &source,
260                to_fra.target_problem(),
261                vec![SolutionPair {
262                    source_config: serde_json::to_value(source_config)
263                        .expect("solution serialization must succeed"),
264                    target_config: serde_json::to_value(target_config)
265                        .expect("solution serialization must succeed"),
266                }],
267            )
268        },
269    }]
270}
271
272#[cfg(test)]
273#[path = "../unit_tests/rules/ksatisfiability_feasibleregisterassignment.rs"]
274mod tests;
problemreductions/rules/ksatisfiability_feasibleregisterassignment.rs

problemreductions/rules/
ksatisfiability_feasibleregisterassignment.rs
