Version 3.9#5 Released

[Neng-Fa Zhou]

I am pleased to announce the release of version 3.9#5. This version introduces a dynamic programming–based encoder for single-constant multiplication constraints into SAT, achieving near-optimal encodings with practical efficiency. The encoder, whose source code is available at https://github.com/nfzhou/Picat/blob/master/scm.pi, demonstrates the use of the new table mode mmin. In addition, this release adopts a refined BDD-based encoding for pseudo-Boolean constraints. With these enhancements, Picat is able to solve many instances that earlier versions could not.

Cheers,

NF

[Oisín Mac Fhearaí]

Great to see new ideas still coming out in Picat!

I tested this version out on a few old AoC programs and some were faster, but I also found some performance regressions compared to 3.9#3:

* https://github.com/DestyNova/advent_of_code_2023/blob/main/24/part2.pi (40s instead of ~16s)

* https://github.com/DestyNova/advent_of_code_2023/blob/main/5/part2.pi (not sure about this one; my notes say ~35 seconds but 3.9b2 errors out, 3.9b3 is much slower and b5 is approx 4x slower than b3... I didn't keep the old Picat version so not sure if I changed/broke the program or what)

* https://github.com/DestyNova/advent_of_code_2022/blob/main/21/part2.pi (swap cp for sat, b5 is slower than b3 and outputs "cost=xxx" messages -- is this a debug build?)

--
You received this message because you are subscribed to the Google Groups "Picat" group.
To unsubscribe from this group and stop receiving emails from it, send an email to picat-lang+...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/picat-lang/7dfee19a-d868-40b4-9a0c-c1bf5079eaa2n%40googlegroups.com.

[Neng-Fa Zhou]

Thank you for your quick feedback. 

Your program for the year-23 day-24 problem doesn't work on my input (https://github.com/nfzhou/aoc/blob/main/in23_24.txt) due to integer overflow. I need to convert the integer constraints to bit-vector constraints to make it work.

I don't see any performance difference between version 3.9#5 and 3.9#4 on your year-23 day-5 program.

Your program for year-22 day-21 problem outputs debug information. The statement for debugging has been removed (the version number is unchanged).

For single-constant multiplication constraints, you may experience slight slowdowns for easy problems as the dynamic programming encoder takes longer to encode the constraints. For hard problems, the time spent on encoding  pays off as DP generally generates much higher quality encodings.

Cheers,

NF