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

[C. G.]

Hi Neng-Fa,

 

Even with the Picat version 3.9#8.2 there are differences between cp and sat.

I've tried to isolate and simplify the bug-reproducing program,  it is given below. CP solves it the way I expect it, finds a set of edges that define a tree on 4 nodes, and reports the set of edges and how many are selected.

SAT just fails.

Here is the program.

%import cp.
import sat.
main:-
N=4,
X=new_array(N,N),X::0..1,
V=[{I,1}:I in 1..N],E=[{I,J,X[I,J]}:I in 1..N,J in 1..N],tree(V,E),
S#=sum([1:I in 1..N, J in 1..N,X[I,J]#=1]),
solve([X,S]),
println(s=S),
println(x=X).

best regards,

CG

[Neng-Fa Zhou]

Hi Cristian,

I am surprised to see that this program works with cp. You should not use constraints in an iterator because an iterator condition is checked eagerly. If you change

S#=sum([1:I in 1..N, J in 1..N,X[I,J]#=1]),

to 

S#=sum([X[I,J]:I in 1..N, J in 1..N]),

your program should work as expected.

Cheers,

NF

To view this discussion visit https://groups.google.com/d/msgid/picat-lang/3186befb-05b6-4c0e-bcde-40a4dbeabbf4n%40googlegroups.com.

[C. G.]

Hi Neng-Fa,

My usage is more complex, this was a minimal reproducing example. These situations appear in ASPIC when it translates ASP aggregators, say
#sum{Y:gen(Y),test(Y)}>5.
When in the ASP program there are these as well
gen(1..2).
test(2..3).
the predicate involving the aggregator expression gets translated to Picat as the following constraint expression:

aspic_gt(aspic_sum([ASPIC_OPTCOND3:Y in 1..2,Y in 2..3,ASPIC_OPTCOND1=aspic_conj([gen(Y),test(Y)]),ASPIC_OPTCOND2#=ASPIC_OPTCOND1,ASPIC_AGVAL1= Y, ASPIC_AGVAL2#=ASPIC_AGVAL1,ASPIC_OPTCOND3 #= cond(ASPIC_OPTCOND2,ASPIC_AGVAL2,0)]) ,5)

where gen/1,test/1,aspic_conj/2,aspic_gt/2,aspic_sum/1 are functions returning either 0,1 or constraint variables.
This is the workaround I found to basically use functions into constraints: Var=function_call(Args), Var2#=Var,... then Var2 can be used in further constraints.

"cond" is used to apply the condition in a constraint way. I could replace cond with multiplication Condition*Value, but I doubt multiplication leads to more efficient modelling, and I still need functions in constraints, so I have to use the workaround explained above.

best regards,
CG

[Neng-Fa Zhou]

Thanks, Cristian, for sharing. I would do the same thing to move out function calls of constraints.

BTW, an update version (3.9#9) has been released, which includes several improvements and the fix of a bug discovered during the preliminary runs of the PB competition. 

Cheers,

NF

[C. G.]

Hi Neng-Fa,

It would be wonderful if you could do this transformation automatically, such that it doesn't need to be done manually.

best regards,

Cristian

[Neng-Fa Zhou]

It's not easy for Picat to do the transformation automatically because the parser doesn't know which functors are function calls and which functors are term constructors. The parser turns a constraint into the term construction mode if the main functor is a constraint operator such as #= and #>. In global constraints, the user has to denote functors as term constructors. That's why $ is needed the n-queens program:

queens(N) =>
    Q=new_list(N),
    Q :: 1..N,
    all_different(Q),
    all_different([$Q[I]-I : I in 1..N]),
    all_different([$Q[I]+I : I in 1..N]),
    solve(Q),
    writeln(Q).

Cheers,

NF

To view this discussion visit https://groups.google.com/d/msgid/picat-lang/34375e61-c081-46e2-8b37-91a408e4b397n%40googlegroups.com.

[C. G.]

I think it would make maybe more sense for the parser to assume the functor are functions, especially for the functors/arity that are already defined as functions. And when the user means actually just a functor, they can force that interpretation using $, like in the other contexts. The issue right now is that one can force the interpretation of "functor constructor" but cannot force the interpretation of "function call", and the functor constructor is simultaneously the default interpretation in the operands of the constraint operators, as you explained, leaving one with no choice other than deconstruct the whole expression and build it manually step by step with many intermediary variables, lowering the readability of the code as well.