Incremental SAT-based method with native Boolean cardinality handling for the Hamiltonian cycle problem

DOI10.1007/978-3-319-11558-0_52MaRDI QIDQ2938540zbMATH OpenOpenAlexFDO

Authors Takehide Soh, Daniel Le Berre, Stéphanie Roussel, Mutsunori Banbara, Naoyuki Tamura

Publication date 14 January 2015

Published in Logics in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-11558-0_52

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Graph theory (including graph drawing) in computer science (68R10) Paths and cycles (05C38) Computational aspects of satisfiability (68R07)

Recommendations

• A SAT based effective algorithm for the directed Hamiltonian cycle problem
• An effective algorithm for and phase transitions of the directed Hamiltonian cycle problem
• A logical model of HCP
• Deterministic ``snakes and ladders heuristic for the Hamiltonian cycle problem
• HybridHAM: a novel hybrid heuristic for finding Hamiltonian cycle

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 5139168 (Why is no real title available?)
• scientific article; zbMATH DE number 2243353 (Why is no real title available?)
• A Decision Procedure for Bit-Vectors and Arrays
• A hybrid simulation-optimization algorithm for the Hamiltonian cycle problem
• Advances on the Hamiltonian problem -- a survey
• An effective algorithm for and phase transitions of the directed Hamiltonian cycle problem
• Boolean satisfiability with transitivity constraints
• Complexity-sensitive decision procedures for abstract argumentation
• Computer Aided Verification
• Counterexample guided abstraction refinement algorithm for propositional circumscription
• RESILIENT LKH: SECURE MULTICAST KEY DISTRIBUTION SCHEMES
• Recent advances on the Hamiltonian problem: survey III
• Reducibility among combinatorial problems
• SAT problems with chains of dependent variables
• Solving QBF with counterexample guided refinement
• Some New Branching and Bounding Criteria for the Asymmetric Travelling Salesman Problem
• TSPLIB—A Traveling Salesman Problem Library
• The traveling salesman problem: An overview of exact and approximate algorithms
• Theory and Applications of Satisfiability Testing
• Towards Robust CNF Encodings of Cardinality Constraints
• Towards an Optimal CNF Encoding of Boolean Cardinality Constraints

Cited in

(8)

• Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
• A linear-size conversion of HCP to 3HCP
• Chinese remainder encoding for Hamiltonian cycles
• An incremental SAT-based approach for solving the real-time taxi-sharing service problem
• Concise integer linear programming formulation for clique partitioning problems
• MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers
• A SAT based effective algorithm for the directed Hamiltonian cycle problem
• Hamiltonian cycle reconfiguration with answer set programming

Describes a project that uses

Uses Software

• Lynx
• Scarab
• Sat4j
• TSPLIB

This page was built for publication: Incremental SAT-based method with native Boolean cardinality handling for the Hamiltonian cycle problem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2938540)