A SAT (satisfyability, azaz kielégíthetőség) egy eldöntési probléma.
Adott egy logikai formula és az érdekel minket, hogy hozzá tudunk-e rendelni a változókhoz igaz/hamis értékeket úgy, hogy a formula igazzá váljon. Pl:
$$(x_1\lor \lnot x_2)\land (x_1\lor x_3)\land ((x_2 \lor \lnot x_3)\land \lnot x_4 )$$Ha ez lehetséges, akkor azt mondjuk, hogy a formula kielégíthető. Ez a konkrét példa kielégíthető, egy lehetséges kielégítés: $x_1,x_2,x_3$ igaz és $x_4$ hamis.
A SAT azért érdekes, mert sok más feladat visszavezethető rá. Tehát ha hatékonyan meg tudjuk oldani, egyszerre sok feladatra nyerünk megoldási módszert.
Pár definíció:
Pl:
$$(x_1\lor \lnot x_2 \lor x_3)\land (x_1\lor x_2)\land (x_2 \lor \lnot x_3\lor \lnot x_5 )$$Tétel: Minden formula átalakítható konjuktív normálformára.
| $x_1$ | $x_2$ | $x_3$ | $$(x_1 \land x_2) \lor (\lnot x_2 \land x_3)$$ | |
|---|---|---|---|---|
| 0 | 0 | 0 | 0 | |
| 0 | 0 | 1 | 1 | |
| 0 | 1 | 0 | 0 | |
| 0 | 1 | 1 | 0 | |
| 1 | 0 | 0 | 0 | |
| 1 | 0 | 1 | 1 | |
| 1 | 1 | 0 | 1 | |
| 1 | 1 | 1 | 1 |
Minden hamis sorra garantálni akarjuk, hogy nem fordulhat elő:
$$(x_1\lor x_2 \lor x_3) \land(x_1\lor \lnot x_2 \lor x_3) \land (x_1\lor \lnot x_2 \lor \lnot x_3) \land(\lnot x_1\lor x_2 \lor x_3) $$Nehéz, a feladat NP teljes!
A 3-SAT feladatban még azt is feltesszük, hogy minden klóz legfeljebb 3 literált tartalmaz. Még ekkor is nehéz!
A 2-SAT feladatban még azt is feltesszük, hogy minden klóz legfeljebb 2 literált tartalmaz. Na ez már könnyű.
Egy egyszerű rekurzív megoldás:
Első javítás: Ellenőrzés helyett frissítsük a formulát. Ha egy $x$ változót igazra állítottunk, eldobhatunk minden klózt, ahol $x$ szerepel. Ha pedig hamisra, akkor minden klózt, ahol $\lnot x$ szerepel.
Ha egy $x$ változót igazra állítottunk, akkor minden klózból törölhető $\lnot x$ ahol szerpel. Ha pedig hamisra, akkor minden klózból törölhető $x$.
Még két ötlet:
unit propagation: Ha a 4. lépés után van olyan klóz, amiben csak egyetlen változó van, akkor annak tudjuk az értékét. Annak beállítása után újra érdemes a 3. és 4. lépést végrehajtani.
pure ellimination: Ha egy változó csak pozitív / csak negatív literálként szerpel akkor megéri bállítani igazra/hamisra, hiszen semmit sem ronthat el. Tehát minden őt tartalmazó klóz eldobható.
Ez csak a stratégia, és a lépések megvalósításán nagyon sok múlik!
Egyik ötlet: "Watch list"-ek használata. Minden klózhoz hozzárendeljük az egyik literálját. Egy klózt nem kell addig ellenőrizni, amíg a kijelölt változóhoz nem érünk, hiszen addig nem lehetünk benne biztosak, hogy hamisat adna a klóz. Amikor a megadott változóhoz érünk megpróbálunk egy másik kiértékeletlen változót választani a kózhoz. Ha ez nem megy csak akkor backtrackelünk.
A backtracknél nem nyúlunk a watch listekhez!
Tutorial: https://sahandsaba.com/understanding-sat-by-implementing-a-simple-sat-solver-in-python.html
Elkódolva: [[1,2,-3],[-1,4]]
class SATfeladat():
def __init__(self):
self.variables = []
self.clauses = []
def add_clause(self,clau):
if clau not in self.clauses:
self.clauses.append(clau)
self.variables=self.variables+[abs(var) for var in clau if (abs(var) not in self.variables)]
def add_clauses(self,claus):
for c in claus:
self.add_clause(c)
s=SATfeladat()
s.add_clause([1,2])
s.add_clause([-2,3])
s.add_clauses([[-3,4],[4,5]])
print("Klózok: ",s.clauses)
print("Változók:", s.variables)
Milyen adatszerkezetet használjunk?
def setup_watchlist(instance):
watchlist = {literal:[] for literal in list(instance.variables)+[-x for x in instance.variables]}
for clause in instance.clauses:
# A klóz az első literálját figyeli
watchlist[clause[0]].append(clause)
return watchlist
s=SATfeladat()
s.add_clause([1,2,])
s.add_clause([-2,3])
s.add_clauses([[-3,4],[-3,4,5]])
print("Klózok:",s.clauses)
wl=setup_watchlist(s)
print("Watch listek:",wl)
def update_watchlist(instance,
watchlist,
false_literal,
assignment,
verbose):
"""
A watch listek frissítése miután 'false_literal'-hoz hozzárendeltünk hamis értéket.
Hamissal tér vissza ha a frissítés nem lehetséges, azaz az aktuális hozzárendelés ellentmondásra vezet.
"""
while watchlist[false_literal]:
clause = watchlist[false_literal][0]
found_alternative = False
for alternative in clause:
v = abs(alternative)
a = alternative>0
if assignment[v] is None or assignment[v] == a:
found_alternative = True
del watchlist[false_literal][0]
watchlist[alternative].append(clause)
break
if not found_alternative:
if verbose:
print('Aktuális hozzárendelés: {}'.format(assigment))
print('A {} klóz ellentmondásra vezetett.'.format(clause))
return False
return True
s=SATfeladat()
s.add_clause([1,2])
s.add_clause([2,3])
s.add_clauses([[-3,4]])
print(s.clauses)
print(s.variables)
wl=setup_watchlist(s)
print(wl)
assigment={x:None for x in s.variables}
assigment[1]=False
update_watchlist(s,wl,1,assigment,True)
assigment[2]=False
update_watchlist(s,wl,2,assigment,True)
print('asd',wl)
def solve(instance, watchlist, assignment, d, verbose):
"""
Rekurzívan megoldjuk a SAT feladatot a d. változótól kezdve, feltéve, hogy a az első d változónak már van éréke.
Egy generátor objektummal térünk vissza, ami felsorolja a megoldásokat.
"""
if d == len(instance.variables):
yield assignment
return
for a in [False, True]:
if verbose:
print('Próba {} = {} '.format(instance.variables[d], a))
assignment[instance.variables[d]] = a
if update_watchlist(instance,
watchlist,
instance.variables[d]*((-1)**(int(a))),
assignment,
verbose):
for a in solve(instance, watchlist, assignment, d + 1, verbose):
yield a
assignment[instance.variables[d]] = None
s=SATfeladat()
s.add_clause([1])
s.add_clause([-2,3])
s.add_clauses([[-3]])
print(s.clauses)
print(s.variables)
wl=setup_watchlist(s)
print(wl)
assigment={x:None for x in s.variables}
sols=solve(s,wl,assigment,0,True)
for x in sols:
print("Megoldás:",x)
A program futása közben új klózokat hozunk létre, melyek a korábbiakból következnek.
Ha $(A\lor B\lor C)$ és $(\neg C\lor D\lor \neg E)$ akkor $(A\lor B\lor D\lor \neg E)$.
Futás előtt és időnként közben kicsit átalakítjuk a formulát.
Ha túl sok új klózt tanulunk meg, akkor lelassul minden. Ezért néha töröljünk. De mi alapján válasszuk a törlendőt?
A változók kiértékelésének sorrendje is erősen számít. Egy lehetséges stratégia:
Minden változóhoz fenttartunk egy pontszámot, ami kezdetben 0. Ha a rekurzió során ellentmondásba futunk, akkor az ellentmondásban részt vevő változók pontszámát növeljük valamilyen $C_1$ konstanssal. Minden k darab konfliktus után minden változó pontszámát megszorozzuk egy $C_2$ konstanssal.
Időnként újraindítjuk az egész futást, de megtartva bizonyos információkat, például a megtanult klózokat. Azt is megjegyezzük, hogy utoljára kihez mi volt rendelve és azzal próbálkozunk majd először az új futás során.
Az újraindításokra is sok stratégia létezik, mostánban az agresszív újraindítgatást szokták preferálni.
Fontos, hogy bár a sat solvereken sokat lehet gyorsítani, de azért az alapvető sebesség problémát nem tudjuk kikerülni. Egy nem triviális formula pár száz változóval is megoldhatatlan lehet a mai solverekkel.
Lehetséges a pozitív természetes számokat két csoporta osztani úgy, hogy egyik csoport sem tartalmazzon olyan $(a, b, c)$ hármast, amire $a^2+b^2=c^2$.
Válasz: nem lehetséges! 1-től 7825-ig már nem megoldható.
Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek 2016
800 mag és 2 nap, 200 terabyteos bizonyítás.
Hogyan hozzunk létre olyan kulcsokat és ajtókat, hogy minden kulcs csak megadott ajtókat tudjon kinyitni?
Egy python csomag, melyel hatékony, nem pythonban írt SAT solvereket lehet meghívni. Pl:
from pysat.solvers import Glucose3
ssolver = Glucose3()
ssolver.add_clause([1,2,-3])
ssolver.add_clause([1,2])
ssolver.add_clause([-2,-3])
ssolver.add_clause([2])
ssolver.solve()
ans=ssolver.get_model()
ssolver.delete()
print(ans)