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

TL;DR

This paper demonstrates how Picat can model and solve graph synthesis problems with reachability constraints efficiently using SAT encodings, showcasing its modeling power and solver performance.

Contribution

It introduces Picat programs for graph synthesis problems that leverage SAT encodings, highlighting modeling capabilities and solving efficiency.

Findings

Effective SAT encodings enable efficient solving of reachability constraints.

Picat demonstrates strong modeling capabilities for graph synthesis problems.

The approach is validated on problems from recent LP/CP competitions.

Abstract

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.