Modeling and Solving Graph Synthesis Problems Using SAT-Encoded Reachability Constraints in Picat

Picat [27] is a Prolog-like language that takes many features from other languages, including patternmatching rules, functions, list/array comprehensions, loops, assignments, tabling for dynamic programming and planning, and constraint programming. These features make Picat a convenient modeling language for combinatorial problems, on a par with AMPL [8], OPL [9], and MiniZinc [17]. As a logic language, Picat can often offer solutions that are as concise and elegant as the ones in ASP [5]. Picat supports constraint solving using different solvers, including CP (constraint programming), SAT (satisfiability), MIP (mixed integer programming), and SMT (SAT Modulo Theories). The last two decades have witnessed dramatic enhancement in SAT solvers' performance, thanks to inventions of techniques, from conflict-driven clause learning, backjumping, variable and value selection heuristics, to random restarts [2, 4, 16]. With findings of effective encodings [12, 13, 15, 19, 21, 23, 26], SAT has become a strong contendant for solving a wide range of constraint satisfaction and optimization problems (CSP). Many CSPs involve synthesizing subgraphs that satisfy certain reachability constraints, including the constraint that ensures a cycle connecting all the vertices, as in the Hamiltonian cycle problem (HCP), and the constraint that ensures a strongly connected component. For that reason, CP systems provide graph constraints for easing the modeling and solving of these problems [1, 20].