Solving Non-Boolean Satisfiability Problems with the Davis-Putnam Method

The Davis-Putnam method has received recent attention for its ability to solve large problems. Many of these problems are non-Boolean, in that they are most naturally expressed as formulas containing variables with domains of more than two values. There are two approaches to solving non-Boolean formulas — either translate the problem into a Boolean equivalent and solve this with a Boolean procedure, or use a non-Boolean procedure directly on the non-Boolean formula. This project develops a direct non-Boolean Davis-Putnam procedure and compares the results of using the two approaches.