5.2. Lipton megoldása a SAT-ra

Adleman kísérlete után Lipton 1995-ben publikálta a SAT megoldására szolgáló kísérletét. Legyen adott egy konjunktív normálformájú formula, pl.

Tekintsük az 5.3. ábrán látható gráfot és készítsük el a DNS kódját (a hat csúcsnak és a nyolc élnek), hasonlóan ahhoz, ahogy Adleman is kódolta a kiindulási gráfot.

5.3. ábra - Az Az három változóval rendelkező formulákhoz használható gráf. három változóval rendelkező formulákhoz használható gráf.

Az három változóval rendelkező formulákhoz használható gráf.

Hosszmérés segítségével kiválaszthatjuk a maximális hosszú (jelen esetben 3 csúcsot tartalmazó) utakat, illetve azt a kódot, ami az ezeken levő csúcsokat jelenti. Könnyen belátható, hogy az ilyen utak minden változónak, vagy a negáltjának megfelelő csúcs kódját tartalmazzák, sőt minden változóra pontosan az egyiket ezek közül. Tulajdonképpen ezek a DNS láncok egy-egy kiértékelésnek felelnek meg, és minden kiértékelés létrejöhet, mivel megjelenik a gráfban, mint maximális hosszúságú út.

Ezután a lépés után sorra vesszük a formulánk elemi diszjunkcióit, és mindegyikre a következő műveleteket végezzük. A kiértékelés-kódokat tartalmazó levest sokszorosítjuk, és annyi részre osztjuk, ahány literál található az adott elemi diszjunkcióban. Minden ilyen részhez hozzá rendeljük az elemi diszjunkció egy-egy literálját, és pecázás segítségével csak azokat a láncokat tartjuk meg, amelyekben az adott literálnak megfelelő csúcs kódja szerepel. A leveseket összeöntjük, így azok a láncok maradnak meg, amelyek olyan kiértékeléseket kódolnak, amelyben az adott elemi diszjunkció igaz.

Az eljárást megismételve az összes elemi diszjunkcióra, végül csak azok a láncok maradnak az oldatban, amelyek olyan kiértékeléshez tartoznak, amelyek kielégítik az összes elemi diszjunkciót, és így az (egész) formulát. Az 5.4. ábra mutatja, hogy a példaként felírt formula esetén, hogyan is néz ki a kísérlet. Végül csak azt kell ellenőriznünk, hogy maradt-e az oldatban (kiértékelést kódoló) molekula.

5.4. ábra - A példaként adott formula elemi diszjunkcióiban levő literálokat pecázzuk.

A példaként adott formula elemi diszjunkcióiban levő literálokat pecázzuk.

Az 5.3. ábrán látható gráfot, illetve azt a levest, amiben ez a gráf van kódolva, minden háromváltozós formula kielégíthetőségének vizsgálatához használhatjuk, több változót tartalmazó formulákhoz nagyobb kiindulási gráfot kell készíteni.