Many constraint satisfaction problems involve synthesizing subgraphs
that satisfy certain reachability constraints. In this talk, I'll
present SAT encodings for the HCP and SCC constraints, and their use
in modeling and solving several graph problems selected from recent
LP/CP programming competitions. The solutions demonstrate the modeling
capabilities of the Picat language and the solving efficiency of the
cutting-edge SAT solvers empowered with effective encodings.

Neng-Fa Zhou is a Professor of Computer Science at the City University
of New York. He has been an active researcher in programming language
systems for more than 25 years. He has authored over 50 papers on
programming languages, constraint-solving, graphics, and machine
learning systems published in journals (TPLP, TOPLAS, JLP, JFLP, and
SPE) and major conferences. He is the principal designer and
implementer of the B-Prolog and Picat systems. The SAT-based CSP
solver, PicatSAT, that he implemented, has won numerous prizes in
MiniZinc and XCSP solver competitions.

===

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

Neng-Fa Zhou
CUNY Brooklyn College & Graduate Center