Routing - the Euclidean bottleneck traveling salesman problem - FAQ
Purpose of exercise
- Practice writing equation-based programs
- Use engineering analysis to deal with numerical approximations
- Practice specifying correctness properties
- Use DrACuLa DoubleCheck for predicate-based, random testing
- Coach the ACL2 mechanical logic to verify software properties
- Define the following functions
- Package the functions you define as a book.
- DoubleCheck the properties stated below
- Use ACL2 to prove the properties
- Package the theorems as a book.
- Define a function insert-everywhere that, given a value x and a list xs,
delivers a list xss whose elements are all like xs, but with x inserted
among the elements. The list xss must contain one more element than xs, and
for each index k, there must be a list in xss whose element of index k is x.
(That is, the list xss must contain versions of xs with x in all possible
positions.) The order of the lists in xss is is immaterial. For example, the
value of (insert-everywhere 1 '(2 3)) could be ((1 2 3) (2 1 3) (2 3 1)), or
it could be ((2 3 1) (2 1 3) (1 2 3)), or it could be other arrangements of
the lists (1 2 3), (2 1 3), and (2 3 1).
- Define a function that delivers the list of permutations of a given list.
The order in which the list arranges the permutations is immaterial. For
example, either the list ((1 2 3) (1 3 2) (2 1 3) (2 3 1) (3 1 2) (3 2 1))
or the list ((1 2 3) (2 1 3) (2 3 1) (1 3 2) (3 1 2) (3 2 1)) or any of many
other arrangements would be suitable values for (permutations '(1 2 3)).
- Define a function that finds an optimal route in the Euclidean bottleneck traveling
salesman problem (as described in Wikipedia).
Note 1: Include your max-min and permutations books in the code, and refer to
functions where you find them useful.
Note 2: Since the bottleneck version of the problem seeks only
minimize the longest segment in a route (not the length of the whole route), you can use squared Euclidean
distance as a proxy for Euclidean distance. This is fortunate, since
Euclidean distance is usually not a rational number.
- State and prove a theorem about the relationship of the length of
(insert-everywhere x xs) compared to the length of xs.
- State and prove a theorem that says that x is an element of every list in
(insert-everywhere x xs) [Hint: Define a predicate (member-all x xss) whose value is non-nil if and only
if the formula (member-equal x xs) is non-nil for every element xs of xss.]
- State and prove a theorem that says that every list in (insert-everywhere
x xs) is a permutation of the list (cons x xs). [Hint: See the the definition
of perm, defined in
Section 10.3 of the Computer-Aided Reasoning textbook]
- Define a theorem that says that (permutations xs) is a true-list of
true-lists, as long as xs is a true-list.