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        crate::rules::traits::validate_target_witness(
82            self.target_problem(),
83            target_solution,
84            |value| value.0,
85            "target configuration is not a feasible register assignment realization",
86        )?;
87        let mut assignment = vec![false; self.num_vars];
88        let compact_vars = self.source_variables.len();
89        for (compact, &original) in self.source_variables.iter().enumerate() {
90            assignment[original] = target_solution[s_pos_idx(compact)]
91                < target_solution[s_neg_idx(compact_vars, compact)];
92        }
93        Ok(assignment)
94    }
95}
96
97#[crate::aggregate_reduction(identity)]
98impl crate::rules::AggregateReductionResult for Reduction3SATToFeasibleRegisterAssignment {}
99
100#[reduction(
101    transform = upper_bound {
102        num_vertices = "2 * num_vars + 12 * num_clauses",
103        num_arcs = "15 * num_clauses",
104        num_registers = "num_vars + 9 * num_clauses",
105        num_same_register_pairs = "num_vars + 3 * num_clauses",
106    }
107)]
108impl ReduceTo<FeasibleRegisterAssignment> for KSatisfiability<K3> {
109    type Result = Reduction3SATToFeasibleRegisterAssignment;
110
111    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
112        if self
113            .clauses()
114            .iter()
115            .any(|clause| clause.literals.is_empty())
116        {
117            // Both predecessors must remain live until vertex 2, but they
118            // share a register. This acyclic target has no realization.
119            return Ok(Reduction3SATToFeasibleRegisterAssignment {
120                target: FeasibleRegisterAssignment::new(3, vec![(2, 0), (2, 1)], 2, vec![0, 0, 1]),
121                num_vars: self.num_vars(),
122                source_variables: Vec::new(),
123            });
124        }
125        let source_variables: Vec<_> = self
126            .clauses()
127            .iter()
128            .flat_map(|clause| clause.literals.iter())
129            .map(|literal| {
130                usize::try_from(literal.unsigned_abs()).expect("native SAT indices fit usize") - 1
131            })
132            .collect::<BTreeSet<_>>()
133            .into_iter()
134            .collect();
135        let num_vars = source_variables.len();
136        let num_clauses = self.num_clauses();
137        let overflow = |operation| {
138            crate::rules::ReductionError::integer_overflow::<Self, FeasibleRegisterAssignment>(
139                operation,
140            )
141        };
142        let variable_vertices = num_vars
143            .checked_mul(2)
144            .ok_or_else(|| overflow("counting variable leaves"))?;
145        let clause_vertices = num_clauses
146            .checked_mul(12)
147            .ok_or_else(|| overflow("counting clause vertices"))?;
148        let num_vertices = variable_vertices
149            .checked_add(clause_vertices)
150            .ok_or_else(|| overflow("counting target vertices"))?;
151        let clause_registers = num_clauses
152            .checked_mul(9)
153            .ok_or_else(|| overflow("counting clause registers"))?;
154        let num_registers = num_vars
155            .checked_add(clause_registers)
156            .ok_or_else(|| overflow("counting target registers"))?;
157        let num_arcs = num_clauses
158            .checked_mul(15)
159            .ok_or_else(|| overflow("counting target arcs"))?;
160        let mut assignment = vec![0usize; num_vertices];
161        let mut arcs = Vec::with_capacity(num_arcs);
162
163        for var in 0..num_vars {
164            assignment[s_pos_idx(var)] = var;
165            assignment[s_neg_idx(num_vars, var)] = var;
166        }
167
168        for (clause_idx, clause) in self.clauses().iter().enumerate() {
169            // Repetition preserves a nonempty disjunction. Every occurrence
170            // keeps its own gadget and register pair, even for repeated literals.
171            let mut literals = clause.literals.clone();
172            literals.resize(3, literals[0]);
173            for literal_pos in 0..3 {
174                assignment[p_idx(num_vars, clause_idx, literal_pos)] =
175                    p_register(num_vars, clause_idx, literal_pos);
176                assignment[q_idx(num_vars, clause_idx, literal_pos)] =
177                    q_register(num_vars, clause_idx, literal_pos);
178                assignment[r_idx(num_vars, clause_idx, literal_pos)] =
179                    r_register(num_vars, clause_idx, literal_pos);
180                assignment[rbar_idx(num_vars, clause_idx, literal_pos)] =
181                    r_register(num_vars, clause_idx, literal_pos);
182
183                arcs.push((
184                    q_idx(num_vars, clause_idx, literal_pos),
185                    p_idx(num_vars, clause_idx, literal_pos),
186                ));
187                arcs.push((
188                    p_idx(num_vars, clause_idx, literal_pos),
189                    r_idx(num_vars, clause_idx, literal_pos),
190                ));
191            }
192
193            arcs.push((
194                q_idx(num_vars, clause_idx, 0),
195                rbar_idx(num_vars, clause_idx, 1),
196            ));
197            arcs.push((
198                q_idx(num_vars, clause_idx, 1),
199                rbar_idx(num_vars, clause_idx, 2),
200            ));
201            arcs.push((
202                q_idx(num_vars, clause_idx, 2),
203                rbar_idx(num_vars, clause_idx, 0),
204            ));
205
206            for (literal_pos, &literal) in literals.iter().enumerate() {
207                let original = usize::try_from(literal.unsigned_abs())
208                    .expect("native SAT indices fit usize")
209                    - 1;
210                let var = source_variables
211                    .binary_search(&original)
212                    .expect("all appearing variables were collected");
213                let (literal_leaf, opposite_leaf) = if literal > 0 {
214                    (s_pos_idx(var), s_neg_idx(num_vars, var))
215                } else {
216                    (s_neg_idx(num_vars, var), s_pos_idx(var))
217                };
218                arcs.push((r_idx(num_vars, clause_idx, literal_pos), literal_leaf));
219                arcs.push((rbar_idx(num_vars, clause_idx, literal_pos), opposite_leaf));
220            }
221        }
222
223        Ok(Reduction3SATToFeasibleRegisterAssignment {
224            target: FeasibleRegisterAssignment::new(num_vertices, arcs, num_registers, assignment),
225            num_vars: self.num_vars(),
226            source_variables,
227        })
228    }
229}
230
231#[cfg(feature = "example-db")]
232pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
233    use crate::export::SolutionPair;
234    use crate::models::algebraic::{Bounded, ILP};
235    use crate::models::formula::CNFClause;
236    use crate::solvers::ILPSolver;
237
238    vec![crate::example_db::specs::RuleExampleSpec {
239        id: "ksatisfiability_to_feasibleregisterassignment",
240        build: || {
241            let source = KSatisfiability::<K3>::new(
242                3,
243                vec![
244                    CNFClause::new(vec![1, -2, 3]),
245                    CNFClause::new(vec![-1, 2, -3]),
246                ],
247            );
248            let to_fra =
249                <KSatisfiability<K3> as ReduceTo<FeasibleRegisterAssignment>>::reduce_to(&source)
250                    .expect("reduction should succeed");
251            let to_ilp =
252                <FeasibleRegisterAssignment as ReduceTo<ILP<i64, i64, Bounded>>>::reduce_to(
253                    to_fra.target_problem(),
254                )
255                .expect("reduction should succeed");
256            let ilp_solution = ILPSolver::new()
257                .solve(to_ilp.target_problem())
258                .expect("canonical FRA example must reduce to a feasible ILP");
259            let target_config = to_ilp.extract_solution(&ilp_solution).unwrap();
260            let source_config = to_fra.extract_solution(&target_config).unwrap();
261            crate::example_db::specs::assemble_rule_example(
262                &source,
263                to_fra.target_problem(),
264                vec![SolutionPair {
265                    source_config: serde_json::to_value(source_config)
266                        .expect("solution serialization must succeed"),
267                    target_config: serde_json::to_value(target_config)
268                        .expect("solution serialization must succeed"),
269                }],
270            )
271        },
272    }]
273}
274
275#[cfg(test)]
276#[path = "../unit_tests/rules/ksatisfiability_feasibleregisterassignment.rs"]
277mod tests;
problemreductions/rules/ksatisfiability_feasibleregisterassignment.rs

problemreductions/rules/
ksatisfiability_feasibleregisterassignment.rs
