had earlier mentioned that he found the problem "irresistibly seductive" when he was an undergraduate and later had progressively become his "lifelong obsession". Other contributions Davis collaborated with Putnam, George Logemann, and Donald W. Loveland in 1961 to introduce the Davis–Putnam–Logemann–Loveland (DPLL) algorithm which was a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem. The algorithm was a refinement of the earlier Davis–Putnam algorithm, which was a resolution-based procedure developed by Davis and Putnam in 1960. The algorithm is foundational in the architecture of fast Boolean satisfiability solvers. In addition to his work on computability theory, Davis also made significant contributions to the fields of computational complexity and mathematical logic. Davis was also known for his model of Post–Turing machines. In 1974, Davis won the Lester R. Ford Award for his expository writing related to his work on Hilbert's tenth problem, and in 1975 he won the Leroy P. Steele Prize and the Chauvenet Prize (with Reuben Hersh). He became a fellow of the American Academy of Arts and Sciences in 1982, and in 2013, he was selected as one of the inaugural fellows of the American Mathematical Society. Davis's 1958 book Computability and Unsolvability is considered a classic in theoretical computer science, while his 2000 book The Universal Computer traces the evolution and history of computing starting including works of Gottfried Wilhelm Leibniz and Alan Turing. His book The Undecidable, the first edition of which was published in 1965, was a collection of unsolvable problems and computable functions. Personal life and death Davis was married to Virginia Whiteford Palmer, a textile artist. The couple met during their time in the Urbana–Champaign area and subsequently married in 1951. They had two children. The couple lived in Berkeley, California, after his retirement. Davis died on January 1, 2023, at age 94. His wife died the same day several hours later. Selected publications Books 1982 Dover reprint 2014 Dover reprint Reprinted as Articles Davis, Martin (1973), "Hilbert's Tenth Problem is Unsolvable", American Mathematical Monthly, 80(3), 233–269. . Davis, Martin (1995), "Is mathematical insight algorithmic?", Behavioral and Brain Sciences, 13(4), 659–60. Davis, Martin (2020), "Seventy Years of Computer Science", In: Blass A., Cégielski P., Dershowitz N., Droste M., Finkbeiner B. (eds.) Fields of Logic and Computation III, 105–117. Lecture Notes in Computer Science, vol. 12180. Springer: Cham, Switzerland. .