EvaBr / LVRSAT

Sat solver
BSD 3-Clause "New" or "Revised" License
0 stars 1 forks source link

TO DO #8

Closed EvaBr closed 10 years ago

EvaBr commented 10 years ago

Kot dogovorjeno še ena to-do lista:

Grafi so pošlihtani, tako da stvar dela in je dokaj prijazna za :eyes: . kbarvanje sem popravila (ni delalo ker je bila ena izmed formul sam copy paste iz 3COL, pa je začel malo tripat :mushroom: ko je do taj prišel). Lahko malo sprobata zaganjat te grafe, če še odkrijeta kašn bug. Tudi vizualno podobo izpisov spreminjajta po mili volji (ura je 3:09 in jaz imam premalo :coffee: , da bi se mi dalo sploh mislit na izgled...).

Sudoku zdaj dela, vprašanje je izpis in dpll. Ali lahko nekdo od vaju preveri, ali izpis deluje? Meni neke štrajka (ko zaženem resljivostSudoku.py se zgodi en velik nič).

Dpll je ultra počasen. Ideja za pohitritev: glede na to, da v kodi miljonkrat skačemo iz CNF v ne-CNF obliko in nazaj, in vmes še dost poenostavljamo (đizus to dolg trajaaa), bi blo mogoče faj stvar prilaagodit da bo potrebovala cel čas (al pa večino) izvajanja le CNF. Kaj bi bilo za to treba nardit:

Če ostane čas je veliko možnosti za upgrade tudi pri poenostavitvah in cnf obliki, kar pa po dogovoru pustimo zaenkrat pri miru (:see_no_evil: )...

EvaBr commented 10 years ago

Ah ja, še to. V repoz bom pušnila še kopijo dpll-ja, datoteko dpll2.py. Dejmo če se strinjata tam notr brainstormat glede pohitritev dpllja, tisto original verzijo, ki razen tega da je počasnejša od moje prababice načeloma dela, pa pustimo za vsak slučaj zaenkrat na miru.

Lp in ln, :octopus:

EvaBr commented 10 years ago

Evo, zdaj ko nam je ratalo dpll2 napisat tako, da uporablja le CNF obliko, se mi zdi da smo kar pohitril zadevco. (400 spremenljivk: slabe 3min na moji mašini)

Je pa še ena stvar - 'zamenjaj' zdaj deluje na CNF obliki, ampak na tak način, da že sproti mičkeno poenostavlja - če mora vstavit F v Ali ga pač kar izpusti, če more vstavit T v Ali pa spusti kar cel stavek... In izkaže se, da se lahko zgodi, da imaš po enem klicu 'zamenjaj' kakšno novo čisto pojavitev. Kar smo prej mislili, da se ne more zgoditi. Tako da predlagam, da poskusimo še to čisto pojavitev dati magari v novo funkcijo in jo nekako zazankati - da se bo izvedla vsaj po vsake nekaj klicih funkcije 'zamenjaj'. Ker pomoje bi to utegnilo pri klobasastih formulah tudi precej pohitrit zadevšno...

Please elaborate. :)

:octopus:

EvaBr commented 10 years ago

Ha, sproban dpll2 na različno polnih(rešljivih) sudokujih;

Tak da je dokaj okej hiter pomoje :smile:

Zdej je potemtakem treba urediti samo še preverjanje sudokujev. Jaz bom pa zdle zamenjala importanje dpllja z dpll2-jem. A ruknemo staro verzijo dpll dol, ali pustimo kar obe gor?

Ln, :octopus:

Teja91 commented 10 years ago

Em, a je bilo kaj sprememb od takrat pušanih? Meni trenutno dpll sploh noče delat. Iščem napako za to in za prazen sudoku. Btw, jaz bi zbrisala staro verzijo, da ne bo nepotrebne zmede. Itak če se odločaš med dvema delujočima verzijama izbereš tahitrejšo, al kaj :))

:bee:

Teja91 commented 10 years ago

Aja, my mistake, nisem opazila da moraš zdaj formulo sam vrečt v cnf obliko. :)

EvaBr commented 10 years ago

Ok, dpll2 zbrisan, glavni algoritem je zaj v dpll.py. Pohitren kolker gre, informativno dodani še implementaciji z manj čistimi pojavitvami in primerjava vseh treh. Grafi so OK, izpis preverjanja sudokuja je narejen (sudokuji), manjka še preverjanje s človeku prijaznejšim zapisom (preverjanje s pomočjo datot. resljivostSudoku).

Če se komu da, se lahko malo ukvarjamo tudi še z metodo poenostavi teh prevedbo na CNF. Oboje kar traja, pa tudi ni popolnoma bug free; oziroma ne vrne najlepše/popolnoma končne, dokončno poenostavljene formule... Or so it seems. Lp, :octopus:

EvaBr commented 10 years ago

Popravljen bug v metodi cnf pri razredih Ali ter In. Tudi poenostavi pošlihtan, manjka le distributivnost, ki pa tudi ni nujna; za šolske razmere stvar (dpll in cnf) pomoje deluje čist fajn hitro. Poenostavi pa že zdaj dela tako počasi, da bi potem morda uspeli še podaljšat čas dpll-ja. Tako da tudi ne škodi, če pustimo kar kot je.

resljivostSudoku sicer ni nujna, ker eno dokaj v redu preverjanje že imamo, lahko po se vseeno še izprsimo, če se komu da... :grin:

Kmalu bo urejen tudi Hadamard, tako da lahko potlej spišemo še preverjanje zanj...

Lp, :octopus:

BaumanB commented 10 years ago

Resljivost je porihtana. Problem je bil v praznih vrsticah med posameznimi sudokuji (vrgo je exception, zato ni nič izpisal), pa še izpis ni bil glih ok. Zdaj dela pač tak preveri samo za en sudoku, ki si ga pač lažje predstavljaš ko je tak "narisan" v txt fajlu kot pa če gledaš seznam trojic.

Lp, :beer:

EvaBr commented 10 years ago

Zakaj si pa to predelal? :O Sej sem jaz še včeraj pa predvčerajšnjem pushala gor stvari, in je bil porihtan že, vse je delal. Mislim, za vse tri sudokuje; je vse prebral pa prav nardil.

EvaBr commented 10 years ago

Ok; po dogovoru bomo obnovili stare verzije. Potem pa je vse pošlihtan. Tako da zapiram išju. :)

We ROCK! :metal: :octopus: