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

Neng-Fa Zhou
(CUNY Brooklyn College & Graduate Center)

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.

In Andrea Formisano, Yanhong Annie Liu, Bart Bogaerts, Alex Brik, Veronica Dahl, Carmine Dodaro, Paul Fodor, Gian Luca Pozzato, Joost Vennekens and Neng-Fa Zhou: Proceedings 37th International Conference on Logic Programming (Technical Communications) (ICLP 2021), Porto (virtual event), 20-27th September 2021, Electronic Proceedings in Theoretical Computer Science 345, pp. 165–178.
Published: 17th September 2021.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: