алгоритм Дэвиса-Патнема-Логемана-Лавленда(полный алгоритм поиска с возвратом для определения выполнимости булевых формул, записанных в конъюнктивной нормальной форме. Опубликован в 1962 г. Мартином Дэвисом, Хилари Патнем, Джорджем Логеманом и Дональдом Лавлендом и представлял собой усовершенствование более раннего алгоритма Дэвиса-Патнема, метода, основанного на правиле резолюци alex_)
алгоритм Дэвиса-Патнема-Логемана-Лавленда(полный алгоритм поиска с возвратом для определения выполнимости булевых формул, записанных в конъюнктивной нормальной форме. Опубликован в 1962 г. Мартином Дэвисом, Хилари Патнемом, Джорджем Логеманом и Дональдом Лавлендом, представляет собой усовершенствование более раннего алгоритма Дэвиса-Патнема (1960 г.), основанного на правиле резолюций Alex_Odeychuk)
