DPLL + Sudoku

[roksokol]

Ne vem zakaj je tema zaprta, ker nam še vedno ne dela pravilno. Skratka, po celem dnevu debugginga sem ugotovil, da problem vseeno ne tiči v DPLL algoritmu.

Zakaj tako mislim, bom razložil kar s primerom. Recimo, da imamo izjavo: i = (~X) and (~X or Z or ~Y) and (X or Z) and (~Z or Y) and (Q or ~A)

Prva stvar, ki jo DPLL naredi je to, da tiste podizjave, ki so sestavljene iz enega elementa nastavijo na True/False skladno s tem, da bo podizjava True. To se ponavlja, dokler ni nobene podizjave dolžine 1. Zgornji primer bi se naredil takole:

vals = { X::False } i = (Z) and (~Z or Y) and (Q or ~A)

vals = { X::False ; Z::True } i = (Y) and (Q or ~A)

vals = { X::False ; Z::True ; Y::True } i = (Q or ~A)

Šele po zgornjem postopku grem iskat čiste spremenljivke. V tem primeru najde čist spremenljivi Q in ~A, valuacije pa se razširijo: vals = { X::False ; Z::True ; Y::True ; Q::True ; A::False}

izjava je sedaj prazen AND, kar pomeni, da smo prišli do rešitve. Seveda je pri problemu sudoko izjava daljša in praviloma ostanejo še spremenljivke z neznano vrednostjo. Skratka, zgornja obdelava izjave pred klicem rekurzivnega dela DPLLja se mi zdi smiselna in pravilna. Če je temu tako, potem algoritem DPLL deluje pravilno in je težava v izjavi, ki jo prejmem. Problem nastopi, ko odstranjujem podizjave dolžine 1 (torej pred iskanjem čistih spremenljivk in ugibanja vrednosti neznank). Stvar je v tem, da pride do protislovja med vrednostmi.

Če je moj postopek napačen, naj mi prosim nekdo pove zakaj. Na mojih testnih primerih (kjer sem opazoval tudi delovanje na vsakem koraku), vse deluje brezhibno.

[roksokol]

PS: če izklopim odstranjevanje podizjav dolžine 1, potem mi ne najde nobene čiste spremenljivke. Če odstranjevanje opravim samo enkrat pa dobim toliko prostih spremenljivk, kot jih dobi Jernej. Vseeno mislim, da bi moral zgoraj opisan postopek delovati.

Testiranje je potekalo na izjava = sudoku([[1,2,0,0],[3,0,1,0],[0,1,0,3],[0,0,2,1]]) in tudi na tistem daljšem 9x9. Za oba dobim rešitev False, kar ni pravilno. Se pa pri obeh zatakne pri zgoraj opisanem problemu.

BTW, tudi če izjave dolžine 1 odstranim samo enkrat, se v vsakem primeru vrne False v rekurziji, ker pride do protislovja.

[strnisaj]

Torej pravš, da more v izjavi sudoku nekje pridt do X and ... and ~X?

[strnisaj]

Men se zdi, da če jest lahko sproduciram valuacijo, v kateri bo sudoku izjava True, in je to prou tista valuacija k reš sudoku poj ne more bit z izjavo nč narobe. Tvoj postopk reduciranja je čist vredu. Če ti pa brute force poj vrne protislovje, poj se more pa tm en problem skrivat.

[roksokol]

Posredno pride do tega ja. Bolj natančno, pride takole: (~X or Z) and (X or Z) and (~Z). Kot sem že napisal, do rekurzije sploh ne pridem, ker se že v samem začetku vrne False zaradi protislovja.

[roksokol]

BTW: sem si potegnil dol današnjo verzijo Izjave.py in je že takoj error: TabError: inconsistent use of tabs and spaces in indentation

Sej je čist očitno, kje je error, samo skrbi me, da se sploh ne proba, če stvar deluje, pred objavo. Kako naj potem verjamem, da ostale stvari delujejo? Ker sem namreč tudi trdno prepričan, da ni težava v DPLLju......

def test(): a = Var('A') b = Var('B') c = Var('C') iz = Not(And([Or([Not(a),b]),Not(And([c,a])),Not(Or([Not(b),a,Not(c)]))])) iz1 = And([a,And([c,b]),Or([Not(a),Not(c)])]) print('Poenostavitev izjave: ') t0 = time.clock() i = iz.poenostavi() print('Pretekel cas: ', time.clock() - t0) print('Poenostavljena izjava: ', i) print('###############################')

print('Vrednost izjave: ')
val = {'A':False,'B':True,'C':True}
val1 = {'A':True,'B':True}
t0 = time.clock()
j = iz.izracun(val)
print('Pretekel cas: ', time.clock() - t0)
print('Vrednost: ', j)
print('###############################')

print('Nastopajoce spremenljivke: ', iz.var())

[roksokol]

Ne izpiše zamikov lepo....ok, vidim sedaj, da si jih popravil pred 15 minutami

[roksokol]

File "C:\Users\Roxon\workspace\Python\SAT\Sudoku.py", line 27, in sudoku x = Izjave.Var('X({0},{1},{2})'.format(i,j,k)) NameError: name 'Izjave' is not defined

Tudi tole je neumen error (kdorkoli ga je že ustvaril...)

[strnisaj]

A mas tazadno verzijo. Ker nej bi Vesna popravla, da ne piše Izjave.Var ampak sam Var.

[roksokol]

Mam tisto izpred cca. 23 min. Sem sam popravil, samo ne razumem, da se objavljajo stvari, ki sploh ne delujejo.....

[strnisaj]

Jest grem spat. Se beremo jutr. Cawc.

[roksokol]

Še ena cvetka se je pojavila: File "C:\Users\Roxon\workspace\Python\SAT\Sudoku.py", line 100, in testS print(CNF.CNF(b)) AttributeError: 'function' object has no attribute 'CNF'

[strnisaj]

Ej a si preizkusu svoj DPLL na 2x2 hadamardu? Men en error vn vrže:

Traceback (most recent call last): File "<pyshell#2>", line 1, in DPLL(a) File "C:\Users\Jernej\Desktop\Python\DPLL_r.py", line 29, in DPLL solution = rec_DPLL(izjava, varValues) # Klic rekurzivne metode File "C:\Users\Jernej\Desktop\Python\DPLL_r.py", line 53, in rec_DPLL pureVals = getPureVals(izjava) # pridobim slovar čistih spremenljivk File "C:\Users\Jernej\Desktop\Python\DPLL_r.py", line 196, in getPureVals if (var.vrni() in varsInStatement) == False: TypeError: unhashable type: 'list'

Res je, da nimam še čist tazadne verzije tvoje. K si reku, da si neki pohitriu.

[gvesna]

Jernej, uploadana je nova verzija, a lahku s tistim sprobas? in zdej je datoteka DPLL in ne vec DPLL_r :) verjetno bi ta znala bols delat. js trenutno ne morm sprobat.

[roksokol]

Sem sedaj probal hadamarda. Res ne dela. Ne dela pa zaradi tega, ker je CNF(h) drugačne oblike, kot sem pričakoval, da bodo CNFji. Zalomi se tukaj: ((X(0,0,1) or X(0,0,-1)) and (X(0,1,1) or X(0,1,-1)) and (X(1,0,1) or X(1,0,-1)) and (X(1,1,1) or X(1,1,-1)) and (((((X(0,1,1) or X(0,1,-1) ...... Tisti številni oklepaji privedejo do tega, da se izjava ne spravi pravilno v 2D-list in zaradi tega pride do errorja. Sem razmišljal, da se tudi pri sudoku zgodi nekaj podobnega (da verjetno kje manjka kakšen oklepaj?). Sem predvideval, da bo CNF vrnil tako, kot smo imeli na predavanjih in sicer: ( (...or ....or ...) ... and .... ( ... or ... or ... ) .... and ... ( ... or ....) ). V čem je fora, da ne dobim take vhodne izjave?

[roksokol]

No, mogoče pa ni CNF razlog. Že pred CNFjem je sumljivo število oklepajev:

(((X(0,0,1) or X(0,0,-1)) and (X(0,1,1) or X(0,1,-1)) and (X(1,0,1) or X(1,0,-1)) and (X(1,1,1) or X(1,1,-1))) and (((((X(0,1,1) and X(1,1,1)) or (X(0,1,-1) and X(1,1,-1))) and not((X(0,0,1) and X(1,0,1)) or (X(0,0,-1) and X(1,0,-1)))) or (not((X(0,1,1) and X(1,1,1)) or (X(0,1,-1) and X(1,1,-1))) and ((X(0,0,1) and X(1,0,1)) or (X(0,0,-1) and X(1,0,-1)))))))

To je za primer: izjava = hadamard([[1,1],[-1,1]])

[strnisaj]

Ko daš v CNF morš še poenostavt. Poj pa dela DPLL na hadamartu.

[roksokol]

Saj kličem poenostavi. Spodnji dve vrstici sta zaporedni. izjava = CNF(izjava) izjava = izjava.poenostavi().vrni()

[strnisaj]

A ti, po tem ko daš izjavo v CNF in jo potem še poenostaviš, ne dela DPLL?

[strnisaj]

CNF res vrne v taki čudni obliki. Te številni oklepaji so zato, k je v bistvu izjava ((X(0,0,1) or X(0,0,-1)) zaprta v še en And. Poenostavi funkcija jih pomeče vn, tko da maš poj res obliko ( (...or ....or ...) ... and .... ( ... or ... or ... ) .... and ... ( ... or ....) ). Tko bi mogl delat. Jst zdele nism pr svojmu kompu, tko da ne morm sprobavat. Bom sprobou, k pridem dam.

[roksokol]

Ne na hadamardovem primeru. Očitno. DPLL je zasnovan tako, da naj bi prejel kakršnokoli izjavo. Nato pokliče CNF in nato poenostavi, da se znebim atomov oblike notnotnotnotX. In na tem se kliče funkcija vrni, ki naj bi (vsaj tako sem bil prepričan) morala vrniti izjavo oblike [ ... (...) .... ], kjer [ ] predstavlja zunanji AND in ( ) predstavlja notranje OR stavke. Če je izjava=CNF(izjava).poenostavi().vrni() vedno drugačne oblike od primera do primera, potem algoritem ne bo pravilno deloval ali pa sploh ne bo deloval.

[strnisaj]

Dj probi klicat: izjava = hadamard([[1,1],[1,-1]]) izjava = CNF(izjava).poenostavi() DPLL(izjava)

Men tko reš. Očitno je blo treba dvakrat poenostavt. Sej to ni vredu ampak vidmo, da ta poenostavi ne dela dobr. Ga bo treba popravt. Al pa, če res v CNF vedno sprot poenostavljaš.

[roksokol]

Nope, neki ne dela. Če kličem izjava=CNF(izjava).poenostavi() je čisto na koncu takele oblike: or X(1,0,1) or X(1,0,-1))))). Če še dvakrat (torej trikrat) poenostavim, potem dobim or X(1,0,1) or X(1,0,-1))) kar je ok. Zgleda da vsak poenostavi() klic odpravi en oklepaj :) V tem primeru, mi reši problem pravilno.

Ampak pri izjava=hadamard([[1,1,1,1],[-1,1,-1,1],[-1,-1,1,1],[1,-1,-1,-1]]) pa ponovno ne deluje, ker je kljub trikratnemu poenostavljanju na koncu takole: or (X(2,0,-1) and X(3,0,-1))))))))))

Žal tudi sudoku ne deluje :(

[roksokol]

Da ne bo pomote....sudoku vrne pravilno obliko izjave za dpll, predvidevam pa, da se tko poenostav, da kakšna stvar pade izven OR-a. To ni nujno res, ampak glede na to, da ti lahko rešiš, meni pa ne gre čez odstranjevanje samostojnih spremenljivk.

[strnisaj]

Bom probou poenostavi() popravt, tko da gre v globino, kokr se da. A bi se v petk dobil pred predavanji?

[roksokol]

Jz lahko pridem ja, kdaj si mel pa v mislih? Ce je opcija, bi rajs, da se po predavanjih/vajah dela, ker mam itak ob petih naprej vaje in sm frej vmes. Itak bom pa ze tko 9 ur na faksu in ne bi bil dlje, ce imata seveda cas tud vidva.

Sent from my iPhone 5

On 15 May 2014, at 00:15, strnisaj notifications@github.com wrote:

Bom probou poenostavi() popravt, tko da gre v globino, kokr se da. A bi se v petk dobil pred predavanji?

— Reply to this email directly or view it on GitHub.

[strnisaj]

Ok. Situacija je taka. Jst sm popravu poenostavi() v Izjavah in zdej res odprav vse odvečne oklepaje in zdej DPLL reš hadamarda takoj. Ampak sem ugotovu, da vrne True, tut če mu podaš matriko, k ni hadamardova:

Če je recimo izjava = hadamard([ [1,1], [-1,-1] ]) bo DPLL(izjava) vrnu True, kar je narobe.

V Sudokuju sm dodou funkcijo valuacija(), kjer lahko preverita, da je sudoku izjava pravilna natanko tedaj, ko je sudoku pravilno rešen. Prav tako po predelavi v CNF in poenostavitvi. Jest ne vem več, kaj bi blo lahko narobe z sudoku izjavo. Podobna funkcija valuacija je tut v Hadamardu.

Nekdo more napisat Bauerju, da nam ne dela in da bi se oglasil.

[roksokol]

Sem preveril, kaj bi lahko bilo narobe in je problem dokaj očiten: hadamard([ [1,1], [-1,-1] ]) in hadamard([ [1,1], [-1,1] ]) vrne isto izjavo. Noben člen ni drugačen, pač popolnoma isti sta. Sem si potegnil novi Izjave.py in Hadamard.py.

[roksokol]

Izjava od CNF(sudoku([[1,2,0,0],[3,0,1,0],[0,1,0,3],[0,0,2,1]])).poenostavi().vrni() je pa, če jo greš na roke reševat, res False.

[strnisaj]

Pa res. my bad. funkcija hadamard sploh ne gleda tisteb matrike ampak sam njeno velikost. Vrne pa izjavo, k je true takrt k obstaja hadamardova matrika te velikosti. Bom še to popravu, da ni treba matrike not pisat ampak sam velikost.

Kako si jo pa ti na roke rešvou? Kaj pomen, da je "False"?. A da ne obstaja valuacija, da bi bla True? To se men mau zdi neverjetno. Da je in s sudokujem neki tko narobe in z funkcijo izracun() da vrne true.

[roksokol]

Ja na roke sem jo reševal tako, da sem si na ekran izpisal v vsako vrstico en OR. Pride 408 takih vrstic. Osem OR-ov je dolžine 1, kar sm nastavu na True in sem na ta način dobil še več OR-ov dolžine 1 (ker je 384 ORov dolžine 2, 16 pa jih je dolžine 4). In pol po tretji iteraciji in 15 minut kasneje dobiš X and notX.

False pomeni, da ne izjava ni rešljiva, ja. Če je pa True, ti pa izpiše še pri katerih valuacijah je izjava True.

[roksokol]

Aja, daj probej na tvoji funkciji, ki ti izračuna sudoku pri dani valuaciji dat izjavo CNF(sudoku([[1,2,0,0],[3,0,1,0],[0,1,0,3],[0,0,2,1]])).poenostavi().vrni() . Če ti bo pri tvojih vrednostih vrnilo True, potem bo to zelo čudno :) če pa vrne False, potem pa ena izmed cnf/poenostavi/vrni ne deluje pravilno, i believe. Sicer pa ne vem, kje bi bil bug zaenkrat

[strnisaj]

Dj si poglej funkcijo valuacija() v sudokuju. Na koncu ti izpiše: sud.izracun(val) CNF(sud).izracun(val) CNF(sud).poenostavi().izracun(val)

kjer je sud = sudoku([[1,2,0,0],[3,0,1,0],[0,1,0,3],[0,0,2,1]])) in val valuacija k jo nardim na podlagi rešenga sudokuja [[1,2,3,4],[3,4,1,2],[2,1,4,3],[4,3,2,1]].

Funkcija vrne 3x True. Čer pa kar kol spremeniš v rešenmu sudokuju, potem pa vrne 3x False.

[roksokol]

Ok...a bi primerjala izjavo od sudoka lahk? Ti jo bom kr na mail poslov, ker bi preveč prostora tukile vzel.

S tole kodo si jo izpišem

def printIzjavaNewLine(izjava):

for subIzjava in izjava:
    print(subIzjava)

[strnisaj]

Men vrne v drgačnmu vrestnem redu. Kako pa predlagaš, da primerjam? Tiste spremenljivke, k nastopajo same so iste.

[strnisaj]

Pa neki me mot. če ti nardiš: izjava = sudoku([[1,2,0,0],[3,0,1,0],[0,1,0,3],[0,0,2,1]])) izjava = CNF(izjava).poenostavi().vrni()

in poj

for subIzjava in izjava: print(subIzjava)

Poj ti nebi smel vračat zadeve v [ ] ampak izjave. npr namesto [notX(0,1,1), notX(0,1,4)] bi ti mogl vrnt (notX(0,1,1) or notX(0,1,4)).

To kar si mi ti poslou men izpiše, če napišem:

for subIzjava in izjava: print(subIzjava.vrni())

pa še takrt mi ne vrne npr [X(0,0,1)] ampak X(0,0,1)

[roksokol]

Te oklepaji so nepomembni, sam prej sem klicu funkcijo, ki mi nardi list listov. Izjava je drugac teb resnicna? Kar ce jo na roke resim, je neresnicna.

Sent from my iPhone 5

On 17 May 2014, at 23:37, strnisaj notifications@github.com wrote:

Pa neki me mot. če ti nardiš: izjava = sudoku([[1,2,0,0],[3,0,1,0],[0,1,0,3],[0,0,2,1]])) izjava = CNF(izjava).poenostavi().vrni()

in poj

for subIzjava in izjava: print(subIzjava)

Poj ti nebi smel vračat zadeve v [ ] ampak izjave. npr namesto [notX(0,1,1), notX(0,1,4)] bi ti mogl vrnt (notX(0,1,1) or notX(0,1,4)).

To kar si mi ti poslou men izpiše, če napišem:

for subIzjava in izjava: print(subIzjava.vrni())

pa še takrt mi ne vrne npr [X(0,0,1)] ampak X(0,0,1)

— Reply to this email directly or view it on GitHub.

[strnisaj]

Tko je kot sm prej napisou. Sej lahko sam sprobaš. Bom jo jest probou se na roke narest. Sam ne zdele, k grem spat.

[strnisaj]

Nej ti povem kaj jest delam, ko probam na roke rešt sudoku. Najprej nastavm:

Potem pa ponavljam:

Po nekaj korakih zadnji ukaz vrne True.

Ne vem a prou delam. Prosim poglej, če je vredu ta postopek.

[roksokol]

Ali se kje preveri, da če imaš recimo val [ x ] = True, da ne postane val [ x ] = False? V zgornji kodi tega nikjer ne vidim, razen če v *.izracun() to pocnes? Sicer pa zadnji dve vrstici ne vem, kaj počneta. Zgleda mal sumljiv....

Ampak, kot sem rekel, če jo na roke izračunam, je izjava False, tako da ja, nekaj je narobe.

[roksokol]

In rešit "na roke" sem imel v mislih papir in svinčnik.

[strnisaj]

Predzadnja vrstica preveri, če je kšna izjava pršla False (to se lah zgodi samo, če je izjava oblike X al pa notX) kar bi pomenil, da sem že nekje nastavu spremenljivko narobe, kar pomen, da se zgodi protislovje.

Zadnja vrstica prever, če sm že pospravu vse in so mi ostal sami True. Torej, da je izjava = [True, True,...,True].

Ja če se bo kje pojavu X in notX (pa recimo, da je X prvi v vrsti), potem bo seveda najprej nastavu val[X] na True potem pa ga bo spremenu na False. Samo potem, ko bo šel izračunavat (naslednji korak) bo pa X.izracun() pršou False in bom mel en False v izjavi