The Davis-Putnam procedure with splitting
In a New York University report of 8 June 1961 Martin Davis, George Logemann and Donald Loveland described a program for the IBM 704 that tests formulas by the Davis-Putnam method of 1960, with one of its rules replaced by a splitting rule. A formula on which Gilmore's program had run for 21 minutes without a result, it proved in under two minutes.
Why it matters
Instead of expanding the formula further, the program split the problem into two smaller ones and dropped branches already inconsistent. Formulas beyond the previous program became a matter of minutes, and problems of hundreds of quantifier-free lines came within reach.
The program keeps Davis and Putnam's one-literal clause rule and their rule for literals of one sign only, and replaces the third rule by splitting: a formula is inconsistent if and only if both of its branches are. The statement that uniform continuity implies continuity, over 500 quantifier-free lines, was found valid in just over two minutes. The machine's memory was 32,768 words. Davis and Putnam's paper in the Journal of the ACM names the three rules itself: elimination of one-literal clauses, the affirmative-negative rule, and the rule for eliminating atomic formulas, by which (A ∨ p) & (B ∨ ¬p) & R is inconsistent if and only if (A ∨ B) & R is. The authors showed the method's advantage thus: a formula on which Gilmore's program for the IBM 704 had run 21 minutes without a result was worked by hand with their method in 30 minutes. The 1962 journal version in Communications of the ACM explains why the third rule gave way to splitting: Rule III quickly increases the number and length of clauses, which is prohibitive on a machine with limited fast storage. The program, for the IBM 704 of New York University's Institute of Mathematical Sciences, was coded entirely in the SAP assembler.