Selective Enumeration
Author: Craig A. Damon (thesis)
Technical Report: CMU-CS-00-151
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.