die package:sbv

Solve the problem using a BMC search. We have:

>>> dieHard
BMC Cover: Iteration: 0
BMC Cover: Iteration: 1
BMC Cover: Iteration: 2
BMC Cover: Iteration: 3
BMC Cover: Iteration: 4
BMC Cover: Iteration: 5
BMC Cover: Iteration: 6
BMC Cover: Satisfying state found at iteration 6
Big: 0, Small: 0 (Initial)
Big: 5, Small: 0 (FillBig)
Big: 2, Small: 3 (BigToSmall)
Big: 2, Small: 0 (EmptySmall)
Big: 0, Small: 2 (BigToSmall)
Big: 5, Small: 2 (FillBig)
Big: 4, Small: 3 (BigToSmall)

Solves the die-hard riddle: In the movie Die Hard 3, the heroes must obtain exactly 4 gallons of water using a 5 gallon jug, a 3 gallon jug, and a water faucet. We use a bounded-model-checking style search to find a solution.