problemreductions/rules/

naesatisfiability_partitionintoperfectmatchings.rs

//! Reduction from NAE-Satisfiability to Partition Into Perfect Matchings.
//!
//! This implements the Schaefer-style reduction for the `K = 2` case.
//! Clauses with two literals are normalized to three literals by duplicating
//! the first literal. Longer clauses are split using auxiliary variables:
//! NAE(a,b,R) iff there exists z: NAE(a,b,z) and NAE(-z,R).

use crate::models::formula::NAESatisfiability;
use crate::models::graph::PartitionIntoPerfectMatchings;
use crate::reduction;
use crate::rules::traits::{ReduceTo, ReductionResult};
use crate::topology::SimpleGraph;

#[derive(Debug, Clone, Copy)]
struct VariableVertices {
    t: usize,
    t_prime: usize,
    f: usize,
    f_prime: usize,
}

#[derive(Debug, Clone, Copy)]
struct SignalVertices {
    s: usize,
    s_prime: usize,
}

#[derive(Debug, Clone)]
struct ClauseLayout {
    literals: [i64; 3],
    signals: [SignalVertices; 3],
    clause_vertices: [usize; 4],
}

#[derive(Debug, Clone, Copy)]
struct ChainPairVertices {
    mu: usize,
    mu_prime: usize,
}

#[derive(Debug, Clone)]
struct ReductionLayout {
    source_num_vars: usize,
    #[cfg(any(test, feature = "example-db"))]
    auxiliary_inputs: Vec<[i64; 3]>,
    variables: Vec<VariableVertices>,
    #[cfg(any(test, feature = "example-db"))]
    clauses: Vec<ClauseLayout>,
    #[cfg(any(test, feature = "example-db"))]
    positive_chains: Vec<Vec<ChainPairVertices>>,
    #[cfg(any(test, feature = "example-db"))]
    negative_chains: Vec<Vec<ChainPairVertices>>,
    num_vertices: usize,
    edges: Vec<(usize, usize)>,
}

/// Result of reducing NAE-Satisfiability to PartitionIntoPerfectMatchings.
#[derive(Debug, Clone)]
pub struct ReductionNAESATToPartitionIntoPerfectMatchings {
    target: PartitionIntoPerfectMatchings<SimpleGraph>,
    layout: ReductionLayout,
}

impl ReductionResult for ReductionNAESATToPartitionIntoPerfectMatchings {
    type Source = NAESatisfiability;
    type Target = PartitionIntoPerfectMatchings<SimpleGraph>;

    fn target_problem(&self) -> &Self::Target {
        &self.target
    }

    fn extract_solution(
        &self,
        target_solution: &<Self::Target as crate::traits::Problem>::Solution,
    ) -> crate::rules::ExtractionResult<<Self::Source as crate::traits::Problem>::Solution> {
        crate::rules::traits::validate_target_witness(
            self.target_problem(),
            target_solution,
            |value| value.0,
            "target partition is not a partition into perfect matchings",
        )?;

        Ok({
            self.layout
                .variables
                .iter()
                .take(self.layout.source_num_vars)
                .map(|variable| target_solution[variable.t] == 0)
                .collect()
        })
    }
}

impl ReductionNAESATToPartitionIntoPerfectMatchings {
    #[cfg(any(test, feature = "example-db"))]
    fn construct_target_solution(&self, source_solution: &[bool]) -> Vec<usize> {
        assert_eq!(
            source_solution.len(),
            self.layout.source_num_vars,
            "source solution has {} variables but reduction expects {}",
            source_solution.len(),
            self.layout.source_num_vars
        );

        let mut source_solution = source_solution.to_vec();
        for &[a, b, last] in &self.layout.auxiliary_inputs {
            let value = |literal: i64| {
                source_solution[literal.unsigned_abs() as usize - 1] == (literal > 0)
            };
            let z = if value(a) == value(b) {
                !value(a)
            } else {
                value(last)
            };
            source_solution.push(z);
        }

        let mut target_solution = vec![usize::MAX; self.layout.num_vertices];
        let mut true_groups = Vec::with_capacity(self.layout.variables.len());
        let mut false_groups = Vec::with_capacity(self.layout.variables.len());

        for (index, variable) in self.layout.variables.iter().enumerate() {
            let true_group = if source_solution[index] { 0 } else { 1 };
            let false_group = 1 - true_group;
            true_groups.push(true_group);
            false_groups.push(false_group);

            target_solution[variable.t] = true_group;
            target_solution[variable.t_prime] = true_group;
            target_solution[variable.f] = false_group;
            target_solution[variable.f_prime] = false_group;
        }

        for clause in &self.layout.clauses {
            for (signal, &literal) in clause.signals.iter().zip(clause.literals.iter()) {
                let variable_index = literal.unsigned_abs() as usize - 1;
                let signal_group = if literal > 0 {
                    true_groups[variable_index]
                } else {
                    false_groups[variable_index]
                };
                target_solution[signal.s] = signal_group;
                target_solution[signal.s_prime] = signal_group;
            }
        }

        for (variable_index, chain_pairs) in self.layout.positive_chains.iter().enumerate() {
            for pair in chain_pairs {
                target_solution[pair.mu] = false_groups[variable_index];
                target_solution[pair.mu_prime] = false_groups[variable_index];
            }
        }

        for (variable_index, chain_pairs) in self.layout.negative_chains.iter().enumerate() {
            for pair in chain_pairs {
                target_solution[pair.mu] = true_groups[variable_index];
                target_solution[pair.mu_prime] = true_groups[variable_index];
            }
        }

        for clause in &self.layout.clauses {
            let clause_groups = clause.signals.map(|signal| 1 - target_solution[signal.s]);
            let zero_count = clause_groups.iter().filter(|&&group| group == 0).count();
            let w3_group = match zero_count {
                1 => 0,
                2 => 1,
                _ => panic!("source assignment is not NAE-satisfying for normalized clauses"),
            };

            for (vertex, &group) in clause
                .clause_vertices
                .iter()
                .take(3)
                .zip(clause_groups.iter())
            {
                target_solution[*vertex] = group;
            }
            target_solution[clause.clause_vertices[3]] = w3_group;
        }

        assert!(
            target_solution.iter().all(|&group| group <= 1),
            "constructed target solution left some vertices unassigned"
        );

        target_solution
    }
}

fn build_layout(
    problem: &NAESatisfiability,
) -> Result<ReductionLayout, crate::registry::ConstructionError> {
    let mut allocator = crate::rules::sat_helpers::SatVariableAllocator::new(
        "NAESatisfiability -> PartitionIntoPerfectMatchings",
        problem.num_vars(),
    )?;
    let mut clauses = Vec::new();
    #[cfg(any(test, feature = "example-db"))]
    let mut auxiliary_inputs = Vec::new();
    for clause in problem.clauses() {
        let literals = &clause.literals;
        if literals.len() == 2 {
            clauses.push([literals[0], literals[0], literals[1]]);
            continue;
        }
        let mut first = literals[0];
        for &middle in &literals[1..literals.len() - 2] {
            let auxiliary = allocator.allocate()?;
            #[cfg(any(test, feature = "example-db"))]
            auxiliary_inputs.push([first, middle, literals[literals.len() - 1]]);
            clauses.push([first, middle, auxiliary]);
            first = -auxiliary;
        }
        clauses.push([
            first,
            literals[literals.len() - 2],
            literals[literals.len() - 1],
        ]);
    }
    let num_clauses = clauses.len();
    let num_vars = allocator.num_vars();

    let mut next_vertex = 0usize;
    let mut edges = Vec::with_capacity(3 * num_vars + 21 * num_clauses);
    let mut variables = Vec::with_capacity(num_vars);

    for _ in 0..num_vars {
        let variable = VariableVertices {
            t: next_vertex,
            t_prime: next_vertex + 1,
            f: next_vertex + 2,
            f_prime: next_vertex + 3,
        };
        next_vertex += 4;

        edges.push((variable.t, variable.t_prime));
        edges.push((variable.f, variable.f_prime));
        edges.push((variable.t, variable.f));
        variables.push(variable);
    }

    let mut clause_layouts = Vec::with_capacity(num_clauses);

    for &literals in &clauses {
        let mut signals = [SignalVertices { s: 0, s_prime: 0 }; 3];
        for (literal_index, _) in literals.iter().enumerate() {
            signals[literal_index] = SignalVertices {
                s: next_vertex,
                s_prime: next_vertex + 1,
            };
            next_vertex += 2;
            edges.push((signals[literal_index].s, signals[literal_index].s_prime));
        }

        clause_layouts.push(ClauseLayout {
            literals,
            signals,
            clause_vertices: [0; 4],
        });
    }

    for clause_layout in &mut clause_layouts {
        let clause_vertices = [
            next_vertex,
            next_vertex + 1,
            next_vertex + 2,
            next_vertex + 3,
        ];
        next_vertex += 4;

        for a in 0..4 {
            for b in (a + 1)..4 {
                edges.push((clause_vertices[a], clause_vertices[b]));
            }
        }
        for (literal_index, &clause_vertex) in clause_vertices.iter().enumerate().take(3) {
            edges.push((clause_layout.signals[literal_index].s, clause_vertex));
        }
        clause_layout.clause_vertices = clause_vertices;
    }

    let mut positive_occurrences: Vec<Vec<(usize, usize)>> = vec![Vec::new(); num_vars];
    let mut negative_occurrences: Vec<Vec<(usize, usize)>> = vec![Vec::new(); num_vars];
    for (clause_index, clause_layout) in clause_layouts.iter().enumerate() {
        for (literal_index, &literal) in clause_layout.literals.iter().enumerate() {
            let variable_index = literal.unsigned_abs() as usize - 1;
            if literal > 0 {
                positive_occurrences[variable_index].push((clause_index, literal_index));
            } else {
                negative_occurrences[variable_index].push((clause_index, literal_index));
            }
        }
    }

    let mut positive_chains: Vec<Vec<ChainPairVertices>> = vec![Vec::new(); num_vars];
    let mut negative_chains: Vec<Vec<ChainPairVertices>> = vec![Vec::new(); num_vars];

    for variable_index in 0..num_vars {
        let mut source_vertex = variables[variable_index].t;
        for &(clause_index, literal_index) in &positive_occurrences[variable_index] {
            let pair = ChainPairVertices {
                mu: next_vertex,
                mu_prime: next_vertex + 1,
            };
            next_vertex += 2;

            let signal_vertex = clause_layouts[clause_index].signals[literal_index].s;
            edges.push((pair.mu, pair.mu_prime));
            edges.push((source_vertex, pair.mu));
            edges.push((signal_vertex, pair.mu));
            positive_chains[variable_index].push(pair);
            source_vertex = signal_vertex;
        }

        let mut source_vertex = variables[variable_index].f;
        for &(clause_index, literal_index) in &negative_occurrences[variable_index] {
            let pair = ChainPairVertices {
                mu: next_vertex,
                mu_prime: next_vertex + 1,
            };
            next_vertex += 2;

            let signal_vertex = clause_layouts[clause_index].signals[literal_index].s;
            edges.push((pair.mu, pair.mu_prime));
            edges.push((source_vertex, pair.mu));
            edges.push((signal_vertex, pair.mu));
            negative_chains[variable_index].push(pair);
            source_vertex = signal_vertex;
        }
    }

    Ok(ReductionLayout {
        source_num_vars: problem.num_vars(),
        #[cfg(any(test, feature = "example-db"))]
        auxiliary_inputs,
        variables,
        #[cfg(any(test, feature = "example-db"))]
        clauses: clause_layouts,
        #[cfg(any(test, feature = "example-db"))]
        positive_chains,
        #[cfg(any(test, feature = "example-db"))]
        negative_chains,
        num_vertices: next_vertex,
        edges,
    })
}

#[crate::aggregate_reduction(identity)]
impl crate::rules::AggregateReductionResult for ReductionNAESATToPartitionIntoPerfectMatchings {}

#[reduction(
    transform = upper_bound {
        num_vertices = "4 * num_vars + 20 * num_literals - 24 * num_clauses",
        num_edges = "3 * num_vars + 24 * num_literals - 27 * num_clauses",
        num_matchings = "2",
    }
)]
impl ReduceTo<PartitionIntoPerfectMatchings<SimpleGraph>> for NAESatisfiability {
    type Result = ReductionNAESATToPartitionIntoPerfectMatchings;

    fn reduce_to(&self) -> Result<Self::Result, crate::rules::ReductionError> {
        let layout = build_layout(self).map_err(
            <Self as ReduceTo<PartitionIntoPerfectMatchings<SimpleGraph>>>::target_construction,
        )?;
        let target = PartitionIntoPerfectMatchings::new(
            SimpleGraph::new(layout.num_vertices, layout.edges.clone()),
            2,
        );

        Ok(ReductionNAESATToPartitionIntoPerfectMatchings { target, layout })
    }
}

#[cfg(feature = "example-db")]
pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
    use crate::export::SolutionPair;
    use crate::models::formula::CNFClause;

    vec![crate::example_db::specs::RuleExampleSpec {
        id: "naesatisfiability_to_partitionintoperfectmatchings",
        build: || {
            let source = NAESatisfiability::new(
                3,
                vec![
                    CNFClause::new(vec![1, 2, 3]),
                    CNFClause::new(vec![-1, 2, -3]),
                ],
            );
            let source_config = vec![true, true, false];
            let reduction =
                ReduceTo::<PartitionIntoPerfectMatchings<SimpleGraph>>::reduce_to(&source)
                    .expect("reduction should succeed");
            let target_config = reduction.construct_target_solution(&source_config);

            crate::example_db::specs::assemble_rule_example(
                &source,
                reduction.target_problem(),
                vec![SolutionPair {
                    source_config: serde_json::to_value(source_config)
                        .expect("solution serialization must succeed"),
                    target_config: serde_json::to_value(target_config)
                        .expect("solution serialization must succeed"),
                }],
            )
        },
    }]
}

#[cfg(test)]
#[path = "../unit_tests/rules/naesatisfiability_partitionintoperfectmatchings.rs"]
mod tests;