알고리즘서지만 확인
A machine program for theorem-provingMartin Davis, George Logemann, Donald Loveland · 1962Communications of the ACM 5(7), 394–397쪽 (1962)증명 절차를 실제 프로그램으로 짜서 돌려 본 경험을 적은 네 쪽짜리 글로, 변수에 값을 넣어 가며 되돌아가는 DPLL 탐색의 출전으로 널리 인용된다. 오늘날 SAT 풀이기의 뼈대인 「값 배정 · 단위 전파 · 되돌아가기」가 davis-putnam-1960 과 이 글에서 비롯했다고 알려져 있다. NP-완전 문제가 실제로는 자주 풀린다는 이야기의 뿌리를 인용하려는 글에 맞다.
확인:Crossref 의 DOI 등록 기록으로 제목·저자·권호·쪽을 확인했다(등록된 초록은 한 문장뿐이며 본문은 열지 못함).