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.
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):
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]