funny idea: let's make picat parallel as a portfolio solver

[C. G.]

I enjoy Picat a lot, although I regret it is not multithreaded in a time when most machines are multicore. 

Still unrelated, the practice shows that one has to experiment with import sat, import cp and so on until one lands on the best choice for the particular program. I've just landed again a problem where cp is much faster than sat (my default choice).

Therefore the idea: what if one simply (and preferably automatically) tries say solving in parallel with cp and sat in a "first to finish" way? This could be done with two separate Picat instances. 

The idea can be extended to the solver options (have multiple SAT variants and multiple cp variants all running in parallel)

Benefit: automatically getting the fastest results, without having to try them all out explicitly.

Potential issue: RAM usage, as they run in parallel, the RAM usage adds up.

What do you think? I wonder whether this can be done from within picat (something like "import constraints") or needs to be done outside it (some sort of wrapper).

best regards,
CG

[Neng-Fa Zhou]

It's not easy to make Picat multi-threaded because many of Picat's built-ins are not thread safe. One way to take advantage of multi-cores is to use a parallel SAT solver. Picat had an interface with p-lingeling, but that interface has become obsolete because p-lingeling is not competitive with the sequential kissat. I don't see any competitive parallel sat solvers available.

I once wrote an interpreter for FlatZinc that chooses sat or cp based on extracted features of variables and constraints. For a simple language like FlatZinc, it's easy to do solver selection, as the interpreter has access to the accumulated constraints, and can post the constraints after a solver is selected. It's not easy to do solver selection within Picat as cp translates constraints into propagators immediately after they are posted.

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/13575a41-419d-4d55-85eb-691fc6781d16n%40googlegroups.com.

[C. G.]

Well, my proposal is not to do solver selection, nor truly/fully parallelize picat, just something like this, assuming we want to execute "program.pi" that uses constraints and solve:

When picat program.pi is called, it spawns multiple picat processes, fully independent of each other, each running the same "program.pi" : some of the picat copies import sat, others import cp. For the ones that imported cp, some solve forward, some backward, some go for ff, some consider the variables in random order. For the ones importing sat, some use the "seq" option, some the "split" one. It is indeed very difficult in advance to know with combination will be the best, the idea is to run all those picat instances in parallel and let the best one win.

Say the problem is a constraints solving one - the very first copy to finish solving wins - all other instances can be shut down, and are, automatically; the winning one continues with the code after solve.

How could something like this be implemented, such that we test if it really brings something? Should I try a wrapper approach first to just prove the concept - actually the portfolio solving is quite well known, and is used by SAT solvers as well, e.g. cryptominisat was using it some years ago, in a very similar fashion, fairly transparent for the user.

best regards,
CG

On Wednesday, 6 May 2026 at 18:05:37 UTC+2 Neng-Fa Zhou wrote:

It's not easy to make Picat multi-threaded because many of Picat's built-ins are not thread safe. One way to take advantage of multi-cores is to use a parallel SAT solver. Picat had an interface with p-lingeling, but that interface has become obsolete because p-lingeling is not competitive with the sequential kissat. I don't see any competitive parallel sat solvers available.

I once wrote an interpreter for FlatZinc that chooses sat or cp based on extracted features of variables and constraints. For a simple language like FlatZinc, it's easy to do solver selection, as the interpreter has access to the accumulated constraints, and can post the constraints after a solver is selected. It's not easy to do solver selection within Picat as cp translates constraints into propagators immediately after they are posted.

Cheers,

NF

[Neng-Fa Zhou]

You can do parallel solving using OS commands. Suppose you have the following  program file "prog.pi":

main([Solver]) =>
    N = 10,
    Qs = new_array(N),
    Qs :: 1..N,
    foreach (I in 1..N-1, J in I+1..N)
        Qs[I] #!= Qs[J],
abs(Qs[I]-Qs[J]) #!= J-I
    end,
    solve(Qs),
    println(Qs),
    printf("finished %s\n",Solver).

Note that no solver module is imported.  You can run it using the following Picat script:

main =>
    run_prog("cp"),
    run_prog("sat"),
    run_prog("mip").

run_prog(SolverName) =>
    FileName = "prog_" ++ SolverName ++ ".pi",
    FD = open(FileName,write),
    println(FD,"import " ++ SolverName ++ "."),
    nl(FD),
    printf(FD,"main => main([\"%s\"]).\n",SolverName),
    nl(FD),
    Lines = read_file_lines("prog.pi"),
    foreach (Line in Lines)
        (Line == [] -> nl(FD); println(FD,Line))
    end,
    close(FD),
    _ = command("picat " ++ FileName ++ "&").

For each solver, the program makes a copy of "prog.pi" with the solver name imported,  and runs the copy as a background process.

Best regards,

NF