Using the Davis-Putnam Procedure in Mathematics without

Abstract

Perhaps the most successful computer programs for solving mathematical problems are based on the Davis-Putnam procedure (DPLL). This is remarkable since this procedure was first introduced about 50 years ago. It is first necessary, however, to "reduce" the problem to logic and then employ the Davis Putnam method. Recently, Adam Kolany and I have given a combinatorial procedure which obviates the necessity to reduce first to logic before employing Davis-Putnam style rules. In this talk we take some common mathematical "satisfiablity" problems and show how they can be solved directly. Problems are drawn from graph coloring, Ramsey theory, sudoku, etc.