A tale of two solvers: Eager and lazy approaches to bit-vectors

The standard method for deciding bit-vector constraints is via eager reduction to propositional logic. This is usually done after first applying powerful rewrite techniques. While often efficient in practice, this method does not scale on problems for which top-level rewrites cannot reduce the problem size sufficiently. A lazy solver can target such problems by doing many satisfiability checks, each of which only reasons about a small subset of the problem. In addition, the lazy approach enables a wide range of optimization techniques that are not available to the eager approach. In this paper we describe the architecture and features of our lazy solver (LBV). We provide a comparative analysis of the eager and lazy approaches, and show how they are complementary in terms of the types of problems they can efficiently solve. For this reason, we propose a portfolio approach that runs a lazy and eager solver in parallel. Our empirical evaluation shows that the lazy solver can solve problems none of the eager solvers can and that the portfolio solver outperforms other solvers both in terms of total number of problems solved and the time taken to solve them.

Autonomous hot metal carrier

This paper reports work involved with the automation of a Hot Metal Carrier — a 20 tonne forklift-type vehicle used to move molten metal in aluminium smelters. To achieve efficient vehicle operation, issues of autonomous navigation and materials handling must be addressed. We present our complete system and experiments demontrating reliable operation. One of the most significant experiments was five-hours of continuous operation where the vehicle travelled over 8 km and conducted 60 load handling operations. We also describe an experiment where the vehicle and autonomous operation were supervised from the other side of the world via a satellite phone network.