Schoeningin algoritmi

Schöningin algoritmi on Uwe Schöningin vuonna 1999 ehdottama todennäköisyysalgoritmi Boolen kaavojen tyydyttävyysongelman ratkaisemiseksi k - konjunktiivisessa normaalimuodossa .

Kuvaus 3-SAT-ratkaisulle

  1. Sinulle annetaan Boolen kaava 3-konjunktiivisessa normaalimuodossa .
  2. Toista kerran:
    1. Aseta satunnaisesti joukko muuttujia .
    2. Jos looginen kaava on tosi, tulosta ja poistu.
    3. Toista kerran:
      1. Valitse disjunktio , joka ei tyydytä .
      2. Valitse muuttuja .
      3. Asenna .
      4. Jos looginen kaava on tosi, tulosta ja poistu.
  3. Tulostus " mahdoton".

Aika monimutkaisuus

Schoeningin algoritmilla on aikamonimutkaisuus , jossa on muuttujien määrä ja disjunktioiden määrä, edellyttäen, että Boolen kaavan tyydyttävyys tarkistetaan . Jos Boolen kaava ei ole mahdollinen, niin Schoeningin algoritmi palauttaa aina oikean tuloksen.

Virhearvio

Jos Boolen kaava on tyydyttävä, virhetodennäköisyys on aina pienempi . Todistuksessa merkitään muuttujien joukko, jolle on tosi, ja myös todennäköisyys, että algoritmi löytää sisäkkäisestä silmukasta (tätä vaihetta kutsutaan myös paikalliseksi hauksi). Siten on alaraja todennäköisyydelle löytää tyydyttävä muuttujajoukko paikallishaun avulla. Seuraavaksi näytämme sen . Kahden joukon välinen etäisyys on niissä olevien erillisten bittien lukumäärä. Määritelkäämme luokka joukoksi kokoelmia, jotka poikkeavat hieman joukosta , ts. . Siten kaikki sarjat voidaan jakaa luokkiin. Reilun vuoksi . Todennäköisyys valita elementti satunnaisesti joukosta on . Paikallisessa haussa huomioidaan disjunktio , jota generoitu muuttujajoukko ei tyydytä, ja jos joukko valitaan satunnaisesti uudelleen, todennäköisyys löytää tyydyttävä muuttuja on yhtä suuri kuin . Näin ollen todennäköisyys siirtyä luokasta luokkaan on vähintään . Todennäköisyys päästä luokasta luokkaan on yhtä suuri kuin maksimi . Olkoon todennäköisyys päästä luokasta portaittain luokkaan , ts. löytää ratkaisu . Tässä tapauksessa missä on mahdollisten siirtymien määrä suuntaan ja todennäköisyys päästä ulos luokasta on . Kun kaavat on korvattu toisillaan ja laskettu likimääräisesti tulos, saadaan todennäköisyys sille, että paikallishaun aikana ei löydy tyydyttävää muuttujajoukkoa, joka on yhtä suuri kuin , ja tällaisten hakujen jälkeen todennäköisyys on jo yhtä suuri kuin .

Muistiinpanot

  1. T. Schoning. Todennäköisyyspohjainen algoritmi k-SAT:lle ja rajoitteiden tyytyväisyysongelmille  // 40th Annual Symposium on Foundations of Computer Science (Cat. No.99CB37039). — New York City, NY, USA: IEEE Comput. Soc, 1999, s. 410-414 . — ISBN 978-0-7695-0409-4 . - doi : 10.1109/SFCS.1999.814612 .