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.