EvaBr / LVRSAT

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

dpll in kok in everything else #3

Closed EvaBr closed 10 years ago

EvaBr commented 10 years ago

Ok, najprej, a čmo tut za koka :chicken: datoteke dat na GeekHub?

Pol, treba je ločit datoteke - iz cnf-ja pobrat kar je odveč, pa naredit posebej en fajl za naloge (a la sudoku, Hadamard, itn). Lah tut za vsako nalogo posebej, kaj bo boljše?

Ko se to zrihta, se bo treba posvetit še pisanju oz. preverbi rešitev za vsakega izmed teh nalog; ampak če sem prav razumela, je za oceno (oziroma s kvazi deadline-om) samo dpll. Tako da bi se mogoče lahko najprej tega lotili, pa pol za posladek še nalogce rešl... Agreed?

Kar se dpllja tiče pa se bo rabilo kar nekaj zadev še... Za osnovno delovanje najprej rabimo funkcijo "zamenjaj(F, object, slovar[object])", ki v formuli F zamenja vsako pojavitev spremenljivke object z njeno vrednostjo slovar[object]. Zdej, zaenkrat sem mislila, da bi bila formula F podana kar v navadni obliki (torej ne CNF), ker je to glede na trenutno kodo bolj uporabno. Imata kako idejo kako bi se lahko to funkcijo realiziralo? Pa tudi, če bi jo bilo morda lažje spisati, ako bi bila F podana v CNF obliki (in če, zakaj)?

Ko bomo imeli to f-jo "zamenjaj", bo treba mičkeno priredit napisano (glej komentarje v trenutnem dpll-ju), pa bo stvar že ready za prvo testiranje in popravke po potrebi (predvsem izpis ustreznega slovarja bi utegnil zajebavat, ampak da bomo videli, če res, rabimo najprej "zamenjaj"...).

Ko bo pa to narejeno... bi se pa lotila še kakih dodatkov, ala čista pojavitev, itd. Lahko se pa tega kateri že tudi zdaj loti - kako mislita, da bi bilo bolje? In pa seveda nas potem čaka zasluženi :beer: ( oz. :beers: ) !

Se opravičujem, da sem se preveč razpisala xD Vsak komentar dobrodošel. Kdo se javi za kter del?

P.S. Ker mi je Teja prijazno pinpointala da ne morem bit :octocat: , ker je to GHjev znak, sem po novem :octopus: ^^

Teja91 commented 10 years ago

Draga :octopus: , O tem sem razmišljala in moje mnenje je, da ima kar vsaka naloga svoj fajl. Se mi zdi bolj pregledno in lepše. Je pa res, to bo sam češnjica na smetani, zaenkrat treba dpll nardit :D Lahko se recimo javim za čisto pojavitev, pa se malo igram, če je to vsem udeležencem ok. :D Si bomo postavli kak deadline, do kdaj bi naš dpll naj deloval? Da se pol nardijo še nalogice. In da ne bom (vsaj jaz) prelagala zadeve na zadnjih nekaj dni, ker to se ne res ne spodobi :P

p.s. pomojem :octopus: piše tak dolge komentarje sam da lahko uporabi čim več smajlijev. :trollface:

EvaBr commented 10 years ago

Ha Ha! A TT bo pa kar :trollface: ?? xD Pa to ni res, :octopus: piše tak dolge komentarje sam zato ker je cela dva dni skos neka programirala namesto da bi se za ponedeljkov kolokvij učila xD in ima VELIIIIKO za povedat :D In ji je dolgcajt :D

EvaBr commented 10 years ago

Aja pa, js bi bl rekla da TT = :bee: ! :smile:

EvaBr commented 10 years ago

A je že kir sprobal dpll? ali pa spremenjen cnf? Ker se ne spomnim, kaj je že bilo pri cnf-ju, da je mogu BB tist seznam argumentov v args dat, in me zato skrbi, kaj utegne iti narobe, ker sem jaz to nazaj spremenila... Any thoughts?

Teja91 commented 10 years ago

Okaay, ppl. Sem dodala preverjanje dpll-ja v testne primerčiče in je še dokaj.. okoren :D Trenutno deluje:

:bee:

EvaBr commented 10 years ago

Pop popravljen, dpll deluje, (tut poenostavi() zgleda okej, sam ga je treba še naredit do konca, kar manjka...), dvojni x v CNF-ju še niso odpravljeni, ampak se nekak strinjamo, da zaenkrat sploh ni potrebe, da se tega lotimo. Ergo: funkcije spisane, vse načeloma deluje, zapiram temo.

:octopus: