“A Machine Program for Theorem-Proving” was published by Martin Davis, George Logemann, and Donald Loveland in Communications of the ACM, volume 5, number 7, pages 394 to 397, in July 1962. It refined an earlier procedure by Davis and Hilary Putnam, and the resulting algorithm is now known by the initials of all four contributors as DPLL, the Davis-Putnam-Logemann-Loveland procedure.
The paper tackles the satisfiability problem: given a logical formula in conjunctive normal form, a big AND of clauses that are ORs of literals, decide whether any assignment of true and false to the variables makes the whole thing true. DPLL is a backtracking search that picks a variable, tries a value, and works out the consequences, undoing choices that lead to a contradiction. Its two famous shortcuts are unit propagation, which forces the value of any variable that appears alone in a clause, and pure-literal elimination. The earlier Davis-Putnam method had used a rule that could blow up memory; the 1962 paper replaced it with the splitting-and-backtracking search that proved far more practical.
This procedure became the skeleton of essentially every modern SAT solver. Decades later, with additions like conflict-driven clause learning, DPLL-based solvers became astonishingly fast and turned satisfiability from a theoretical curiosity into an industrial tool.
Why business readers should care: SAT solvers descended from DPLL now verify that microprocessors and safety-critical software behave correctly, configure complex products, and schedule resources. A short 1962 paper laid down the search strategy that quietly checks much of the technology people depend on.