|
Abstract : |
This document describes the implementation and use of a Davis-Putnam procedure for the propositional satisfiability problem. It also describes code that takes statements in firstorder logic with equality and a domain size n searches for models of size n. The first-order model-searching code transforms the statements into set of propositional clauses such that the first-order statements have a model of size n if and only if the propositional clauses are satisfiable. The propositional set is then given to the Davis-Putnam code; any propositional models that are found can be translated to models of the first-order statements. The firstorder model-searching program accepts statements only in a flattened relational clause form without function symbols. Additional code was written to take input statements in the language of Otter 3.0 [5] and produce the flattened relational form. The program was successfully applied to several open questions on the existence of orthogonal quasigroups. 1 The Davis-Putnam Procedure The Davis-Putnam procedure is widely regarded as the best method for deciding the satisfiability of a set of propositional clauses. I'll assume that the reader is familiar with it. I list here some features of our implementation. 1. There are no checks for pure literals. Experience has shown that is usually more expensive than its worth. 2. Deletion of subsumed clauses is optional. Again, experience has shown that it is too expensive. 3. The variable selected for splitting is the always first literal of the first, shortest positive clause., |
