HCUP

Solving the Hamiltonian Cycle Problem via SAT and User Propagators

This repository contains the implementation accompanying our paper. It encodes the Hamiltonian Cycle Problem (HCP) as a SAT formula and solves it using CaDiCaL extended with the IPASIR-UP interface for user propagators. The user propagator monitors partial assignments, detects subcycles early, and injects blocking clauses directly into the solver — either inside the solver (via cb_check_found_model) or outside through an iterative solve loop.

---

Overview

The Hamiltonian Cycle Problem asks whether a given undirected graph contains a cycle that visits every vertex exactly once. The tool encodes the degree constraints of each vertex as a SAT formula and refines partial models during search by asserting external clauses whenever a subcycle is detected. Multiple strategies for generating these clauses are implemented and can be selected at runtime. Other strategies include reasoning to propagate assignments and make decisions.

Architecture

src/
├── main.cpp                    Entry point, signal handling
├── hcup.{hpp,cpp}              Top-level orchestration
├── util/
│   ├── config.{hpp,cpp}        CLI parsing, configuration
│   ├── encodings.{hpp,cpp}     SAT encoding of HCP (Sinz, Commander, CRT)
│   └── lib.{hpp,cpp}           Graph utilities, miscellaneous functions
├── Factory/                    Solver instantiation from config
├── HCPSolver/                  Solver interface (IHCPSolver)
├── Propagators/                IPASIR-UP propagators with varying interaction frequencies
├── Policy/
│   ├── BlockingClausePolicy.hpp      Blocking clause strategies
│   ├── UserDecisionPolicy.hpp        Decision heuristics
│   └── UserPropagationPolicy.hpp     Unit propagation via graph knowledge
├── UnionFind/                  UnionFind datastructures for graph representation
└── ExternalClauseStore/        External clause queue that adds them during search

Input Formats

Format	Extension	Description
HCP	.hcp	Header with a whitespace-separated edge list (u v per line)
DIMACS	.col	Standard DIMACS graph colouring format

A copy of the Flinders Hamiltonian Cycle Project Challenge Set can be found in the directory problems/.

Partial Encodings

Flag value	Description
commander	Commander encoding for at-most-one constraints (default)
sinz	Sinz encoding for at-most-one constraints
chinese-remainder	Chinese Remainder Theorem-based ordering encoding (requires -m)

Blocking Clause Strategies (-b)

Strategy	Description
all-cutset	Assert cutset clauses for every detected subcycle (default)
single-cutset	Assert only the smallest cutset clause
all-subcycle	Assert a clause breaking each subcycle directly (both directions)
single-subcycle	Assert a clause breaking the smallest subcycle (both directions)
merge-cutset	Attempt to merge subcycles via 2-opt before asserting cutset
pair-cutset	Group subcycles into two classes; assert the inter-class cutset
pair-cutset-balanced	Like pair-cutset but balances class sizes
pair-cutset-oa	Over-approximation variant of pair-cutset

---

Build

Requirements

• CMake ≥ 3.18
• C++20-capable compiler (GCC or Clang)
• The CaDiCaL submodule (included under include/cadical)

Release Build

git clone --recursive https://github.com/FabianTUW/HCP-IPASIR-UP.git
cd HCP-IPASIR-UP
cmake -B cmake-build-release -DCMAKE_BUILD_TYPE=Release
cmake --build cmake-build-release --target all -j $(nproc)

The binary is placed at cmake-build-release/hcup.

Debug Build (includes tests)

cmake -B cmake-build-debug -DCMAKE_BUILD_TYPE=Debug
cmake --build cmake-build-debug --target all -j $(nproc)

GoogleTest is fetched automatically by CMake in debug mode. No manual installation is required.

---

Usage

hcup -i <FILE> [OPTIONS] [--cadical <CADICAL OPTIONS>]

Options

Flag	Long form	Argument	Default	Description
-i	--input	FILE	—	Input graph file (.hcp or .col)
-e	--encoding	commander|sinz|chinese-remainder	commander	At-most-one encoding (+ forbid partial cycles for CRE)
-m	--crt-modulus	UINT	—	Modulus for CRT encoding (e.g. 2, 6, 12, 60)
-b	--strategy-blocking-clause	see above	all-cutset	Blocking clause strategy
-s	--stage-blocking-clause	inside|outside	outside	Where blocking clauses are emitted
-c	--early-cycle-detection	none|cutset|subcycle|cutset-subcycle	none	Detect cycles during propagation
-d	--user-decision	none|heat|smallest-degree	none	Custom decision heuristic
-p	--user-propagation	none|prevent-subcycle	none	Custom unit propagation
-f	--interaction-frequency	UINT	1	Interact with the graph every N steps
-l	--low-frequency-mode	step-size|trail-length|merge-cutset	—	Low-frequency interaction mode
-o	--output-format	vertices|edges|hcp	vertices	Solution output format
--cadical		CADICAL OPTS	—	Pass options directly to CaDiCaL

Examples

Solve a graph with default settings:

./cmake-build-release/hcup -i problems/hcp/graph1.hcp

Use the merge-cutset strategy:

./cmake-build-release/hcup -i problems/hcp/graph1.hcp -b merge-cutset

Enable early cycle detection, user propagation and refine models during the search:

./cmake-build-release/hcup -i problems/hcp/graph1.hcp \
    -c cutset -p prevent-subcycle -s inside

Use the low-frequency propagator (interact every 25% (at 25%, 50% and 75%) of assigned trail):

./cmake-build-release/hcup -i problems/hcp/graph1.hcp \
    -c cutset -l trail-length -f 25

Pass CaDiCaL options directly:

./cmake-build-release/hcup -i problems/hcp/graph1.hcp \
    --cadical --lucky=false --restartint=100

To check if the found solution represents a Hamiltonian cycle run e.g.:

./cmake-build-release/hcup -i problems/hcp/graph1.hcp -o edges | python3 verify_solution.py problems/txt/graph1.txt 

Exit Codes

Code	Meaning
0	Satisfiable — a Hamiltonian cycle was found and printed
1	Unsatisfiable — no Hamiltonian cycle exists
2	Interrupted — solver was terminated before completion
255	Could not process command line arguments.

---

Running Tests

Tests require a debug build (see above).

# Fast tests only
ctest -L fast --test-dir cmake-build-debug -j $(nproc) --output-on-failure

# Full test suite (includes slow regression tests)
ctest --test-dir cmake-build-debug -j $(nproc) --output-on-failure

With just (if installed):

just test        # fast tests
just test-full   # all tests

---

Auxiliary Scripts

Script	Description
verify_solution.py	Verify a printed solution against a .txt graph
runlim_bench.py	Benchmark runner with resource limits via runlim

The directory ./data-analysis contains additional code to analyze runs.

---

Dependencies

Dependency	Version	Notes
CaDiCaL	submodule	SAT solver with IPASIR-UP support
GoogleTest	v1.14.0	Fetched automatically in debug builds

Reproducibility Notes

To help reproducibility we report the version of the CaDiCaL and HCUP version together with the supplied configuration at the start of every run. Attention should also be placed on the compiler version as well as the compiler flags used to produce the executable.

Citation

If you want to cite our paper please use:

TODO