Direct finite first-order model generation with negative constraint propagation heuristic
Olga Shumsky, Ralph W. Wilkerson, William W. McCune, Fikret Erçal · 1997
An automated finite first-order model generator has been developed. The problem is viewed as a firstorder satisfiability problem. Most existing model generators reduce the problem to propositional satisfiability by converting the input first-order clauses into propositional clauses. This generator, unlike others, stores the input first-order clauses and solves the problem directly. It uses an exhaustive backtracking algorithm with weight-based splitting. A negative constraint propagation is implemented to reduce the number of decision points and thus to speed up the search. PROBLEM STATEMENT AND SOLUTION METHODS We are presented with a set of first-order sentences and a finite domain of elements. To simplify the problem, we always convert the sentences to first-order clauses, which are disjunctions of literals. A literal, in this case, is a statement about functions. The task is to determine whether the given set of clauses is satisfiable, i.e. whether there exists an assignment of f...