Fix #1098: [Rule] HamiltonianCircuit to Satisfiability

docs/paper/reductions.typ

@@ -17661,6 +17661,137 @@ The following table shows concrete target-variable counts for example instances,
   _Solution extraction._ Binary-to-bounded-integer and bounded-to-general conversions preserve the assignment. Binary encoding returns $x_i = L_i + sum_j w_(i j)y_(i j)$.
 ]
 
+// HamiltonianCircuit → Satisfiability (#1098)
+#let hc_sat = load-example("HamiltonianCircuit", "Satisfiability")
+#let hc_sat_sol = hc_sat.solutions.at(0)
+#let hc_sat_n = hc_sat.source.instance.graph.num_vertices
+#let hc_sat_edges = hc_sat.source.instance.graph.edges
+#let hc_sat_m = hc_sat_edges.len()
+#let hc_sat_clauses = hc_sat.target.instance.clauses.map(c => c.literals)
+#let hc_sat_lit(v, p) = v * hc_sat_n + p + 1
+#let hc_sat_adj(u, v) = hc_sat_edges.any(e => (e.at(0) == u and e.at(1) == v) or (e.at(0) == v and e.at(1) == u))
+#assert(hc_sat_n == 5 and hc_sat_m == hc_sat_n + 1)
+#assert(hc_sat_adj(0, 2) and not hc_sat_adj(0, 3))
+#assert(hc_sat_sol.source_config.sorted() == range(hc_sat_n))
+#assert(range(hc_sat_n).all(p => hc_sat_adj(hc_sat_sol.source_config.at(p), hc_sat_sol.source_config.at(calc.rem(p + 1, hc_sat_n)))))
+#assert(hc_sat_sol.target_config.len() == hc_sat_n * hc_sat_n)
+#assert(hc_sat.target.instance.num_vars == hc_sat_n * hc_sat_n)
+#assert(hc_sat_clauses.len() == 2 * hc_sat_n + hc_sat_n * hc_sat_n * (hc_sat_n - 1) + hc_sat_n * (hc_sat_n * hc_sat_n - 2 * hc_sat_m))
+#assert(hc_sat_clauses.fold(0, (count, c) => count + c.len()) == 4 * calc.pow(hc_sat_n, 3) - 4 * hc_sat_n * hc_sat_m)
+#assert(range(hc_sat_n).all(v => range(hc_sat_n).all(p => hc_sat_sol.target_config.at(v * hc_sat_n + p) == (hc_sat_sol.source_config.at(p) == v))))
+#assert(hc_sat_clauses.all(c => c.any(l => hc_sat_sol.target_config.at(calc.abs(l) - 1) == (l > 0))))
+#reduction-rule("HamiltonianCircuit", "Satisfiability",
+  example: true,
+  example-caption: [A cycle with one chord encoded by a vertex-position matrix],
+  extra: [
+    #pred-commands(
+      "pred create --example " + rule-spec(hc_sat) + " -o circuit.json",
+      "pred reduce circuit.json --via route.json -o bundle.json",
+      "pred solve bundle.json",
+      "pred evaluate circuit.json --config " + cli-config(hc_sat_sol.source_config),
+    )
+    #{
+      let positions = range(hc_sat_n).map(i => {
+        let a = 90deg - i * 360deg / hc_sat_n
+        (2 * calc.cos(a), 2 * calc.sin(a))
+      })
+      align(center, canvas(length: 0.65cm, {
+        for e in hc_sat_edges { g-edge(positions.at(e.at(0)), positions.at(e.at(1))) }
+        for (v, pos) in positions.enumerate() { g-node(pos, name: str(v), label: str(v)) }
+      }))
+    }
+
+    *YES example.* The loaded graph has $n = #hc_sat_n$ vertices and
+    $m = #hc_sat_m$ edges, namely
+    #hc_sat_edges.map(e => $(#e.at(0), #e.at(1))$).join(", ").
+    Its stored circuit is $[#fmt-values(hc_sat_sol.source_config)]$.
+    There are $#hc_sat.target.instance.num_vars = n^2$ variables.
+    The positive clauses contribute $#(2 * hc_sat_n)$ clauses and
+    $#(2 * hc_sat_n * hc_sat_n)$ literals; the pairwise exclusions contribute
+    $#(hc_sat_n * hc_sat_n * (hc_sat_n - 1))$ clauses and
+    $#(2 * hc_sat_n * hc_sat_n * (hc_sat_n - 1))$ literals.
+    The $#(hc_sat_n * hc_sat_n - 2 * hc_sat_m)$ forbidden ordered vertex pairs
+    contribute $#(hc_sat_n * (hc_sat_n * hc_sat_n - 2 * hc_sat_m))$ successor clauses.
+    The actual target totals are #hc_sat_clauses.len() clauses and
+    #hc_sat_clauses.fold(0, (count, c) => count + c.len()) literal occurrences.
+    Its true literal numbers are
+    #hc_sat_sol.target_config.enumerate().filter(((i, bit)) => bit).map(((i, bit)) => str(i + 1)).join(", ");
+    reading the unique vertex at each position returns the stored circuit.
+    Since $0$ and $3$ are not adjacent, a representative clause is
+    $#(-hc_sat_lit(0, 0)) or #(-hc_sat_lit(3, 1))$ in signed literal notation.
+    Reversing the circuit also satisfies the formula and extraction preserves
+    that orientation; no rotation or reversal is applied by the decoder.
+
+    #{
+      let order = hc_sat_sol.source_config
+      let path = range(hc_sat_n - 1).map(p => (order.at(p), order.at(p + 1)))
+      let degree(v) = path.filter(e => e.contains(v)).len()
+      assert(path.all(e => hc_sat_adj(e.at(0), e.at(1))))
+      assert(not path.any(e => e.contains(0) and e.contains(2)))
+      assert(degree(order.first()) == 1 and degree(order.last()) == 1)
+      let m = path.len()
+      [*NO example.* Retain only the consecutive edges of the stored ordering,
+      omitting its closing edge and the chord. This gives the path
+      #path.map(e => $(#e.at(0), #e.at(1))$).join(", ") on #hc_sat_n vertices,
+      with #m edges. Its target has $#(hc_sat_n * hc_sat_n)$ variables,
+      $#(2 * hc_sat_n + hc_sat_n * hc_sat_n * (hc_sat_n - 1) + hc_sat_n * (hc_sat_n * hc_sat_n - 2 * m))$
+      clauses and $#(4 * calc.pow(hc_sat_n, 3) - 4 * hc_sat_n * m)$ literals.
+      Vertex #order.first() has only one neighbor, whereas a permutation cycle
+      on at least three vertices requires distinct predecessor and successor
+      neighbors. Thus the source is NO, every permutation matrix violates a
+      successor clause, and the uniqueness constraints exclude all remaining
+      Boolean assignments.]
+    }
+  ],
+)[
+  Hamiltonian Circuit in an undirected simple graph @garey1979 reduces to CNF
+  satisfiability by the direct absolute position encoding @velevGao2009.
+  A vertex-position matrix enforces a permutation; forbidden cyclic successor
+  pairs enforce graph adjacency. The target size is $O(n^3)$.
+][
+  _Construction._ Let $G=(V,E)$, $V={0,dots,n-1}$, $n=|V|$, and $m=|E|$.
+  For $n<3$, emit $(z) and (not z)$ over one variable, matching the source's
+  rejection of all such graphs. Otherwise introduce $x_(v,p)$ for vertex $v$
+  and cyclic position $p$, numbered by $ell(v,p)=v n+p+1$ as a signed,
+  one-based literal. For every position, require at least one vertex and
+  exclude every pair of vertices. For every vertex, require at least one
+  position and exclude every pair of positions. For each $p$ and ordered
+  pair $(u,v)$ with $u=v$ or ${u,v} in.not E$, add
+  $not x_(u,p) or not x_(v,(p+1) mod n)$, including the closing position.
+  These are the direct permutation and exclusivity adjacency constraints
+  of @velevGao2009, with explicit exactly-one constraints on both axes.
+
+  _Correctness._ ($arrow.r.double$) An accepted source ordering has $n>=3$.
+  Set precisely its occupied matrix entries true. Each vertex and position
+  occurs once, so both exactly-one families hold. Every cyclic step is a
+  distinct edge, so no emitted successor clause has both entries true.
+  ($arrow.l.double$) A satisfying assignment cannot satisfy the small-graph
+  contradiction. The positive and pairwise clauses give exactly one vertex
+  per position and exactly one position per vertex, hence a permutation.
+  Any equal or non-edge successor pair would falsify its emitted clause.
+  Therefore all cyclic steps, including last-to-first, are edges, and the
+  permutation is an accepted Hamiltonian circuit.
+
+  _Solution extraction._ Validate the target assignment once, then read the
+  unique true vertex in each position and return that ordering. This preserves
+  the starting vertex and orientation. The scan costs $O(n^2)$ after validation.
+
+  _Overhead._ For $n>=3$ there are $n^2$ variables,
+  $2n+n^2(n-1)+n(n^2-2m)$ clauses and $4n^3-4n m$ literal occurrences:
+  $2n$ positive clauses, $n^2(n-1)$ pairwise clauses, and $n$ copies of the
+  $n^2-2m$ forbidden ordered pairs. Redundant equal-successor clauses are
+  retained with multiplicity. The global upper bounds add one variable and
+  two clauses/literals to cover the $(1,2,2)$ small-instance target; omitting
+  the negative edge terms gives the registered bounds. A table of graph
+  adjacencies makes construction $O(n^3)$.
+
+  _Special cases._ An isolated vertex has no permitted successor. A cyclic
+  permutation spanning disconnected components would require a forbidden
+  crossing. These instances are NO. Mathematically, loops cannot supply equal
+  successors and parallel copies do not change adjacency; the Rust simple
+  graph representation rejects both loops and repeated edges.
+]
+
 #let hc_hp = load-example("HamiltonianCircuit", "HamiltonianPath")
 #let hc_hp_sol = hc_hp.solutions.at(0)
 #let hc_hp_n = graph-num-vertices(hc_hp.source.instance)

docs/paper/references.bib

@@ -1,3 +1,13 @@
+@inproceedings{velevGao2009,
+  author    = {Miroslav N. Velev and Ping Gao},
+  title     = {Efficient {SAT} Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles},
+  booktitle = {Proceedings of the Eighth Symposium on Abstraction, Reformulation and Approximation},
+  pages     = {159--166},
+  publisher = {AAAI Press},
+  year      = {2009},
+  url       = {https://miroslav-velev.com/Velev_and_Gao_SARA09.pdf}
+}
+
 @misc{ozkayaCatalyurek2022,
   author       = {M. Yusuf {\"O}zkaya and {\"U}mit V. {{\c C}}ataly{\"u}rek},
   title        = {A Simple and Elegant Mathematical Formulation for the Acyclic {DAG} Partitioning Problem},

src/rules/hamiltoniancircuit_satisfiability.rs

@@ -0,0 +1,164 @@
+//! Absolute position encoding of Hamiltonian circuits as CNF satisfiability.
+
+use crate::models::formula::{CNFClause, Satisfiability};
+use crate::models::graph::HamiltonianCircuit;
+use crate::rules::ReductionError;
+use crate::rules::traits::{ReduceTo, ReductionResult};
+use crate::topology::{Graph, SimpleGraph};
+
+/// A vertex-major position matrix and its source vertex count.
+#[derive(Debug, Clone)]
+pub struct ReductionHamiltonianCircuitToSatisfiability {
+    target: Satisfiability,
+    num_vertices: usize,
+}
+
+impl ReductionResult for ReductionHamiltonianCircuitToSatisfiability {
+    type Source = HamiltonianCircuit<SimpleGraph>;
+    type Target = Satisfiability;
+
+    fn target_problem(&self) -> &Satisfiability {
+        &self.target
+    }
+
+    fn extract_solution(&self, solution: &Vec<bool>) -> crate::rules::ExtractionResult<Vec<usize>> {
+        crate::rules::traits::validate_target_witness(
+            self.target_problem(),
+            solution,
+            |value| value.0,
+            "target assignment does not satisfy the circuit encoding",
+        )?;
+        let n = self.num_vertices;
+        Ok((0..n)
+            .flat_map(|p| (0..n).filter(move |&v| solution[v * n + p]))
+            .collect())
+    }
+}
+
+#[crate::aggregate_reduction(identity)]
+impl crate::rules::AggregateReductionResult for ReductionHamiltonianCircuitToSatisfiability {}
+
+fn checked_num_vars(n: usize) -> Result<usize, ReductionError> {
+    let overflow = || {
+        ReductionError::integer_overflow::<HamiltonianCircuit<SimpleGraph>, Satisfiability>(
+            "sizing the position encoding",
+        )
+    };
+    let square = n.checked_mul(n).ok_or_else(overflow)?;
+    // Four times n³ bounds every clause and literal count in the main branch.
+    square
+        .checked_mul(n)
+        .and_then(|cube| cube.checked_mul(4))
+        .ok_or_else(overflow)?;
+    <HamiltonianCircuit<SimpleGraph> as ReduceTo<Satisfiability>>::exact_i64(
+        square,
+        "numbering SAT variables",
+    )?;
+    Ok(square)
+}
+
+fn literal_index(n: usize, v: usize, p: usize) -> Result<i64, ReductionError> {
+    let index = v
+        .checked_mul(n)
+        .and_then(|offset| offset.checked_add(p))
+        .and_then(|offset| offset.checked_add(1))
+        .ok_or_else(|| {
+            ReductionError::integer_overflow::<HamiltonianCircuit<SimpleGraph>, Satisfiability>(
+                "indexing a position literal",
+            )
+        })?;
+    <HamiltonianCircuit<SimpleGraph> as ReduceTo<Satisfiability>>::exact_i64(
+        index,
+        "representing a position literal",
+    )
+}
+
+#[crate::reduction(transform = upper_bound {
+    num_vars = "num_vertices * num_vertices + 1",
+    num_clauses = "2 * num_vertices + num_vertices * num_vertices * (num_vertices - 1) + num_vertices^3 + 2",
+    num_literals = "4 * num_vertices^3 + 2",
+})]
+impl ReduceTo<Satisfiability> for HamiltonianCircuit<SimpleGraph> {
+    type Result = ReductionHamiltonianCircuitToSatisfiability;
+
+    fn reduce_to(&self) -> Result<Self::Result, ReductionError> {
+        let n = self.num_vertices();
+        let (num_vars, clauses) = if n < 3 {
+            (1, vec![CNFClause::new(vec![1]), CNFClause::new(vec![-1])])
+        } else {
+            let num_vars = checked_num_vars(n)?;
+            let mut adjacent = vec![false; num_vars];
+            for (u, v) in self.graph().edges() {
+                adjacent[u * n + v] = true;
+                adjacent[v * n + u] = true;
+            }
+            let lit = |v, p| literal_index(n, v, p);
+            let mut clauses = Vec::new();
+            for p in 0..n {
+                clauses.push(CNFClause::new(
+                    (0..n).map(|v| lit(v, p)).collect::<Result<_, _>>()?,
+                ));
+                for u in 0..n {
+                    for v in u + 1..n {
+                        clauses.push(CNFClause::new(vec![-lit(u, p)?, -lit(v, p)?]));
+                    }
+                }
+            }
+            for v in 0..n {
+                clauses.push(CNFClause::new(
+                    (0..n).map(|p| lit(v, p)).collect::<Result<_, _>>()?,
+                ));
+                for p in 0..n {
+                    for q in p + 1..n {
+                        clauses.push(CNFClause::new(vec![-lit(v, p)?, -lit(v, q)?]));
+                    }
+                }
+            }
+            for p in 0..n {
+                let q = (p + 1) % n;
+                for u in 0..n {
+                    for v in 0..n {
+                        if u == v || !adjacent[u * n + v] {
+                            clauses.push(CNFClause::new(vec![-lit(u, p)?, -lit(v, q)?]));
+                        }
+                    }
+                }
+            }
+            (num_vars, clauses)
+        };
+        let target = Satisfiability::try_new(num_vars, clauses)
+            .map_err(<Self as ReduceTo<Satisfiability>>::target_construction)?;
+        Ok(ReductionHamiltonianCircuitToSatisfiability {
+            target,
+            num_vertices: n,
+        })
+    }
+}
+
+#[cfg(feature = "example-db")]
+pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
+    use crate::export::SolutionPair;
+    vec![crate::example_db::specs::RuleExampleSpec {
+        id: "hamiltoniancircuit_to_satisfiability",
+        build: || {
+            let source = HamiltonianCircuit::new(SimpleGraph::new(
+                5,
+                vec![(0, 1), (1, 2), (2, 3), (3, 4), (0, 4), (0, 2)],
+            ));
+            let n = source.num_vertices();
+            let order: Vec<_> = (0..n).collect();
+            let assignment: Vec<_> = (0..n).flat_map(|v| (0..n).map(move |p| v == p)).collect();
+            crate::example_db::specs::rule_example_with_witness::<_, Satisfiability>(
+                source,
+                SolutionPair {
+                    source_config: serde_json::json!(order),
+                    target_config: serde_json::json!(assignment),
+                },
+            )
+        },
+    }]
+}
+
+#[cfg(test)]
+#[path = "../unit_tests/rules/hamiltoniancircuit_satisfiability.rs"]
+mod tests;

src/rules/mod.rs

@@ -55,6 +55,7 @@ pub(crate) mod hamiltoniancircuit_ilp;
 pub(crate) mod hamiltoniancircuit_longestcircuit;
 pub(crate) mod hamiltoniancircuit_quadraticassignment;
 pub(crate) mod hamiltoniancircuit_ruralpostman;
+pub(crate) mod hamiltoniancircuit_satisfiability;
 pub(crate) mod hamiltoniancircuit_stackercrane;
 pub(crate) mod hamiltoniancircuit_strongconnectivityaugmentation;
 pub(crate) mod hamiltoniancircuit_travelingsalesman;
@@ -392,6 +393,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
     specs.extend(hamiltoniancircuit_longestcircuit::canonical_rule_example_specs());
     specs.extend(hamiltoniancircuit_quadraticassignment::canonical_rule_example_specs());
     specs.extend(hamiltoniancircuit_ruralpostman::canonical_rule_example_specs());
+    specs.extend(hamiltoniancircuit_satisfiability::canonical_rule_example_specs());
     specs.extend(hamiltoniancircuit_stackercrane::canonical_rule_example_specs());
     specs.extend(hamiltoniancircuit_strongconnectivityaugmentation::canonical_rule_example_specs());
     specs.extend(hamiltoniancircuit_travelingsalesman::canonical_rule_example_specs());