eyeprolog

Knapsack optimization

Which gear gives an expedition the most value within its weight limit?

Eight items, each with a weight and a value, and a pack that holds 15 units. The 0/1 knapsack problem asks which subset of items to take, each item taken whole or not at all, so that the total value is as large as possible. EyeProlog enumerates every subset, filters by weight, and keeps the best one.

Run it in the playground · Source


The question

What is the most valuable pack that weighs at most 15? What are its weight and value, and how many packs fit at all?


The data

capacity(15).
items([atlas, battery, camera, drone, emergency_radio, field_laptop, medkit, sensor]).

item(atlas, 2, 6).
item(battery, 4, 10).
item(camera, 3, 8).
item(drone, 6, 13).

item(Name, Weight, Value) facts form the item table, kept apart from the rules so the problem can be retuned without touching the logic.


Every subset, once

subset([], []).
subset([Item|Rest], [Item|Chosen]) :- subset(Rest, Chosen).
subset([_item|Rest], Chosen) :- subset(Rest, Chosen).

For each item there are two clauses: take it, or leave it. Backtracking through both choices for all eight items produces all 2⁸ = 256 subsets.

best_pack(Pack, Weight, Value) :-
  aggregate_max(Value, pack(Pack, Weight), feasible_pack(Pack, Weight, Value), Value, pack(Pack, Weight)).

feasible_pack/3 keeps the subsets within capacity, and aggregate_max/5 picks the one with the highest value.


The answer

eyeprolog examples/knapsack-optimization.pl
knapsack_answer(best_pack, [atlas, battery, camera, medkit, sensor]).
knapsack_answer(total_weight, 15).
knapsack_answer(total_value, 40).
knapsack_answer(feasible_pack_count, 113).

113 of the 256 subsets fit, and the best uses the full capacity for a value of

  1. It skips the single most valuable item, the field laptop (16), because five lighter items give more value per unit of weight.

The reason

eyeprolog --proof examples/knapsack-optimization.pl
step(best_pack([atlas, battery, camera, medkit, sensor], 15, 40),
     rule(19),
     ['Pack' = [atlas, battery, camera, medkit, sensor], 'Weight' = 15, 'Value' = 40],
     [aggregate_max(40, pack([atlas, battery, camera, medkit, sensor], 15), feasible_pack([atlas, battery, camera, medkit, sensor], 15, 40), 40, pack([atlas, battery, camera, medkit, sensor], 15))]).

The best pack holds by rule 19, whose single premise is the aggregate_max/5 call with the winning pack, weight and value filled in.


The check

condition('C1', resolution, ok, 5).
obligation(builtin, theory_scoped, countall(feasible_pack(A, B, C), 113)).
verdict(checked_with_obligations).

The five rule steps replay against the program. The maximum and the count each summarize a search over all 256 subsets. The checker records them as theory-scoped obligations, trusted premises that rest on the aggregate library, rather than redoing the search.


Try it

Learn more in The Art of EyeProlog, Chapter 24.