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

arXiv: https://arxiv.org/abs/2109.08293 · HTML: https://mlsanity.com/paper/2109.08293/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 2 of its 29 references that are in the map.
- First posted on arXiv 17 Sep 2021.

## Builds on (most cited first, 2 of 2)

- [Local Consistency and SAT-Solvers](https://mlsanity.com/paper/1401.4613/) (2014)
- [Declaratively solving Google Code Jam problems with Picat](https://mlsanity.com/paper/1504.00977/) (2015)

## Built on by (most cited first, 1 of 1)

- [Proceedings of the 2022 XCSP3 Competition](https://mlsanity.com/paper/2209.00917/) (2022)

## Abstract (arXiv)

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.