Picat Version 3.9#8 Released

[Neng-Fa Zhou]

Picat 3.9#8 is available from https://picat-lang.org and  https://github.com/picat-lang/Picat.

This release brings major improvements to the SAT compiler and delivers significant performance gains on Pseudo-Boolean (PB) optimization problems.

In our experiments, the new version solves nearly twice as many PB instances as the version submitted to last year’s PB competition. These improvements are the result of several new techniques and optimizations introduced in the SAT compiler.

Improved PB Constraint Decomposition: A new algorithm for decomposing PB constraints has been introduced that exploits the presence of at-most-one constraints. This optimization significantly reduces encoding size and improves propagation efficiency on many benchmark instances.

Advanced Hybrid Encodings: New hybridization strategies have been developed for combining BDD, binary-adder, and Espresso encodings of PB constraints. The compiler can now better adapt encodings to the features of individual constraints, resulting in smaller SAT instances and faster solving times.

Bit-Vector Objectives in solve/2: The objective to be minimized or maximized in the solve/2 predicate of the sat module can now be specified as a bit-vector. This enhancement makes it possible to model optimization problems that involve big objective values.

Improved Branch-and-Bound Implementation: The implementation of the branch-and-bound algorithm in the SAT compiler has been improved. The new implementation generally reduces the number of calls of the SAT solver required to find optimal solutions.

We thank the Picat community for their continued support and feedback.

[Neng-Fa Zhou]

P.S. The Linux executable was built with an older version of gcc/g++ to avoid dependencies on newer system libraries. For the best performance, I recommend building Picat from the source code.

Cheers,

NF

--
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/4ce798d4-0d2d-4128-b7ae-3f48102e3973n%40googlegroups.com.

[C. G.]

Hi Neng-Fa,

A related bug report:

With 3.9#7 and with the new 3.9#8 as well (both on Linux) there are differences between the solution sets for cp vs sat.

I have extracted from a program generated by ASPIC a reproducible small test:

import cp. %returns [[0,0],[1,-2]]
%import sat. %returns only [[1,-2]]
main=>
A::0..1,
B#=cond(A, -2 ,0), % "useless" constraint that leads to the cp vs sat difference
L=solve_all([A,B]),println(L).

SAT fails to find one of the solutions in this case. In other cases, as it constraints more than it should, it fails to find solutions at all to models that cp solves successfully ; in yet other cases, by missing some of the search space it fails to find with sat the optimum value when the problem is one of optimization (I have seen all that).

The behavior is triggered by the constraint involving cond. It might well be that I don't understand something there, as the cp vs sat difference disappears when the -2 in cond is replaced with a positive number, such as 2. 

best regards,

CG

[Neng-Fa Zhou]

Thanks, Cristian, for spotting that. I have fixed the bug and released a patch 3.9#8.1.

Best regards,

NF

To view this discussion visit https://groups.google.com/d/msgid/picat-lang/2c35ec1d-bf93-46b2-a606-065d55688707n%40googlegroups.com.

[Oisín Mac Fhearaí]

Very cool! I tested it on a couple of Advent of Code SAT solutions and got speedups from 60s -> 34.6s and 5.1s -> 4.2s. Impressive.

To view this discussion visit https://groups.google.com/d/msgid/picat-lang/CAFOC6HQv_aRf1Du6R3y%2B_v2Yr2PhMSTixZNdKhSLGOk4Wo7Omw%40mail.gmail.com.

[C. G.]

I hoped for a similar improvement on the N-queens benchmark for large N where in the ASPIC paper we compare clingo and aspic/picat on the same source. 

With picat 3.9#4, 512 queens is solved in 26 s. 

With 3.9#8.1 the time on the same machine is 62.5 s. 

With Picat 3.9#7: 64.5 s.

Somewhere between 3.9#4 and 3.9#7  picat got twice slower on that problem.

CG

[Neng-Fa Zhou]

While the new version with the new optimizations overall is faster, it may be slower on some instances. This is always the case as the SAT solver uses opportunistic strategies. I notice that 3.9#8 is much slower than 3.9#6 on the bqueens benchmark (https://picat-lang.org/sat/bqueens.pi). For n=500, 3.9#6 took 5.5s while 3.9#8 took 16.3s on my computer, despite that the encoding sizes are similar (nvars=370042,ncls=2420822 for 3.9#6 and nvars=370050,ncls=2420650 for 3.9#8).

Cheers,

NF