DPLL

DPLL ( Davis-Putnam-Logeman-Loveland-algoritmi ) on täydellinen backtracking -algoritmi CNF-SAT- ongelman ratkaisemiseksi - määrittää konjunktiiviseen normaalimuotoon  kirjoitettujen Boolen kaavojen tyydyttävyyden .

Julkaisijat Martin Davis , Hilary Putnam , George Logeman ja Donald Loveland vuonna 1962 parannuksena aikaisempaan Davis-Putnam-algoritmiin , joka perustuu resoluutiosääntöön .

Se on erittäin tehokas algoritmi ja pysyy merkityksellisenä puolen vuosisadan jälkeen, ja sitä käytetään useimmissa SAT -ratkaisijoissa ja automaattisissa todistusjärjestelmissä ensimmäisen asteen logiikan fragmenteille [1] .

Toteutukset ja sovellukset

Boolen kaavojen tyydyttävyysongelma on tärkeä sekä teoreettisesta että käytännön näkökulmasta. Monimutkaisuusteoriassa tämä on ensimmäinen ongelma, jolle kuuluminen NP-täydellisten ongelmien luokkaan on todistettu . Se voi esiintyä myös monissa käytännön sovelluksissa, kuten mallin tarkistuksessa , aikataulutuksessa ja diagnostiikassa.

Tämä alue oli ja on edelleen kasvava tutkimusalue, kilpailuja järjestetään vuosittain eri SAT-ratkaisijoiden välillä [2] ; DPLL-algoritmin nykyaikaiset toteutukset, kuten Chaff , zChaff [3] [4] , GRASP ja Minisat [5] , sijoittuvat tällaisissa kilpailuissa ensimmäiselle sijalle.

Toinen sovellustyyppi, jossa DPLL:ää käytetään usein, ovat lauseiden todistavat järjestelmät .

Algoritmin kuvaus

Peruutusalgoritmi alkaa valitsemalla muuttuja, asettamalla sen arvoon tosi, yksinkertaistamalla kaavaa ja testaamalla sitten rekursiivisesti yksinkertaistetun kaavan toteutettavuutta. jos se on mahdollista, niin alkuperäinen kaava on myös toteutettavissa; muussa tapauksessa toimenpide toistetaan, mutta valitun muuttujan arvoksi asetetaan epätosi. Tätä lähestymistapaa kutsutaan "jakosäännöksi", koska se jakaa tehtävän kahteen yksinkertaisempaan osatehtävään. Yksinkertaistamisvaiheessa poistetaan kaavasta kaikki lauseet, jotka muuttuvat todeksi sen jälkeen, kun valitulle muuttujalle on annettu arvo "true", ja poistetaan muista lauseista kaikki tämän muuttujan esiintymät, joista tulee epätosi.

DPLL-algoritmi parantaa perusperuutusalgoritmia käyttämällä jokaisessa vaiheessa seuraavia sääntöjä:

Muuttujan leviäminen jos lauseessa on täsmälleen yksi muuttuja, jolle ei ole vielä annettu arvoa, lauseesta voi tulla tosi vain, jos muuttujalle on annettu arvo, joka tekee siitä tosi (tosi jos muuttuja on lauseessa ilman negatiivista ja false jos muuttuja on negatiivinen). Tässä vaiheessa ei siis tarvitse tehdä valintaa. Käytännössä tätä seuraa muuttujien määräysten sarja, mikä vähentää merkittävästi iterointivaihtoehtojen määrää. "Puhtaiden" muuttujien poissulkeminen jos jokin muuttuja tulee kaavaan vain yhdellä "polariteetilla" (eli joko vain ilman negaatioita tai vain negaatioilla), sitä kutsutaan puhtaaksi . "Puhtaille" muuttujille voidaan aina antaa arvo siten, että kaikista niitä sisältävistä lauseista tulee tosi. Näin ollen nämä lausekkeet eivät vaikuta muunnelmien tilaan, ja ne voidaan poistaa.

Tiettyjen muuttujien arvojen tyydyttämättömyys määritellään, kun yksi lauseista tulee "tyhjäksi", eli kaikille sen muuttujille annetaan arvot siten, että niiden esiintyminen (negatiolla tai ilman) muuttuu vääriksi. Kaavan tyydyttävyys ilmoitetaan joko silloin, kun kaikki muuttujat on asetettu arvoihin niin, ettei niissä ole "tyhjiä" lauseita, tai nykyaikaisissa toteutuksissa, jos kaikki lauseet ovat tosi. Koko kaavan tyydyttämättömyys voidaan todeta vasta tyhjentävän luettelon päätyttyä.

DPLL-algoritmi voidaan ilmaista käyttämällä seuraavaa pseudokoodia, jossa Φ tarkoittaa kaavaa konjunktiivisessa normaalimuodossa:

Syöttötiedot: Joukko lauseita, joilla on kaava Φ. Tulos: Totuusarvo funktio DPLL(Φ) , jos Φ on suoritettavien lauseiden joukko, palauttaa tosi ; jos Φ sisältää tyhjän lauseen , palauttaa epätosi; jokaiselle lausekkeelle yhdestä muuttujasta l arvoon Φ Φ yksikkö-etenevä ( l , Φ); jokaiselle muuttujalle l , joka esiintyy puhtaassa muodossa Φ:ssä Φ puhdas-kirjaimellinen-määritä ( l , Φ); l valita-kirjaimellinen (Φ); palauttaa DPLL (Φ&l) tai DPLL (Φ¬(l));

Tässä pseudokoodissa unit-propagate(l, Φ), ja pure-literal-assign(l, Φ) ovat funktioita, jotka palauttavat tuloksen soveltamisesta muuttujaan lja muuttujan etenemiskaavaan Φja "puhtaan muuttujan" poissulkemissääntöön. Toisin sanoen ne korvaavat jokaisen muuttujan lesiintymän tosi-muodolla ja jokaisen negatiivisen muuttujan esiintymän not lepätosi-muodolla kaavassa Φja yksinkertaistavat sitten tuloksena olevaa kaavaa. Yllä oleva pseudokoodi palauttaa vain vastauksen - täyttääkö viimeinen määritetyistä arvojoukoista kaavan. Nykyaikaisissa toteutuksissa myös osittaiset suoritussarjat tuovat voittoa.

Algoritmi riippuu "haaramuuttujan" valinnasta, eli muuttujasta, joka valitaan algoritmin seuraavassa vaiheessa paluulla. määrittääksesi sille tietyn arvon. Kyseessä ei siis ole yksi algoritmi, vaan kokonainen algoritmien perhe, yksi kullekin mahdolliselle "haaramuuttujien" valintatavalle. Algoritmin tehokkuus riippuu suuresti tästä valinnasta: on esimerkkejä ongelmista, joissa algoritmin ajoaika voi olla vakio tai kasvaa eksponentiaalisesti riippuen "haaramuuttujien" valinnasta. Valintamenetelmät ovat heuristisia tekniikoita, ja niitä kutsutaan myös "haarautumisheuristiksi" [6] .

Nykytutkimus

Nykyinen tutkimus algoritmin parantamiseksi tehdään kolmeen suuntaan: erilaisten optimointimenetelmien määrittely "haaramuuttujan" valitsemiseksi; uusien tietorakenteiden kehittäminen algoritmin nopeuttamiseksi, erityisesti muuttujan leviämistä varten; ja peruspalautusalgoritmin eri muunnelmien kehittäminen. Viimeinen suunta sisältää "ei-kronologisen perääntymisen" ja huonojen tapausten muistamisen . Näitä parannuksia voidaan kuvata menetelmäksi palauttaa väärän lausekkeen saavuttamisen jälkeen, jolloin muistetaan mikä tietty arvon antaminen muuttujalle aiheutti tämän tuloksen, jotta vältytään täsmälleen samalta laskusarjalta tulevaisuudessa, mikä vähentää työaika.

Vuodesta 1990 lähtien on tunnettu uudempi algoritmi, Stalmark-menetelmä. Myös vuodesta 1986 lähtien SAT-ongelman ratkaisemiseen on käytetty päätöskaavioita.

DPLL-algoritmiin perustuva CDCL-algoritmi luotiin 1990-luvun puolivälissä ja siitä on tullut laajalti käytössä .

Muistiinpanot

  1. ↑ Nieuwenhuis, Robert; Oliveras, Albert & Tinelly, Cesar (2004), Abstract DPLL and Abstract DPLL Modulo Theories , Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2004, Proceedings : 36–50 , < http://www.lsi.upc.edu /~roberto/papers/lpar04.pdf > Arkistoitu 17. marraskuuta 2011 Wayback Machinessa 
  2. ↑ Kansainvälisten SAT-kilpailujen verkkosivu , la! live , < http://www.satcompetition.org/ > Arkistoitu 12. helmikuuta 2005 Wayback Machinessa 
  3. ↑ zChaff-verkkosivusto , < http://www.princeton.edu/~chaff/zchaff.html > Arkistoitu 19. huhtikuuta 2017 Wayback Machinessa 
  4. ↑ Chaff-sivusto , < http://www.princeton.edu/~chaff/ > Arkistoitu 23. helmikuuta 2020 Wayback Machinessa 
  5. ↑ Minisat-verkkosivusto . Arkistoitu alkuperäisestä 20. huhtikuuta 2012.
  6. ↑ Marques-silva, Joao. Haaroittuvan heuristiikan vaikutus propositional satisfiability -algoritmeihin  (englanniksi)  // In 9th Portuguese Conference on Artificial Intelligence (EPIA) : Journal. - 1999. - doi : 10.1.1.111.9184 . Arkistoitu alkuperäisestä 14. huhtikuuta 2012.

Kirjallisuus