Suggestion: making it easier to swap the integrated kissat - led to 2x-9x acceleration on one problem

[C. G.]

Hi,

I tried to execute this code, and it was quite slow (about 32.6 seconds until the integrated satsolver decided there is no solution):

import sat.
admissible(A,N,K)=>A=new_array(N,N),A::0..1,
    foreach(I1 in 1..N, I2 in 1..N, I2>I1, I3 in 1..N, I3>I2, J1 in 1..N, J2 in 1..N, J2>J1, J3 in 1..N, J3>J2)sum([A[Ii, Jj] : Ii in [I1,I2,I3], Jj in [J1,J2,J3]])#>0,
    foreach(I in 1..N-1)lex_le([A[I,J]:J in 1..N],[A[I+1,J]:J in 1..N]).

main0=>N=7,S=34,admissible(A,N,3),sum([A[I,J]:I in 1..N,J in 1..N])#=N*N-S,solve(A),println(A).
main=>time2(main0).

I replaced the sat solver in picat with the newest version of kissat, which also won medals this year (again?) for its top performance. The improvement for the code above was really dramatic: the runtime reduced to 3.6 seconds, it went 9x faster!

When one replaces S=34 with S=33 the problem becomes satisfiable. In this case the execution time decreased from 5.25 s to 2.53 seconds, about 2x faster.

As a suggestion, this is what I did to replace kissat with the newest version:

in kissat:

./configure -shared
make libkissat.a

in picat/emu:

rm -rf kissat #I did compile it separately
mkdir -p kissat/src
cp kissat.h kissat/src
cp libkissat.a kissat

add libkissat.a in common.mak on this line
picat$(EXT) : $(OBJ) $(ESPRESSO_OBJ)
$(CPP) -o picat$(EXT) $(CFLAGS) $(OBJ) $(ESPRESSO_OBJ)  $(KISSAT_OBJ) kissat/libkissat.a  $(LFLAGS)
and remove all the kissat related compilation.

This type of integration makes it also easier to integrate newer versions of kissat in the future, as the changes in its set of source files require no further changes in the common.mak file.

Also appreciated would be a way to define/call other SAT solvers, e.g. by interacting with those using the DIMACS file format.

best regards,

Cristian

[Hakan Kjellerstrand]

Hi Cristian.

Regarding the model. there are at least one, perhaps two missing "end" in the admissible/3 predicate.

With the "-log" logging parameter, Picat prints two

   "--- SYNTAX WARNING --- (59-67) missing 'end' inserted for foreach."

I added two "end" and then it took < 1s (from 1 minute on my machine for your original model),:

- S=34: 0.6s

- S= 33: 0.2s

Here's the adjusted model ("<--" markes the two "end" that are added)..

"""

import sat.

admissible(A,N,K) =>

  A=new_array(N,N),A::0..1,
  foreach(I1 in 1..N,
          I2 in 1..N, I2>I1,
          I3 in 1..N, I3>I2,
          J1 in 1..N, J2 in 1..N, J2>J1,
          J3 in 1..N, J3>J2)
    sum([A[Ii, Jj] : Ii in [I1,I2,I3], Jj in [J1,J2,J3]]) #> 0

  end, % <---
  foreach(I in 1..N-1)

    lex_le([A[I,J]:J in 1..N],[A[I+1,J]:J in 1..N])

  end. % <---

main0 =>
  N=7,
  S=34,
  admissible(A,N,3),

  sum([A[I,J]:I in 1..N,J in 1..N])#=N*N-S,
  solve(A),
  println(A).
main=>time2(main0).

"""

The output for S=33.

"""

{{0,0,0,0,0,1,1},{0,0,1,0,1,1,0},{0,0,1,1,0,0,0},{0,1,0,0,0,0,0},{1,0,0,0,1,0,0},{1,0,0,1,0,1,0},{1,0,1,0,0,0,1}}

"""

Without the "end" after the first foreach loop in adminissible/3  then then second loop is repeated many times.

Hope this help.

That being said, I like your suggestion on making it easier to swap the SAT solver, but it's on Neng-Fa's table.

Best,

Hakan

[Neng-Fa Zhou]

Hi,

I did a comparison of the latest version of kissat and the old version  that is currently included in Picat, I noticed no improvement of the latest version overall on the 2024 MiniZinc benchmarks. Individually, you can find instances that run faster with one version than the other.

Cheers,

NF

[C. G.]

Hi Hakan,

Many thanks for your answer, and especially for the hint about the wrong syntax. I confirm getting similarly small running times as you report, 0.124 and 0.664 s with the newer kissat on my machine.

best regards,

Cristian