diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 88cd07556..a3906113b 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -12189,6 +12189,76 @@ where $P$ is a penalty weight large enough that any constraint violation costs m _Solution extraction._ For each vertex $v$, find $c$ with $x_(v,c) = 1$. ] +#let kc_sat = load-example("KColoring", "Satisfiability") +#let kc_sat_sol = kc_sat.solutions.at(0) +#let kc_sat_n = graph-num-vertices(kc_sat.source.instance) +#let kc_sat_m = graph-num-edges(kc_sat.source.instance) +#let kc_sat_k = kc_sat.source.instance.num_colors +#let kc_sat_num_vars = kc_sat.target.instance.num_vars +#let kc_sat_num_clauses = sat-num-clauses(kc_sat.target.instance) +#let kc_sat_num_literals = kc_sat.target.instance.clauses.map(c => c.literals.len()).sum() +#reduction-rule("KColoring", "Satisfiability", + example: true, + example-caption: [Five-cycle ($n = #kc_sat_n$, $|E| = #kc_sat_m$) with $k = #kc_sat_k$ colors], + extra: [ + #pred-commands( + "pred create --example " + problem-spec(kc_sat.source) + " -o kcoloring.json", + "pred reduce kcoloring.json --to " + target-spec(kc_sat) + " -o bundle.json", + "pred solve bundle.json", + "pred evaluate kcoloring.json --config " + kc_sat_sol.source_config.map(str).join(","), + ) + + #{ + let edges = kc_sat.source.instance.graph.edges + let vertices = range(kc_sat_n).map(i => { + let angle = -calc.pi / 2 + 2 * calc.pi * i / kc_sat_n + (1.15 * calc.cos(angle), 1.15 * calc.sin(angle)) + }) + let fills = kc_sat_sol.source_config.map(c => graph-colors.at(c)) + align(center, canvas(length: 0.8cm, { + for (u, v) in edges { g-edge(vertices.at(u), vertices.at(v)) } + for (v, pos) in vertices.enumerate() { + g-node(pos, name: str(v), fill: fills.at(v), label: str(v)) + } + })) + } + + *Step 1 -- Start from the source cycle.* The fixture supplies $C_#kc_sat_n$ with edges #kc_sat.source.instance.graph.edges.map(e => $paren.l #e.at(0), #e.at(1) paren.r$).join(", ") and $k = #kc_sat_k$. Its stored proper coloring is $(#kc_sat_sol.source_config.map(str).join(", "))$, shown above. With only two colors, alternating colors around this odd cycle would force the last edge to have equal-colored endpoints, so the same $C_#kc_sat_n$ instance with $k=2$ is infeasible. + + *Step 2 -- Create assignment variables.* Each vertex-color pair receives one Boolean variable. The fixture therefore has $n k = #kc_sat_n times #kc_sat_k = #kc_sat_num_vars$ variables, ordered in vertex blocks as $x_(0,0), x_(0,1), x_(0,2), dots.c, x_(4,2)$. SAT literal $x_(v,c)$ has one-based index $v k + c + 1$. + + *Step 3 -- Emit the three clause families.* The construction creates #kc_sat_n at-least-one clauses, $n k(k-1)/2 = #(kc_sat_n * kc_sat_k * (kc_sat_k - 1) / 2)$ pairwise at-most-one clauses, and $m k = #(kc_sat_m * kc_sat_k)$ edge clauses. Altogether the fixture contains #kc_sat_num_clauses clauses and #kc_sat_num_literals literal occurrences: $#kc_sat_n$ clauses of length $#kc_sat_k$ and $#(kc_sat_num_clauses - kc_sat_n)$ binary clauses. + + *Step 4 -- Verify the target assignment.* One-hot encoding $(#kc_sat_sol.source_config.map(str).join(", "))$ gives the Boolean vector of length #kc_sat_num_vars, namely $(#kc_sat_sol.target_config.map(str).join(", "))$. Every vertex block has exactly one 1, so all at-least-one and at-most-one clauses hold. Each cycle edge joins different selected colors, so every edge clause holds. Extracting the position of the 1 in each block returns $(#kc_sat_sol.source_config.map(str).join(", "))$ #sym.checkmark. + + *Multiplicity:* The fixture stores one canonical witness. The pairwise clauses force exactly one true bit per vertex, so encoding and extraction give a bijection between proper labeled colorings and satisfying assignments. In particular, $C_5$ has $(k-1)^5-(k-1) = 30$ proper colorings for $k=3$, hence 30 satisfying assignments; this count follows from the cycle chromatic polynomial, not from the fixture length. + ], +)[ + This $O(n k^2 + m k)$ assignment-variable reduction uses $n k$ Boolean variables and emits at-least-one, pairwise at-most-one, and edge-conflict clauses. The assignment variables and the first and third clause families are the standard assignment encoding in @faber_et_al:LIPIcs.SAT.2024.12[Section 2.2]; the repository uses the pairwise (binomial) at-most-one encoding rather than the sequential encoding analyzed there. +][ + _Construction._ Let $G = (V,E)$ be the stored undirected graph, with vertices $V = {0, dots, n-1}$, stored edge sequence $E$, and available colors $C = {0, dots, k-1}$. Introduce a Boolean variable $x_(v,c)$ for every $(v,c) in V times C$. The CNF formula is the conjunction of three clause families: + $ + or.big_(c in C) x_(v,c) & quad forall v in V, \ + not x_(v,a) or not x_(v,b) & quad forall v in V, thin a,b in C, thin a < b, \ + not x_(u,c) or not x_(v,c) & quad forall (u,v) in E, thin c in C. + $ + The first family selects at least one color, the second selects at most one, and the third forbids equal colors across every stored edge. The exact output has + $ + N &= n k, \ + M &= n + n k(k-1)/2 + m k, \ + L &= n k + n k(k-1) + 2 m k + $ + variables, clauses, and literal occurrences, respectively, where $m$ is the length of the stored edge sequence. + + _Correctness._ ($arrow.r.double$) Let $c: V -> C$ be a proper coloring. Set $x_(v,c(v)) = 1$ and all other $x_(v,d) = 0$. Every vertex then satisfies its at-least-one clause, no vertex violates a pairwise at-most-one clause, and properness gives $c(u) eq.not c(v)$ for each stored edge $(u,v)$, so no edge clause has both literals false. Hence the CNF is satisfiable. ($arrow.l.double$) Conversely, let $bold(x)$ satisfy the CNF. For every vertex, the at-least-one clause supplies some true $x_(v,c)$, while the pairwise at-most-one clauses make that color unique. Define $c(v)$ to be this unique color. For every stored edge $(u,v)$ and every color $d$, the edge clause forbids $x_(u,d) = x_(v,d) = 1$; therefore $c(u) eq.not c(v)$ and $c$ is proper. + + _Variable mapping._ The zero-based source pair $(v,c)$ occupies target configuration position $v k + c$ and signed SAT literal index $v k + c + 1$. Positive literals denote selection; negative literals denote non-selection. + + _Solution extraction._ Partition a satisfying assignment into $n$ consecutive blocks of length $k$ and return, for each vertex, the position of its unique 1. + + _Repository edge-case semantics._ The literature presentation assumes $k > 0$ and a loop-free graph. The same clauses cover the repository's full stored-graph domain without separate cases. When $n=k=0$, the empty CNF is satisfiable and extracts the empty coloring. When $n>0$ and $k=0$, every vertex contributes an empty at-least-one clause, making the formula unsatisfiable. A self-loop contributes $not x_(v,c) or not x_(v,c)$ for every color and therefore makes a positive-$k$ instance infeasible. Parallel edges deliberately duplicate their edge clauses but do not change satisfiability. Isolated vertices, disconnected components, and $k>n$ require no modification. +] + #reduction-rule("MaximumSetPacking", "QUBO")[ Set packing selects mutually disjoint sets of maximum total weight. Two sets conflict if and only if they share a universe element — the same adjacency structure as an independent set on the _intersection graph_. This reduction builds the intersection graph implicitly and applies the IS penalty method directly: each set becomes a QUBO variable, diagonal entries reward selection, and off-diagonal entries penalize pairs of overlapping sets with a penalty large enough to forbid any overlap. ][ diff --git a/docs/paper/references.bib b/docs/paper/references.bib index 186f70de2..bdda1e85c 100644 --- a/docs/paper/references.bib +++ b/docs/paper/references.bib @@ -2143,3 +2143,20 @@ @article{berlekampMcElieceTilborg1978 doi = {10.1109/TIT.1978.1055873} } +@inproceedings{faber_et_al:LIPIcs.SAT.2024.12, + author = {Faber, Daniel and Jabrayilov, Adalat and Mutzel, Petra}, + title = {{SAT Encoding of Partial Ordering Models for Graph Coloring Problems}}, + booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, + pages = {12:1--12:20}, + series = {Leibniz International Proceedings in Informatics (LIPIcs)}, + isbn = {978-3-95977-334-8}, + issn = {1868-8969}, + year = {2024}, + volume = {305}, + editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik}, + address = {Dagstuhl, Germany}, + url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.12}, + urn = {urn:nbn:de:0030-drops-205340}, + doi = {10.4230/LIPIcs.SAT.2024.12} +} diff --git a/src/rules/kcoloring_satisfiability.rs b/src/rules/kcoloring_satisfiability.rs new file mode 100644 index 000000000..922d816a9 --- /dev/null +++ b/src/rules/kcoloring_satisfiability.rs @@ -0,0 +1,112 @@ +//! Reduction from graph K-Coloring to Boolean Satisfiability. + +use crate::models::formula::{CNFClause, Satisfiability}; +use crate::models::graph::KColoring; +use crate::reduction; +use crate::rules::traits::{ReduceTo, ReductionResult}; +use crate::topology::{Graph, SimpleGraph}; +use crate::variant::KN; + +/// Result of reducing K-Coloring to Satisfiability. +#[derive(Debug, Clone)] +pub struct ReductionKColoringToSatisfiability { + target: Satisfiability, + num_vertices: usize, + num_colors: usize, +} + +impl ReductionResult for ReductionKColoringToSatisfiability { + type Source = KColoring; + type Target = Satisfiability; + + fn target_problem(&self) -> &Self::Target { + &self.target + } + + fn extract_solution(&self, target_solution: &[usize]) -> Vec { + (0..self.num_vertices) + .map(|vertex| { + let start = vertex * self.num_colors; + target_solution[start..start + self.num_colors] + .iter() + .position(|&value| value == 1) + .expect("satisfying assignment must select one color per vertex") + }) + .collect() + } +} + +#[reduction( + overhead = { + num_vars = "num_vertices * num_colors", + num_clauses = "num_vertices + num_vertices * num_colors * (num_colors - 1) / 2 + num_edges * num_colors", + num_literals = "num_vertices * num_colors + num_vertices * num_colors * (num_colors - 1) + 2 * num_edges * num_colors", + } +)] +impl ReduceTo for KColoring { + type Result = ReductionKColoringToSatisfiability; + + fn reduce_to(&self) -> Self::Result { + let num_vertices = self.graph().num_vertices(); + let num_colors = self.num_colors(); + let variable = |vertex: usize, color: usize| (vertex * num_colors + color + 1) as i32; + let mut clauses = Vec::new(); + + for vertex in 0..num_vertices { + clauses.push(CNFClause::new( + (0..num_colors) + .map(|color| variable(vertex, color)) + .collect(), + )); + } + + for vertex in 0..num_vertices { + for first_color in 0..num_colors { + for second_color in first_color + 1..num_colors { + clauses.push(CNFClause::new(vec![ + -variable(vertex, first_color), + -variable(vertex, second_color), + ])); + } + } + } + + for (first_vertex, second_vertex) in self.graph().edges() { + for color in 0..num_colors { + clauses.push(CNFClause::new(vec![ + -variable(first_vertex, color), + -variable(second_vertex, color), + ])); + } + } + + ReductionKColoringToSatisfiability { + target: Satisfiability::new(num_vertices * num_colors, clauses), + num_vertices, + num_colors, + } + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + use crate::export::SolutionPair; + + vec![crate::example_db::specs::RuleExampleSpec { + id: "kcoloring_to_satisfiability", + build: || { + let source = KColoring::::with_k(SimpleGraph::cycle(5), 3); + crate::example_db::specs::rule_example_with_witness::<_, Satisfiability>( + source, + SolutionPair { + source_config: vec![0, 1, 0, 1, 2], + target_config: vec![1, 0, 0, 0, 1, 0, 1, 0, 0, 0, 1, 0, 0, 0, 1], + }, + ) + }, + }] +} + +#[cfg(test)] +#[path = "../unit_tests/rules/kcoloring_satisfiability.rs"] +mod tests; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 95eb5f477..c1d0ef5d2 100644 --- a/src/rules/mod.rs +++ b/src/rules/mod.rs @@ -53,6 +53,7 @@ pub(crate) mod kcoloring_bicliquecover; mod kcoloring_casts; pub(crate) mod kcoloring_clustering; pub(crate) mod kcoloring_partitionintocliques; +pub(crate) mod kcoloring_satisfiability; pub(crate) mod kcoloring_twodimensionalconsecutivesets; mod knapsack_qubo; pub(crate) mod ksatisfiability_acyclicpartition; @@ -464,6 +465,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec) -> ReductionKColoringToSatisfiability { + ReduceTo::::reduce_to(source) +} + +#[test] +fn test_kcoloring_to_satisfiability_closed_loop() { + let source = KColoring::::with_k(SimpleGraph::cycle(5), 3); + let reduction = reduce(&source); + + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &reduction, + "KColoring->Satisfiability closed loop", + ); +} + +#[test] +fn test_kcoloring_to_satisfiability_clause_families_and_sizes() { + let source = KColoring::::with_k(SimpleGraph::new(2, vec![(0, 1)]), 3); + let reduction = reduce(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vars(), 6); + assert_eq!(target.num_clauses(), 11); + assert_eq!(target.num_literals(), 24); + assert_eq!( + target.clauses(), + &[ + CNFClause::new(vec![1, 2, 3]), + CNFClause::new(vec![4, 5, 6]), + CNFClause::new(vec![-1, -2]), + CNFClause::new(vec![-1, -3]), + CNFClause::new(vec![-2, -3]), + CNFClause::new(vec![-4, -5]), + CNFClause::new(vec![-4, -6]), + CNFClause::new(vec![-5, -6]), + CNFClause::new(vec![-1, -4]), + CNFClause::new(vec![-2, -5]), + CNFClause::new(vec![-3, -6]), + ] + ); +} + +#[test] +fn test_kcoloring_to_satisfiability_extracts_canonical_coloring() { + let source = KColoring::::with_k(SimpleGraph::cycle(5), 3); + let reduction = reduce(&source); + let assignment = vec![1, 0, 0, 0, 1, 0, 1, 0, 0, 0, 1, 0, 0, 0, 1]; + + assert!(reduction.target_problem().evaluate(&assignment).0); + assert_eq!(reduction.extract_solution(&assignment), vec![0, 1, 0, 1, 2]); +} + +#[test] +fn test_kcoloring_to_satisfiability_five_cycle_feasibility() { + let solver = BruteForce::new(); + + let feasible = KColoring::::with_k(SimpleGraph::cycle(5), 3); + let feasible_reduction = reduce(&feasible); + assert_eq!(feasible_reduction.target_problem().num_vars(), 15); + assert_eq!(feasible_reduction.target_problem().num_clauses(), 35); + assert_eq!(feasible_reduction.target_problem().num_literals(), 75); + assert!(solver + .find_witness(feasible_reduction.target_problem()) + .is_some()); + + let infeasible = KColoring::::with_k(SimpleGraph::cycle(5), 2); + let infeasible_reduction = reduce(&infeasible); + assert_eq!(infeasible_reduction.target_problem().num_vars(), 10); + assert_eq!(infeasible_reduction.target_problem().num_clauses(), 20); + assert_eq!(infeasible_reduction.target_problem().num_literals(), 40); + assert!(solver + .find_witness(infeasible_reduction.target_problem()) + .is_none()); +} + +#[test] +fn test_kcoloring_to_satisfiability_empty_zero_colors_is_satisfiable() { + let source = KColoring::::with_k(SimpleGraph::empty(0), 0); + let reduction = reduce(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vars(), 0); + assert!(target.clauses().is_empty()); + assert_eq!(BruteForce::new().find_witness(target), Some(vec![])); + assert_eq!(reduction.extract_solution(&[]), Vec::::new()); +} + +#[test] +fn test_kcoloring_to_satisfiability_nonempty_zero_colors_is_infeasible() { + let source = KColoring::::with_k(SimpleGraph::empty(2), 0); + let reduction = reduce(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_vars(), 0); + assert_eq!( + target.clauses(), + &[CNFClause::new(vec![]), CNFClause::new(vec![])] + ); + assert!(BruteForce::new().find_witness(target).is_none()); +} + +#[test] +fn test_kcoloring_to_satisfiability_isolated_and_disconnected_vertices() { + let source = KColoring::::with_k(SimpleGraph::new(5, vec![(0, 1), (2, 3)]), 2); + let reduction = reduce(&source); + let target_solution = BruteForce::new() + .find_witness(reduction.target_problem()) + .expect("disconnected bipartite graph must be colorable"); + let source_solution = reduction.extract_solution(&target_solution); + + assert!(source.evaluate(&source_solution).0); + assert_eq!(source_solution.len(), 5); +} + +#[test] +fn test_kcoloring_to_satisfiability_self_loop_is_infeasible() { + let source = KColoring::::with_k(SimpleGraph::new(1, vec![(0, 0)]), 1); + let reduction = reduce(&source); + + assert_eq!( + reduction.target_problem().clauses(), + &[CNFClause::new(vec![1]), CNFClause::new(vec![-1, -1])] + ); + assert!(BruteForce::new() + .find_witness(reduction.target_problem()) + .is_none()); +} + +#[test] +fn test_kcoloring_to_satisfiability_parallel_edges_duplicate_conflicts() { + let source = KColoring::::with_k(SimpleGraph::new(2, vec![(0, 1), (0, 1)]), 2); + let reduction = reduce(&source); + let target = reduction.target_problem(); + + assert_eq!(target.num_clauses(), 8); + assert_eq!( + target + .clauses() + .iter() + .filter(|clause| clause.literals == vec![-1, -3]) + .count(), + 2 + ); + assert_eq!( + target + .clauses() + .iter() + .filter(|clause| clause.literals == vec![-2, -4]) + .count(), + 2 + ); +} + +#[test] +fn test_kcoloring_to_satisfiability_more_colors_than_vertices() { + let source = KColoring::::with_k(SimpleGraph::new(2, vec![(0, 1)]), 3); + let reduction = reduce(&source); + let target_solution = BruteForce::new() + .find_witness(reduction.target_problem()) + .expect("an edge is colorable with three colors"); + + assert!( + source + .evaluate(&reduction.extract_solution(&target_solution)) + .0 + ); +}