An UPgrade for HCP: Solving the Hamiltonian Cycle Problem via User Propagators

Abstract

Das Hamiltonkreisproblem fragt, ob es in einem Graphen einen geschlossenen Pfad gibt, der jeden Knoten genau einmal besucht. Als eines der 21 NP-vollständigen Probleme von Karp hat es besonderes Forschungsinteresse auf sich gezogen. Moderne Lösungsansätze reduzieren HCP auf das Erfüllbarkeitsproblem (SAT) und verwenden gegenbeispielgeleitete Abstraktionsverfeinerung (CEGAR), um inkrementell Subzyklen von Lösungskandidaten zu entfernen.Diese Arbeit präsentiert Hcup, den ersten HCP-Solver, der sich das IPASIR-User-Propagator-Interface von CaDiCaL zunutze macht. Obwohl das Anschließen eines User-Propagators die meisten Formelvereinfachungstechniken von SAT-Solvern deaktiviert, erlaubt es auch das Beeinflussen der internen Suche des SAT-Solvers an verschiedenen Punkten. Das ermöglicht es, spezialisierte auf HCP angepasste Suchalgorithmen zu entwerfen. Beispielsweise kann eine externe Propagation das Schließen eines Zyklus verhindern oder eine externe Klausel generiert und zum SAT-Solver hinzugefügt werden, um Zyklen, die sich in einer partiellen Belegung bilden, zu widerlegen. Das Ziel dieser Arbeit ist es, die potenziellen Vorteile von HCP-spezifischen externen Propagatoren zu untersuchen. Um diese Untersuchung zu unterstützen, wurde Hcup in einem erweiterbaren, modularen Rahmen konzipiert, der das Kombinieren solcher Suchalgorithmen mit geringen Einschränkungen erlaubt und das Hinzufügen neuer Algorithmen ermöglicht, ohne dass die anderen beeinflusst werden.Wir evaluieren Hcup in 24 Konfigurationen von User-Propagatoren auf allen 1001 Instanzen des Flinders Hamiltonian Cycle Problem Challenge Sets. Zudem implementieren wir den State-of-the-Art-HCP-Lösungsansatz von Ohashi et al., der eine Standard CEGAR-Methode darstellt. Durch das Deaktivieren von Formelvereinfachungstechniken in dieser CEGAR-Methode erhalten wir eine Baseline, die uns ermöglicht, zwei verschiedene Lösungsansätze miteinander zu vergleichen und den potenziellen Vorteil von User-Propagatoren zu messen. Unsere Ergebnisse zeigen, dass die meisten Propagatoren mehr Probleminstanzen lösen als die Baseline. Der vielversprechendste Propagator propagiert Literale, die verhindern, dass der SAT-Solver einen Subzyklus schließt, und löst 117 Instanzen mehr als die Baseline. Weiters zeigen das Verfeinern der Lösungskandidaten innerhalb des SAT-Solvers, das die bereits generierten Belegungen beibehält, und das Anwenden einer Entscheidungsheuristik Verbesserungen gegenüber der Baseline. Zuletzt zeigt das Erkennen von Subzyklen während der Suche durchwachsene Ergebnisse, wobei das frühere und häufigere Erkennen weniger Instanzen löste als das Erkennen erst spät in der Suche.Die Ergebnisse sind ermutigend und motivieren weitere Arbeiten, die untersuchen, wie sich die Vorteile von User-Propagatoren, der CEGAR-Methode und Formelvereinfachungstechniken effizient kombinieren lassen.

The Hamiltonian Cycle Problem (HCP) asks whether a graph contains a cycle that visits every vertex exactly once. As one of Karp’s 21 NP-complete problems, it has seen significant research interest. State-of-the-art approaches reduce HCP to BooleanSatisfiability (SAT) and apply counterexample-guided abstraction refinement (CEGAR) to incrementally eliminate subcycles from candidate solutions.This thesis presents Hcup, the first HCP solver to leverage the IPASIR-UP interface for user propagators from CaDiCaL. Although attaching an external propagator disables most of the formula simplification techniques used by a SAT solver, it enables interference with the solver’s internal search at several points. This allows for the design of specialized search algorithms tailored to HCP. For example, an external propagation can prevent the closing of subcycles during search, and an external clause can be generated and added during search to refute subcycles that have formed in a partial assignment. The goal of this thesis is to investigate the potential benefits of such HCP-specific external propagators. To support this investigation, Hcup is designed as a modular and extensible framework in which these search algorithms can be combined with minimal restrictions, and new algorithms can be implemented in isolation.We evaluate Hcup in 24 configurations of user propagators on all 1001 instances of the Flinders Hamiltonian cycle problem challenge set. Additionally, we implement the state-of-the-art HCP-solving approach by Ohashi et al., which follows the standard CEGAR approach. By disabling formula simplification in the CEGAR method, we obtain a baseline, enabling us to effectively compare two different solving approaches and measure the potentially beneficial effect of user propagators on the search.Our results show great potential for user propagators for HCP solving compared to current methods. Most of our proposed user propagators solve more instances than the baseline does. The most promising propagator, which propagates literals to prevent the SAT solver from closing subcycles, solves 117 instances more than the baseline. Further, refining the model candidates inside the SAT solver, thereby keeping the assignment trail and applying a decision heuristic, also shows improvement over the baseline. Finally, detecting subcycles during the search yields mixed results, as earlier and more frequent detections solve fewer instances than when applied only in the later stages of the search.These results are encouraging and motivate future work to investigate how the benefits of user propagators, CEGAR, and formula simplifications could be combined efficiently.