Modeling and Solving Graph Synthesis Problems Using SAT-Encoded Reachability Constraints in Picat
This work addresses constraint satisfaction problems for researchers and practitioners in logic programming and constraint solving, but it is incremental as it applies existing methods to new data.
The paper tackled graph synthesis problems with reachability constraints by developing Picat programs for four competition problems, demonstrating the language's modeling capabilities and the efficiency of SAT solvers with effective encodings.
Many constraint satisfaction problems involve synthesizing subgraphs that satisfy certain reachability constraints. This paper presents programs in Picat for four problems selected from the recent LP/CP programming competitions. The programs demonstrate the modeling capabilities of the Picat language and the solving efficiency of the cutting-edge SAT solvers empowered with effective encodings.