%0 Book Section %1 DPLL %A Davis, D. Loveland M. %B Communications of the ACM %D 1962 %K 1962 SAT-solver dpll theorem-proving %T A machine program for theorem proving %V 5

@incollection{DPLL, added-at = {2007-05-25T13:58:36.000+0200}, author = {Davis, D. Loveland M.}, biburl = {https://www.bibsonomy.org/bibtex/2866607ebef08a1c369cd4794bfc98a7f/zeno}, booktitle = {Communications of the ACM}, description = {SAT}, interhash = {9a12387d5decbac24efd2ca8c02d012d}, intrahash = {866607ebef08a1c369cd4794bfc98a7f}, keywords = {1962 SAT-solver dpll theorem-proving}, timestamp = {2007-07-25T15:20:39.000+0200}, title = {A machine program for theorem proving}, volume = 5, year = 1962 }