Picat - A new avenue for exploration

The field of constraint programming CP and Satisfaction Modular theory SMT appear to have a high barriers to entry. Many of the concepts that lie behind the solvers, rely on mathematical explanations and verified computational theories. However when it gets down to it, understanding a problem thoroughly, and being able to express it in precise logical terms is all that is needed for making progress in this area.

What has been very rewarding is seeing a computer generate a solution, after giving it just the description of the problem, rather than providing a method to solve the problem. This is very different from the current mode of artificial intelligence included in ChatGPT et cetera which provides solutions by looking for answers near places that textually look like the question being asked. 

The general method used up to this point, has been encoding a problem into a textual / numerical description, then transforming that description into the language required by either Z3, or MathSat5. This has been a successful approach, providing answers to all shapes and sizes of Soduku, Gogen, Hidato, and other similar numerical puzzles. Whilst this has proved a satisfactory avenue of exploration, it did feel like spoon feeding the solver with a rather low level and basic language. (SMT-2) being their language of choice.

I felt there must be a better way, and I think I found it. Picat is a problem text processor that encompasses in its logical language how to describe various shapes and sizes of problems and includes different solvers. I am just taking the very first steps in understanding how to use Picat, but I am encouraged by its compact syntax and flexibility. 

Peoples way of learning a new language or skill vary. Some like to tinker explore tryout, poke with a stick and others like to read the technical descriptions and before getting their hands dirty. Personally I like to tinker around with new things but have a goal in mind. Picat was very amenable to trying out things once a couple of fundamentals were understood. I'll document my first efforts in the next post.

A shortlist of resources is provided.

The introduction paper

My First Look At Picat as a Modeling Language for Constraint Solving and

Planning by Håkan Kjellerstrand1

http://picat-lang.org/download/a_first_look_at_picat.pdf

This is a great starting point for existing users of solver type programs.

The Website 

From which the "Getting started" and "User guides" are available along with install downloads for PC, Mac and Linux platforms.

http://picat-lang.org/

The Book  

"Constraint Solving and Planning with Picat"

Whilst there is a .pdf available having the book makes access easier.

The jumbo boxes of Picat examples

There is a set of 99 converted problems here 

and 

A big set of other example including numerical puzzles here.

The Guy

I had a couple of email dialogs with Haken Kjellerstrand, the Sweden based co-author of the book and major contributor to Picat. He was just so helpful, engaged, and willing to put effort into looking at the questions I had that it gave me a warm, fuzzy feeling about Picat community.

The other Guys

Picat is created by Neng-Fa Zhou and Jonathan Fruhman.