<!DOCTYPE html>
<html><head>
<meta charset="UTF-8">
</head><body><p class="default-style"><br>I am pleased to announce the release of Picat version 2.5.</p><p class="default-style">The new version includes the SAT-based constraint solver that won one gold medal and one bronze medal in the XCSP competition, and one silver medal and one bronze medal in the MiniZinc Challenge in 2018. The competition results show that Picat represents the state of the art in encoding general constraint satisfaction problems into SAT. The PicatSAT compiler is written in Picat with over 10,000 LOC. In addition to the advancement of SAT solvers and the optimization techniques used in the compiler, the spectacular performance of Picat in the competitions is also attributed to the Picat language itself. Picat's features, such as attributed variables, unification, pattern-matching rules, backtracking, and loops, are all put into good use in the implementation. There are hundreds of optimization rules, and they are easily described as pattern-matching rules in Picat.</p><p class="default-style">The new version also features a new constraint module, named smt, which uses z3 or cvc4 as the underlying SMT solver. SMT is another primary paradigm for solving combinatorial problems. This new module makes it possible to use Picat as a modeling language for SMT solvers. The smt module follows the same interface as the three other constraint modules (cp, sat, and mip). With this new module, Picat will offer a convenient platform for experimenting with different types of solvers.</p><p class="default-style"><br></p><p class="default-style">Sincerely,<br>Neng-Fa Zhou<br>on behalf of the Picat team<br></p></body></html>