Selective Enumeration: A Formal Definition
Author: Craig A. Damon
Technical Report: CMU-CS-98-104
Download the PostScript.
Abstract
Selective enumeration is a method for reducing the number of cases required when
performing a generate-and-test search to solve relational formulae. This paper gives
a formal definition of selective enumeration and using that definition,
proves soundness for each of the selective enumeration techniques developed.
Keywords:
Relational calculus, exhaustive search, model checking, specification checking,
constraint satisfaction.
Back to Nitpick Home Page