From fb0b6fc7ea91151fac372c5689d76dd1753d0b4d Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Mon, 2 Nov 2026 20:56:23 -0800 Subject: [PATCH] Add HamiltonianCircuit to Satisfiability reduction --- docs/paper/reductions.typ | 131 +++++++++ docs/paper/references.bib | 10 + .../hamiltoniancircuit_satisfiability.rs | 164 +++++++++++ src/rules/mod.rs | 2 + .../hamiltoniancircuit_satisfiability.rs | 262 ++++++++++++++++++ 5 files changed, 569 insertions(+) create mode 100644 src/rules/hamiltoniancircuit_satisfiability.rs create mode 100644 src/unit_tests/rules/hamiltoniancircuit_satisfiability.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 8e0462b7a..db2376d00 100644 --- a/docs/paper/reductions.typ +++ b/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) diff --git a/docs/paper/references.bib b/docs/paper/references.bib index 0dda81fd2..55d8caf38 100644 --- a/docs/paper/references.bib +++ b/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}, diff --git a/src/rules/hamiltoniancircuit_satisfiability.rs b/src/rules/hamiltoniancircuit_satisfiability.rs new file mode 100644 index 000000000..794daaf03 --- /dev/null +++ b/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; + type Target = Satisfiability; + + fn target_problem(&self) -> &Satisfiability { + &self.target + } + + fn extract_solution(&self, solution: &Vec) -> crate::rules::ExtractionResult> { + 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 { + let overflow = || { + ReductionError::integer_overflow::, 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)?; + as ReduceTo>::exact_i64( + square, + "numbering SAT variables", + )?; + Ok(square) +} + +fn literal_index(n: usize, v: usize, p: usize) -> Result { + 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::, Satisfiability>( + "indexing a position literal", + ) + })?; + as ReduceTo>::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 for HamiltonianCircuit { + type Result = ReductionHamiltonianCircuitToSatisfiability; + + fn reduce_to(&self) -> Result { + 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::>()?, + )); + 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::>()?, + )); + 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(>::target_construction)?; + Ok(ReductionHamiltonianCircuitToSatisfiability { + target, + num_vertices: n, + }) + } +} + +#[cfg(feature = "example-db")] +pub(crate) fn canonical_rule_example_specs() -> Vec { + 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; diff --git a/src/rules/mod.rs b/src/rules/mod.rs index 7606f4923..6128c78dc 100644 --- a/src/rules/mod.rs +++ b/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 ReductionHamiltonianCircuitToSatisfiability { + ReduceTo::::reduce_to(&HamiltonianCircuit::new(graph)).unwrap() +} + +fn encode(order: &[usize]) -> Vec { + (0..order.len()) + .flat_map(|v| order.iter().map(move |&occupant| occupant == v)) + .collect() +} + +fn chorded_cycle() -> SimpleGraph { + SimpleGraph::new(5, vec![(0, 1), (1, 2), (2, 3), (3, 4), (0, 4), (0, 2)]) +} + +fn solve_target(target: &Satisfiability) -> Option> { + use crate::solvers::{SolveOutcome, SolverRequest, solve}; + let loaded = crate::registry::LoadedDynProblem::new(Box::new(target.clone())); + match solve(&loaded, SolverRequest::Ilp).unwrap().outcome { + SolveOutcome::Optimal { solution, .. } => Some(serde_json::from_value(solution).unwrap()), + SolveOutcome::Infeasible => None, + } +} + +#[test] +fn test_hamiltoniancircuit_to_satisfiability_closed_loop() { + let source = HamiltonianCircuit::new(SimpleGraph::cycle(3)); + let result = ReduceTo::::reduce_to(&source).unwrap(); + assert_satisfaction_round_trip_from_satisfaction_target( + &source, + &result, + "circuit position encoding", + ); +} + +#[test] +fn test_aggregate_decision_recovery() { + use crate::rules::{ReductionGraph, ReductionMode}; + let graph = ReductionGraph::new(); + let source_variant = + ReductionGraph::variant_to_map(&HamiltonianCircuit::::variant()); + let target_variant = ReductionGraph::variant_to_map(&Satisfiability::variant()); + let path = graph + .find_all_paths_mode( + HamiltonianCircuit::::NAME, + &source_variant, + Satisfiability::NAME, + &target_variant, + ReductionMode::Aggregate, + ) + .into_iter() + .find(|path| path.len() == 1) + .expect("direct aggregate reduction"); + for input in [SimpleGraph::cycle(3), SimpleGraph::empty(3)] { + let source = HamiltonianCircuit::new(input); + let chain = graph + .reduce_aggregate_along_path(&path, &source) + .unwrap() + .unwrap(); + let target = chain + .target_problem_any() + .downcast_ref::() + .unwrap(); + let target_yes = BruteForce::new().solve(target).unwrap().is_some(); + let source_yes = BruteForce::new().solve(&source).unwrap().is_some(); + assert_eq!( + chain.extract_value(serde_json::json!(target_yes)).unwrap(), + serde_json::json!(source_yes) + ); + } +} + +#[test] +fn test_examples_and_both_orientations() { + let source = HamiltonianCircuit::new(chorded_cycle()); + let result = ReduceTo::::reduce_to(&source).unwrap(); + let target = result.target_problem(); + assert_eq!( + ( + target.num_vars(), + target.num_clauses(), + target.num_literals() + ), + (25, 175, 380) + ); + assert_parameter_predictions(&source, &result); + let solved = solve_target(target).unwrap(); + assert!( + source + .evaluate(&result.extract_solution(&solved).unwrap()) + .unwrap() + .0 + ); + for order in [vec![0, 1, 2, 3, 4], vec![0, 4, 3, 2, 1]] { + let witness = encode(&order); + assert!(source.evaluate(&order).unwrap().0); + assert!(target.evaluate(&witness).unwrap().0); + assert_eq!(result.extract_solution(&witness).unwrap(), order); + } + assert!(target.clauses().contains(&CNFClause::new(vec![-1, -17]))); + assert!(target.clauses().contains(&CNFClause::new(vec![-5, -16]))); + assert!(result.extract_solution(&encode(&[0, 1, 3, 2, 4])).is_err()); + let no = reduce(SimpleGraph::path(5)); + assert_eq!( + ( + no.target.num_vars(), + no.target.num_clauses(), + no.target.num_literals() + ), + (25, 195, 420) + ); + assert!(no.target.clauses().contains(&CNFClause::new(vec![-25, -1]))); + assert!(no.extract_solution(&encode(&[0, 1, 2, 3, 4])).is_err()); + assert!(solve_target(no.target_problem()).is_none()); +} + +fn exhaustive_graphs(n: usize, masks: std::ops::Range) { + let pairs: Vec<_> = (0..n) + .flat_map(|u| (u + 1..n).map(move |v| (u, v))) + .collect(); + for mask in masks { + let edges = pairs + .iter() + .enumerate() + .filter(|(i, _)| mask & (1 << i) != 0) + .map(|(_, &e)| e) + .collect(); + let source = HamiltonianCircuit::new(SimpleGraph::new(n, edges)); + let result = ReduceTo::::reduce_to(&source).unwrap(); + let expected: HashSet<_> = BruteForce::new() + .find_all_witnesses(&source) + .unwrap() + .into_iter() + .collect(); + let assignments = BruteForce::new() + .find_all_witnesses(result.target_problem()) + .unwrap(); + let actual: HashSet<_> = assignments + .iter() + .map(|a| { + let order = result.extract_solution(a).unwrap(); + assert_eq!(encode(&order), *a); + order + }) + .collect(); + assert_eq!(actual, expected, "n={n}, edge mask={mask}"); + assert_parameter_predictions(&source, &result); + if n < 3 { + assert_eq!(result.target.num_vars(), 1); + assert_eq!( + result.target.clauses(), + &[CNFClause::new(vec![1]), CNFClause::new(vec![-1])] + ); + assert!(result.extract_solution(&vec![false]).is_err()); + assert!(result.extract_solution(&vec![true]).is_err()); + } + } +} + +#[test] +fn test_all_graphs_through_three_vertices() { + for n in 0..=3 { + exhaustive_graphs(n, 0..1 << (n * (n.saturating_sub(1)) / 2)); + } +} + +#[test] +fn test_four_vertex_edge_masks_0_to_15() { + exhaustive_graphs(4, 0..16); +} +#[test] +fn test_four_vertex_edge_masks_16_to_31() { + exhaustive_graphs(4, 16..32); +} +#[test] +fn test_four_vertex_edge_masks_32_to_47() { + exhaustive_graphs(4, 32..48); +} +#[test] +fn test_four_vertex_edge_masks_48_to_63() { + exhaustive_graphs(4, 48..64); +} + +#[test] +fn test_extraction_rejects_malformed_and_unsatisfying_assignments() { + let result = reduce(chorded_cycle()); + let valid = encode(&[0, 1, 2, 3, 4]); + let mut empty_column = valid.clone(); + empty_column[0] = false; + let mut two_occupants = valid.clone(); + two_occupants[5] = true; + for invalid in [ + vec![false; 25], + vec![true; 25], + valid[..24].to_vec(), + [valid.as_slice(), &[false]].concat(), + empty_column, + two_occupants, + encode(&[0, 0, 2, 3, 4]), + ] { + assert!(result.extract_solution(&invalid).is_err()); + } +} + +#[test] +fn test_isolated_and_disconnected_graphs() { + for graph in [ + SimpleGraph::new(4, vec![(0, 1), (1, 2), (0, 2)]), + SimpleGraph::new(6, vec![(0, 1), (1, 2), (0, 2), (3, 4), (4, 5), (3, 5)]), + ] { + let source = HamiltonianCircuit::new(graph); + let result = ReduceTo::::reduce_to(&source).unwrap(); + assert!(BruteForce::new().solve(&source).unwrap().is_none()); + assert!(solve_target(result.target_problem()).is_none()); + } +} + +#[test] +fn test_simple_graph_rejects_loops_and_parallel_edges() { + for edges in [vec![(0, 0)], vec![(0, 1), (1, 0)]] { + assert!(SimpleGraph::try_new(3, edges.clone()).is_err()); + assert!( + serde_json::from_value::( + serde_json::json!({"num_vertices":3,"edges":edges}) + ) + .is_err() + ); + } +} + +#[test] +fn test_size_and_literal_arithmetic_boundaries() { + let mut low = 0usize; + let mut high = 1usize << (usize::BITS / 3); + let limit = u128::try_from(usize::MAX).unwrap() / 4; + while low < high { + let mid = low + (high - low).div_ceil(2); + if u128::try_from(mid).unwrap().pow(3) <= limit { + low = mid; + } else { + high = mid - 1; + } + } + assert_eq!(checked_num_vars(low).unwrap(), low * low); + assert!(checked_num_vars(low + 1).is_err()); + assert!(checked_num_vars(1usize << (usize::BITS / 2 - 1)).is_err()); + assert!(checked_num_vars(usize::MAX).is_err()); + if let Ok(max) = usize::try_from(i64::MAX) { + assert_eq!(literal_index(max - 1, 1, 0).unwrap(), i64::MAX); + assert!(literal_index(max, 1, 0).is_err()); + } + assert!(literal_index(usize::MAX, 2, 0).is_err()); + assert!(literal_index(usize::MAX, 1, 1).is_err()); + assert!(literal_index(usize::MAX, 1, 0).is_err()); + assert_eq!(literal_index(5, 4, 4).unwrap(), 25); +}