Hi,
I'm currently taking a course on algorithms, and a major part of said course is to write proofs about why a given algorithm is correct/has a certain complexity/has some other property. Unfortunately, I'm not very good with proofs. Most times, I can explain why a given property holds, but when the time comes to turn it into a proof, I simply hit a dead end.
I'm currently working on an assignment, where the objective is to device a brute force search algorithm for solving the knapsack problem, prove it correct, give a complexity estimate and prove that estimate. The algorithm I've come up with looks like this:
Function knap
Returns:
A pair of an integer and a list; the list is the most valuable list of
items that fits in the knapsack, and the integer is the total
value of said list.
Inputs:
Let xs be a list of roads that may be taken (items that may be chosen)
Let p be the path we took to get here (items we've previously chosen)
Let c be the maximum capacity of the knapsack
Let bestPath be the best "path" (set of items), and set it initially
to the empty list.
Let val be the value of bestPath, and set it initially to 0
If size(p) > c, then return (val, bestPath)
If value(p) > val
Let bestPath = p
Let val = value(p)
End If
For Each x in xs
(val, bestPath) = knap(xs - x, p + x, c, bestPath, value)
End For
Return (val, bestPath)
Looks like this implemented in haskell:
-- xs is the list of itms to choose from, p is the candidate solution,
-- c is the knapsack capacity, bv is the value of the current best solution,
-- and bl is the current best solution
knap xs p c bv bl
| sackSize p > c = (bv, bl)
| otherwise = foldl forEachItem (bv', bl') xs where
(bv', bl') -- if value(p) > val .. end if
= case sackValue p of
v | v > bv -> (v, p)
_ -> (bv, bl)
forEachItem (bv, bl) x
= knap (delete x xs) (x:p) c bv bl
sackSize = foldl (\acc (x, _) -> acc + x) 0
sackValue = foldl (\acc (_, x) -> acc + x) 0
The problem is, as you may have guessed, that I'm having trouble proving the correctness of it. More specifically, I'm trying to prove that it actually examines all valid candidate solutions. Explaining why it doesn't miss any possible solution in plain English is easy:
For every way to pick an item x from a set, we add x to our candidate solution and recursively examine all ways to pick another item when x is already taken and thus no longer available until we either run out of items to choose from, or the weight of the candidate solution exceeds the knapsack capacity. With every item added to the candidate solution, we check if the candidate is better than the current best solution, and update that best solution accordingly.
...but I can't seem to turn that into a proof. I'm not asking for you to write out a complete proof for me, but perhaps someone could give me a nudge in the right direction?
I've tried creating a proof by induction for it, but I'm having a hard time defining the base cases and induction steps, especially since it's an accumulating recursive function.
