search

strnisaj / LVR-sat

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

DPLL #3

Closed gvesna closed 10 years ago

strnisaj commented 10 years ago

Oj A je vama kej ratal naprogramirat?

gvesna commented 10 years ago

Hej. Rok se je vceri lotu tega, js se bom pa cez vikend.

strnisaj commented 10 years ago

Jest zdej tut nism šure, če mi prou dela. Men vrne za 9x9 sudoku valuiranih 270 spremenljivk in nevaluiranih 459 spremenljivk. Mau se mi zdi vseen sumljivo, da teb vrne sam 56 spremenljivk nevaluiranih. Vseh spremenljivk je namreč 9^3 = 729. Da bi jih blo 673 čistih, se mi zdi mau težko.

roksokol commented 10 years ago

56 je blo za naš mini testni primer 'a'. Za testni primer 'b' mi vrne 699 nevaluiranih in 30 čistih. Se skupaj tud men sešteje v 729. Hm. Da mi ugotovi te stvari traja tudi 80 sekund, kar se mi zdi čisto preveč (to je pred 'ugibanjem' vrednosti ostalih spremenljivk). Tebi?

strnisaj commented 10 years ago

Men Traja okol 40s. Sam ne vem zakaj dobiva različno. Pomoje bi se mogl dobit.

strnisaj commented 10 years ago

jest nč ne bruteforcam, k nism poj naprej programirou. Ena ideja je, da ko nastavš eno spremenljivko na True (rečva ji X) ti bodo vsi stavki k so oblike (notX or Y) al pa (noX or noY) razpadl na enojčke Y al pa notY. Poj lahko spet poženeš poenostavitev, k ti bo vse enojčke spet odstranl, pa boš meu ful mn za pregledvt. Nevem, če je to kej uporabn. Ko enkrat veš, da je X=True vredu, lahko odstranš vse stavke v katerih se pojavlja X in spet poenostavljaš. lahko ti pošlem moj program, k poenostavlja, sam bruteforce pa jst še nimam.

roksokol commented 10 years ago

Hm, sm mislu, da rabs omenjen cs za resitev... Sm drugac razmislov tud jz na ta nacin, ampak se mi nekak dozdeva, da se lah nahecas....mislm kako pa ves, da je X true? Mislm predstavlam si problem, kjer obstaja pac ena sama resitev. Recimo se, da nimas nobene ciste spremenljivke in nobene "proste". Torej na zacetku ne ves se za nobeno vrednost. Potem gres pa racunat in X nastavis recimo na true in nardis postopek, ki si ga omenil. Nato pa pri ene 25-i spremenljivki ugotovis, da nisi prisel do resitve. Kako zdej ves, katero izmed teh 25-ih je potrebno spremenit? Kaj pa, ce je potrebno 3 spremenit? Ne vem, se mi zdi, da je vsen treba nekak pobruteforceat. No ja, sj to se ve, samo kako najbolj ucinkovito bi se to izpeljal? Pridm jz v petek na vaje in po vajah mam cs do 17h, pa lah kj skp naprogramiramo mogoce? Do tekrt bom pa probov popravt tist moj bug, kj vec pa dvomim, ker mam se eno drugo mrtvo crto do cetrtka...

Sent from my iPhone 5

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

jest nč ne bruteforcam, k nism poj naprej programirou. Ena ideja je, da ko nastavš eno spremenljivko na True (rečva ji X) ti bodo vsi stavki k so oblike (notX or Y) al pa (noX or noY) razpadl na enojčke Y al pa notY. Poj lahko spet poženeš poenostavitev, k ti bo vse enojčke spet odstranl, pa boš meu ful mn za pregledvt. Nevem, če je to kej uporabn. Ko enkrat veš, da je X=True vredu, lahko odstranš vse stavke v katerih se pojavlja X in spet poenostavljaš. lahko ti pošlem moj program, k poenostavlja, sam bruteforce pa jst še nimam.

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

strnisaj commented 10 years ago

Ja sej to. Mogl bi se nekak premislt kako se ti lahko zatakne pa poj vidt, če se da kej nazaj o X povedat. Jst v petk lahko samo pred vajami. Lah se pa vidva z Vesno dobita. Da bo še ona kej nardila.

btw: Čs mamo pa do sobote zdej, k je Bauer na Konferenci, pa bo takt sele gledou kaj je gor. Je napisou na učilnci.