Azərbaycanca AzərbaycancaБеларускі БеларускіDansk DanskDeutsch DeutschEspañola EspañolaFrançais FrançaisIndonesia IndonesiaItaliana Italiana日本語 日本語Қазақ ҚазақLietuvos LietuvosNederlands NederlandsPortuguês PortuguêsРусский Русскийසිංහල සිංහලแบบไทย แบบไทยTürkçe TürkçeУкраїнська Українська中國人 中國人United State United StateAfrikaans Afrikaans
Підтримка
www.wikidata.uk-ua.nina.az

Алгоритм Девіса Патнема Логемана Лавленд це повний алгоритм пошуку з поверненням для визначення здійсненності булевих фо

Алгоритм DPLL

Алгоритм DPLL

Алгоритм Девіса-Патнема-Логемана-Лавленд — це повний алгоритм пошуку з поверненням для визначення здійсненності булевих формул, записаних в кон'юнктивній нормальній формі (КНФ) для вирішення завдання CNF-SAT.

image
Алгоритм пошуку з поверненням DPLL

Алгоритм був опублікований в 1962 році Мартіном Девісом, Гіларі Патнемом, Джорджем Логеманом й Дональдом Лавленд та є удосконаленням більш раннього алгоритму Девіса-Патнема, методу, заснованого на правилі резолюцій, розробленого Девісом та Патнемом в 1960 році.

DPLL — високо-ефективний алгоритм якому вже 50 років але все ще лежить в основі більшості ефективних вирішувачів для SAT, а також для систем автоматичного доведення теорем та фрагментів логіки першого порядку.

Реалізації та додатки

Завдання здійсненності булевих формул важливо як з теоретичної, так й з практичної точок зору. В теорії складності це перше завдання для якої були доведена приналежність клас NP-повні задачі. Також вона може з'являтися в самих різних практичних додатків, наприклад перевірка моделей, складання розкладів, діагностика.

Даний напрямок був та залишається областю досліджень, що розвивається. Щорічно проводяться змагання між різними людьми котрі вирішують SAT. Сучасні реалізації алгоритму DPLL, такі як Chaff and zChaff, GRASP або MINISAT займають перші позиції протягом останніх років. Інший тип додатків, в яких часто використовується DPLL — це системи автоматичного доведення теорем.

Опис алгоритму

Основний алгоритм з поверненням починається з вибору змінної, присвоєння їй значення «істина», спрощення формули та потім рекурсивним чином перевірити спрощення формули на здійсненність; якщо вона здійсненна, то вихідна формула теж здійсненна. Інакше, процедура повторюється, але для обраної змінної встановлюється значення «брехня». Цей підхід називається «правилом розбивки», так як він розбиває завдання на дві більш прості підзадачі. Крок спрощення полягає в тому, що з формули дістаються всі диз'юнкти, які стають істинними після присвоєння обраній змінній значення «істина», та видалення від решти диз'юнкт всіх входжень цієї змінної зі значенням «брехні».

Алгоритм DPLL дозволяє поліпшити основний алгоритм з поверненням за рахунок використання наступних правил на кожному кроці:

Поширення змінної

Якщо диз'юнкта містить рівно одну змінну, якій ще не задали значення, ця диз'юнкта може прийняти значення «істина» тільки в разі присвоєння змінній значення, яке зробить її істинною («істина», якщо змінна входить в диз'юнкт без заперечення та «брехня», якщо змінна з запереченням). Таким чином, не потрібно робити вибір на даному етапі. На практиці за цим слідує багато присвоєнь змінним значень, та через це істотно скорочується кількість варіантів перебору.

Виняток «чистих» змінних

Якщо деяка змінна входить в формулу тільки з однієї «полярністю», тобто без заперечень, або тільки з запереченнями, вона називається чистою. «Чистим» змінним завжди можна задати значення так, що всі утримуючи її диз'юнкти стануть істинними. Таким чином, ці диз'юнкти не впливатимуть на простір варіантів та їх можна буде видалити.

Нездійсненність, при даних конкретних значеннях змінних, визначається коли одна з диз'юнкт стає «порожня», тобто всім її змінним задаються значення таким чином, що їх входження стають помилковими. Здійснимість формули констатується або коли всім змінним задані значення так, що не виникає «порожніх» диз'юнкт, або (в сучасних реалізація) кожна диз'юнкта дорівнює істини. Нездійсненність формули може бути встановлена тільки після закінчення перебору. Алгоритм DPLL може бути виражений за допомогою наступного псевдокоду, де знаком Φ позначена формула в кон'юнктивній нормальній формі (КНФ):

Алгоритм DPLL Вхідні дані: Набір диз'юнкт формули Φ. Вихідні дані: Значення істинності

Псевдокод:

function DPLL(Φ) if Φ - набір виконуваних диз'юнкт then return true; if Φ містить порожню диз'юнкту then return false; for each диз'юнкти з однією змінною l in Φ Φ ← unit-propagate(l, Φ); for each l яка зустрічається в "чистому" вигляді in Φ Φ ← pure-literal-assign(l, Φ); l ← choose-literal(Φ); return DPLL(Φ&l) or DPLL(Φ&not(l));

У цьому псевдокоді unit-propagate(l, Φ) й pure-literal-assign(l, Φ) — це функції, які повертають результат застосовуваний до змінної l в формулі Φ — поширення змінної та правила виключення «чистої змінної». Іншими словами, вони замінють кожне входження змінної lзначенням «істина» та кожне входження змінної з запереченням not l значенням «брехня» у формулі Φ, а потім спрощують результативну формулу. Наведений псевдокод повертає тільки відповідь — чи виконує формулу останній з присвоєних наборів значень чи ні. У сучасних реалізаціях, часткові виконувані набори, теж повертаються у разі успіху.

Алгоритм залежить від вибору «змінної розгалуження», тобто змінної, яка вибирається на черговому кроці алгоритму з поверненням присвоєння їй певного значення. Таким чином, це не один алгоритм, а ціле сімейство алгоритмів, по одному на кожен можливий спосіб вибору «змінних розгалуження». Ефективність алгоритму сильно залежить від цього вибору. Час роботи алгоритму (для яких може бути image або рости експоненціально) в залежності від вибору «змінних розгалуження». Методи вибору — евристичні техніки, які називаються також «евристиками для розгалуження» (branching heuristics).

Візуалізація

Девіс, Логемана, Лавленд (1962) розробили цей алгоритм. Деякі властивості алгоритму:

  • Він засновується для пошуку.
  • Він є основою для багатьох сучасних вирішувачів SAT.
  • Він не використовує джерела введено в 1996 році.

Приклад з візуалізацією алгоритму DPLL, що має хронологічні джерела:

  • image
    Всі можливі випадки КНФ формул.
  • image
    Вибираємо змінну.
  • image
    Приймаємо рішення, змінна а = False (0), таким чином, зелені положення стають True.
  • image
    Після кількох рішень, ми знаходимо імплікаційний граф, який призводить до конфлікту.
  • image
    Тепер повертаємося назад та надаємо значення змінній.
  • image
    Рішення все ще приводить до іншого конфлікту.
  • image
    Повертаємося на попередній рівень.
  • image
    Зробили нове рішення але це призводить до конфлікту також.
  • image
    Зробили ще одне зміщення але знову це призводить до конфлікту.
  • image
    Повертаємося на попередній рівень.
  • image
    Продовжуємо таким же чином до остаточного імплікаційного графу.

Сучасні дослідження

Поточні дослідження щодо поліпшення алгоритму виконуються в трьох напрямках:

  • визначення різних оптимізуючих методів вибору «змінної розгалуження»;
  • розробка нових структур даних для прискорення роботи алгоритму, особливо для поширення змінної;
  • розробка різних варіантів базового алгоритму перебору з поверненням.

Останній напрям включає «нехронологічні повернення» та запам'ятовування помилкових випадків. Ці поліпшення можна описати як метод повернення після досягнення помилкових диз'юнкт, при якому запам'ятовується, яке саме привласнення значення змінної спричинило цей результат, щоб в подальшому уникнути даремних обчислень, тим самим скоротити час роботи.

Новіший алгоритм — метод Сталмарка — відомий з 1990 року, використовується для вирішення задачі SAT. На основі DPLL-алгоритму в середині 1990-х був створений CDCL-алгоритм.

Зв'язок з іншими

Алгоритми DPLL оснований на нездійсненних випадках котрі відповідають доказам спрощення дозволу дерева.

Див. також

  • [en]
  • [en]
  • [en]
  • [en]

Посилання

  1. LLC, Revolvy,. "Davis–Putnam algorithm" on Revolvy.com. www.revolvy.com (англ.). Процитовано 28 квітня 2017.
  2. . dai.fmph.uniba.sk (амер.). Архів оригіналу за 23 лютого 2017. Процитовано 28 квітня 2017.
  3. committee, SATComp Organizing. . www.satcompetition.org. Архів оригіналу за 12 лютого 2005. Процитовано 19 квітня 2017.
  4. . www.princeton.edu. Архів оригіналу за 19 квітня 2017. Процитовано 19 квітня 2017.
  5. MiniSat Page. minisat.se. Архів оригіналу за 20 квітня 2012. Процитовано 19 квітня 2017.
  6. Лекториум (24 липня 2013), DPLL алгоритм с вероятностным отсечением: оценка времени работы | Елена Иконникова | CSC | Лекториум, процитовано 28 квітня 2017

Література

  • R. Dechter; I. Rish. «Directional Resolution: The Davis–Putnam Procedure, Revisited». In J. Doyle and E. Sandewall and P. Torasso. Principles of Knowledge Representation and Reasoning: Proc. of the Fourth International Conference (KR'94). Starswager18. pp. 134—145.
  • John Harrison (2009). Handbook of practical logic and automated reasoning. Cambridge University Press. pp. 79–90. .

Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет

Algoritm Devisa Patnema Logemana Lavlend ce povnij algoritm poshuku z povernennyam dlya viznachennya zdijsnennosti bulevih formul zapisanih v kon yunktivnij normalnij formi KNF dlya virishennya zavdannya CNF SAT Algoritm poshuku z povernennyam DPLL Algoritm buv opublikovanij v 1962 roci Martinom Devisom Gilari Patnemom Dzhordzhem Logemanom j Donaldom Lavlend ta ye udoskonalennyam bilsh rannogo algoritmu Devisa Patnema metodu zasnovanogo na pravili rezolyucij rozroblenogo Devisom ta Patnemom v 1960 roci DPLL visoko efektivnij algoritm yakomu vzhe 50 rokiv ale vse she lezhit v osnovi bilshosti efektivnih virishuvachiv dlya SAT a takozh dlya sistem avtomatichnogo dovedennya teorem ta fragmentiv logiki pershogo poryadku Realizaciyi ta dodatkiZavdannya zdijsnennosti bulevih formul vazhlivo yak z teoretichnoyi tak j z praktichnoyi tochok zoru V teoriyi skladnosti ce pershe zavdannya dlya yakoyi buli dovedena prinalezhnist klas NP povni zadachi Takozh vona mozhe z yavlyatisya v samih riznih praktichnih dodatkiv napriklad perevirka modelej skladannya rozkladiv diagnostika Danij napryamok buv ta zalishayetsya oblastyu doslidzhen sho rozvivayetsya Shorichno provodyatsya zmagannya mizh riznimi lyudmi kotri virishuyut SAT Suchasni realizaciyi algoritmu DPLL taki yak Chaff and zChaff GRASP abo MINISAT zajmayut pershi poziciyi protyagom ostannih rokiv Inshij tip dodatkiv v yakih chasto vikoristovuyetsya DPLL ce sistemi avtomatichnogo dovedennya teorem Opis algoritmuOsnovnij algoritm z povernennyam pochinayetsya z viboru zminnoyi prisvoyennya yij znachennya istina sproshennya formuli ta potim rekursivnim chinom pereviriti sproshennya formuli na zdijsnennist yaksho vona zdijsnenna to vihidna formula tezh zdijsnenna Inakshe procedura povtoryuyetsya ale dlya obranoyi zminnoyi vstanovlyuyetsya znachennya brehnya Cej pidhid nazivayetsya pravilom rozbivki tak yak vin rozbivaye zavdannya na dvi bilsh prosti pidzadachi Krok sproshennya polyagaye v tomu sho z formuli distayutsya vsi diz yunkti yaki stayut istinnimi pislya prisvoyennya obranij zminnij znachennya istina ta vidalennya vid reshti diz yunkt vsih vhodzhen ciyeyi zminnoyi zi znachennyam brehni Algoritm DPLL dozvolyaye polipshiti osnovnij algoritm z povernennyam za rahunok vikoristannya nastupnih pravil na kozhnomu kroci Poshirennya zminnoyi Yaksho diz yunkta mistit rivno odnu zminnu yakij she ne zadali znachennya cya diz yunkta mozhe prijnyati znachennya istina tilki v razi prisvoyennya zminnij znachennya yake zrobit yiyi istinnoyu istina yaksho zminna vhodit v diz yunkt bez zaperechennya ta brehnya yaksho zminna z zaperechennyam Takim chinom ne potribno robiti vibir na danomu etapi Na praktici za cim sliduye bagato prisvoyen zminnim znachen ta cherez ce istotno skorochuyetsya kilkist variantiv pereboru Vinyatok chistih zminnih Yaksho deyaka zminna vhodit v formulu tilki z odniyeyi polyarnistyu tobto bez zaperechen abo tilki z zaperechennyami vona nazivayetsya chistoyu Chistim zminnim zavzhdi mozhna zadati znachennya tak sho vsi utrimuyuchi yiyi diz yunkti stanut istinnimi Takim chinom ci diz yunkti ne vplivatimut na prostir variantiv ta yih mozhna bude vidaliti Nezdijsnennist pri danih konkretnih znachennyah zminnih viznachayetsya koli odna z diz yunkt staye porozhnya tobto vsim yiyi zminnim zadayutsya znachennya takim chinom sho yih vhodzhennya stayut pomilkovimi Zdijsnimist formuli konstatuyetsya abo koli vsim zminnim zadani znachennya tak sho ne vinikaye porozhnih diz yunkt abo v suchasnih realizaciya kozhna diz yunkta dorivnyuye istini Nezdijsnennist formuli mozhe buti vstanovlena tilki pislya zakinchennya pereboru Algoritm DPLL mozhe buti virazhenij za dopomogoyu nastupnogo psevdokodu de znakom F poznachena formula v kon yunktivnij normalnij formi KNF Algoritm DPLL Vhidni dani Nabir diz yunkt formuli F Vihidni dani Znachennya istinnosti Psevdokod function DPLL F if F nabir vikonuvanih diz yunkt then return true if F mistit porozhnyu diz yunktu then return false for each diz yunkti z odniyeyu zminnoyu l in F F unit propagate l F for each l yaka zustrichayetsya v chistomu viglyadi in F F pure literal assign l F l choose literal F return DPLL F amp l or DPLL F amp not l U comu psevdokodi unit propagate l F j pure literal assign l F ce funkciyi yaki povertayut rezultat zastosovuvanij do zminnoyi l v formuli F poshirennya zminnoyi ta pravila viklyuchennya chistoyi zminnoyi Inshimi slovami voni zaminyut kozhne vhodzhennya zminnoyi lznachennyam istina ta kozhne vhodzhennya zminnoyi z zaperechennyam not l znachennyam brehnya u formuli F a potim sproshuyut rezultativnu formulu Navedenij psevdokod povertaye tilki vidpovid chi vikonuye formulu ostannij z prisvoyenih naboriv znachen chi ni U suchasnih realizaciyah chastkovi vikonuvani nabori tezh povertayutsya u razi uspihu Algoritm zalezhit vid viboru zminnoyi rozgaluzhennya tobto zminnoyi yaka vibirayetsya na chergovomu kroci algoritmu z povernennyam prisvoyennya yij pevnogo znachennya Takim chinom ce ne odin algoritm a cile simejstvo algoritmiv po odnomu na kozhen mozhlivij sposib viboru zminnih rozgaluzhennya Efektivnist algoritmu silno zalezhit vid cogo viboru Chas roboti algoritmu dlya yakih mozhe buti c o n s t displaystyle const abo rosti eksponencialno v zalezhnosti vid viboru zminnih rozgaluzhennya Metodi viboru evristichni tehniki yaki nazivayutsya takozh evristikami dlya rozgaluzhennya branching heuristics Vizualizaciya Devis Logemana Lavlend 1962 rozrobili cej algoritm Deyaki vlastivosti algoritmu Vin zasnovuyetsya dlya poshuku Vin ye osnovoyu dlya bagatoh suchasnih virishuvachiv SAT Vin ne vikoristovuye dzherela vvedeno v 1996 roci Priklad z vizualizaciyeyu algoritmu DPLL sho maye hronologichni dzherela Vsi mozhlivi vipadki KNF formul Vibirayemo zminnu Prijmayemo rishennya zminna a False 0 takim chinom zeleni polozhennya stayut True Pislya kilkoh rishen mi znahodimo implikacijnij graf yakij prizvodit do konfliktu Teper povertayemosya nazad ta nadayemo znachennya zminnij Rishennya vse she privodit do inshogo konfliktu Povertayemosya na poperednij riven Zrobili nove rishennya ale ce prizvodit do konfliktu takozh Zrobili she odne zmishennya ale znovu ce prizvodit do konfliktu Povertayemosya na poperednij riven Prodovzhuyemo takim zhe chinom do ostatochnogo implikacijnogo grafu Suchasni doslidzhennyaPotochni doslidzhennya shodo polipshennya algoritmu vikonuyutsya v troh napryamkah viznachennya riznih optimizuyuchih metodiv viboru zminnoyi rozgaluzhennya rozrobka novih struktur danih dlya priskorennya roboti algoritmu osoblivo dlya poshirennya zminnoyi rozrobka riznih variantiv bazovogo algoritmu pereboru z povernennyam Ostannij napryam vklyuchaye nehronologichni povernennya ta zapam yatovuvannya pomilkovih vipadkiv Ci polipshennya mozhna opisati yak metod povernennya pislya dosyagnennya pomilkovih diz yunkt pri yakomu zapam yatovuyetsya yake same privlasnennya znachennya zminnoyi sprichinilo cej rezultat shob v podalshomu uniknuti daremnih obchislen tim samim skorotiti chas roboti Novishij algoritm metod Stalmarka vidomij z 1990 roku vikoristovuyetsya dlya virishennya zadachi SAT Na osnovi DPLL algoritmu v seredini 1990 h buv stvorenij CDCL algoritm Zv yazok z inshimiAlgoritmi DPLL osnovanij na nezdijsnennih vipadkah kotri vidpovidayut dokazam sproshennya dozvolu dereva Div takozh en en en en PosilannyaLLC Revolvy Davis Putnam algorithm on Revolvy com www revolvy com angl Procitovano 28 kvitnya 2017 dai fmph uniba sk amer Arhiv originalu za 23 lyutogo 2017 Procitovano 28 kvitnya 2017 committee SATComp Organizing www satcompetition org Arhiv originalu za 12 lyutogo 2005 Procitovano 19 kvitnya 2017 www princeton edu Arhiv originalu za 19 kvitnya 2017 Procitovano 19 kvitnya 2017 MiniSat Page minisat se Arhiv originalu za 20 kvitnya 2012 Procitovano 19 kvitnya 2017 Lektorium 24 lipnya 2013 DPLL algoritm s veroyatnostnym otsecheniem ocenka vremeni raboty Elena Ikonnikova CSC Lektorium procitovano 28 kvitnya 2017LiteraturaR Dechter I Rish Directional Resolution The Davis Putnam Procedure Revisited In J Doyle and E Sandewall and P Torasso Principles of Knowledge Representation and Reasoning Proc of the Fourth International Conference KR 94 Starswager18 pp 134 145 John Harrison 2009 Handbook of practical logic and automated reasoning Cambridge University Press pp 79 90 ISBN 978 0 521 89957 4

Дата публікації:
Топ