2. Логика высказываний - синтаксис, семантика, выполнимость, общезначимость, метод семантических таблиц, алгоритм DPLL (Лекции), страница 2
Описание файла
Файл "2. Логика высказываний - синтаксис, семантика, выполнимость, общезначимость, метод семантических таблиц, алгоритм DPLL" внутри архива находится в папке "Лекции". PDF-файл из архива "Лекции", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 6 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 2 страницы из PDF
. . . . . . . .Решение для миллионов переменных и множителей вформулах, возникающих на практикеКонференции, соревнования, использование в индустрии и наукеИ при этомникто не понимает, почему оно работает1Davis–Putnam–Logemann–LovelandSAT: локальный поискСхема работы алгоритмов локального поиска:1. выбрать начальный набор значений переменных2.
если на полученном наборе КНФ истинна, то завершитьработу3. иначе выбрать переменную, изменить её значение иперейти к (2)4. по необходимости выбрать новый набор значенийпеременных или досрочно завершить работуIIIВыбор осуществляется с привлечением случайностицель “блужданий” по наборам — получить как можнобольше истинных множителейесли КНФ невыполнима или подходящий выполняющийнабор не найден, то ответ не определёнSAT: DPLLСхема работы DPLL-алгоритмов для КНФ C :DPLL(cnf C):if(C == "true") return trueif(C == "false") return falsepick X: X is variable of Cpick b: b = 0 or b = 1if(DPLL(C{X=b})) return truereturn DPLL(C{X=!b})Дополнительные оптимизации:IIсвёртка констант: если в множителе КНФ осталось однослагаемое X (или X), то немедленно подставить значениеX = 1 (или X = 0)деполяризация: если переменная X входит в C только безотрицания (или только с отрицанием), то немедленноподставить значение X = 1 (или X = 0)SAT: DPLLПример(x1 ∨ x2 ∨ x3 ) (x1 ∨ x2 ∨ x3 ) (x1 ∨ x2 ) (x2 ∨ x3 )x2 = 1(x1 ∨ x3 ) x1 x3Пояснения:Выбираем переменную x2 и значение 1SAT: DPLLПример(x1 ∨ x2 ∨ x3 ) (x1 ∨ x2 ∨ x3 ) (x1 ∨ x2 ) (x2 ∨ x3 )x2 = 1(x1 ∨ x3 ) x1 x3x1 = x3 = 0falseПояснения:Свёртка констант для x1 , x3SAT: DPLLПример(x1 ∨ x2 ∨ x3 ) (x1 ∨ x2 ∨ x3 ) (x1 ∨ x2 ) (x2 ∨ x3 )x2 = 1(x1 ∨ x3 ) x1 x3x1 = x3 = 0falseПояснения:Появился ложный множитель: откатSAT: DPLLПример(x1 ∨ x2 ∨ x3 ) (x1 ∨ x2 ∨ x3 ) (x1 ∨ x2 ) (x2 ∨ x3 )x2 = 1(x1 ∨ x3 ) x1 x3x2 = 0x1 ∨ x3x1 = x3 = 0falseПояснения:Переходим к оставшемуся значению 0 для x2SAT: DPLLПример(x1 ∨ x2 ∨ x3 ) (x1 ∨ x2 ∨ x3 ) (x1 ∨ x2 ) (x2 ∨ x3 )x2 = 1(x1 ∨ x3 ) x1 x3x1 = x3 = 0falseПояснения:Деполяризация для x1 и x3x2 = 0x1 ∨ x3x1 = x3 = 1trueSAT: DPLLПример(x1 ∨ x2 ∨ x3 ) (x1 ∨ x2 ∨ x3 ) (x1 ∨ x2 ) (x2 ∨ x3 )x2 = 1(x1 ∨ x3 ) x1 x3x1 = x3 = 0falseПояснения:СТОП: формула выполнимаx2 = 0x1 ∨ x3x1 = x3 = 1trueКонец лекции 2.