Picat doesn't seem to be optimising for the objective

Question

This is my first time using Picat. I have attempted to write a basic knapsack problem. However, when run, the solution seems to pick no items even though I (think I) have asked it to maximise the total value of the items picked.

Here's the output:

$ Picat/picat --version
Picat version 3.5

$ more items-59.txt 
58
45,27,1,2,27,4,22,4,36,19,39,54,26,17,8,23,35,38,35,12,52,21,43,15,46,43,21,22,49,1,12,8,47,23,28,35,4,17,14,1,45,41,13,49,24,6,7,20,4,33,32,16,46,17,14,40,40,52,33
9,19,15,14,7,20,18,19,2,3,15,15,4,14,3,20,1,15,13,10,21,14,18,20,17,23,18,14,6,23,14,3,4,9,20,21,10,19,9,13,8,4,11,23,3,13,2,10,15,20,23,5,10,14,4,20,10,3,18

$ more knapsack.pi
import sat.
import util.

main(Args) =>
    solve_knap(Args).

solve_knap(Args) =>
    Params = open(Args[1]),
    MaxWeight = to_int(read_line(Params)),
    ValsStr = split(read_line(Params),","),
    N = len(ValsStr),
    Vals = [to_int(X) : X in ValsStr],
    WeightsStr = split(read_line(Params),","),
    Weights = [to_int(X) : X in WeightsStr],

    Take = new_array(N),
    Take :: 0..1 ,
    TotalWeight #= sum([ W * T : W in Weights, T in Take]),
    TotalWeight #<= MaxWeight ,

    TotalVal #= sum([ V * T : V in Vals, T in Take]),

    solve([$max(TotalVal),$report(printf("Found %d\n",TotalVal))],Take),

    println(TotalWeight),
    println(MaxWeight),
    println(Take).
 
$ Picat/picat knapsack.pi items-59.txt 
Found 0
0
58
{0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0}

The is the same whether I import cp or import sat. I'm sure I'm making a newbie mistake, any help would be appreciated.

Answer 1

The main issue with this model is the two list comprehensions (see below for the full model):

TotalWeight #= sum([ W * T : W in Weights, T in Take)]),
TotalWeight #= sum([ W * T : {W,T} in zip(Weights,Take)]),

They are actually doing cross products (all W's times all T's) which is not the proper way. Instead they should be using zip to just multiply each ith pair.

TotalWeight #= sum([ W * T : {W,T} in zip(Weights,Take)]),
TotalVal #= sum([ V * T : {V,T} in zip(Vals,Take)]),

Unfortunately, for zip to work the Take must be a list, not an array:

Take = new_list(N),

An alternative of using zip is to use this approach (which works with Take as an array):

TotalWeight #= sum([Weights[I]*Take[I] : I in 1..N]), 
TotalVal #= sum([Vals[I]*Take[I] : I in 1..N]), 

Also, for this problem a MIP solver (GLPK or Cbc) are faster than SAT and CP solvers, and the SMT solvers are (surprisingly) fast. Here's the timing of the solvers I have on my machine (I don't have Gurobi available):

• MIP (GLPK): 0.1s
• MIP (Cbc): 0.5s
• SMT (z3); 1.65s
• SMT (cvc4): 3.4s
• CP (with ffd/updown): 12.2s
• SAT: 16.4s

Here's the full model:

solve_knap(Args) =>
    nolog,
    Params = open(Args[1]),
    MaxWeight = to_int(read_line(Params)),
    ValsStr = split(read_line(Params),","),
    N = len(ValsStr),
    Vals = [to_int(X) : X in ValsStr],
    WeightsStr = split(read_line(Params),","),
    Weights = [to_int(X) : X in WeightsStr],

    Take = new_list(N),
    Take :: 0..1 ,
    TotalWeight #= sum([ W * T : {W,T} in zip(Weights,Take)]),
    TotalWeight #<= MaxWeight , 

    TotalVal #= sum([ V * T : {V,T} in zip(Vals,Take)]),    

    solve($[ff,updown,max(TotalVal),report(printf("Found %d\n",TotalVal))],Take ++ [TotalWeight]),

    println(totalWeight=TotalWeight),
    println(maxWeight=MaxWeight),
    println(totalVal=TotalVal),
    println(take=Take).

Here's the solution (from the MIP/GLPK run):

totalWeight = 57
maxWeight = 58
totalVal = 465
take = [1,0,0,0,0,0,0,0,1,1,0,0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,1,0,0,0,0,0,0,0,1,1,0,0,1,0,0,0,0,0,0,0,1,0,0,0,0,1,0]