http://www.lambda.ee/w/index.php?action=history&feed=atom&title=Prax_2%3A_lihtsa_DPLL_lahendaja_realiseerimine 2026-11-03T08:00:38Z Selle lehekülje redigeerimiste ajalugu MediaWiki 1.43.11 http://www.lambda.ee/w/index.php?title=Prax_2:_lihtsa_DPLL_lahendaja_realiseerimine&diff=12299&oldid=prev 2015-03-12T12:40:46Z

<p></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="et"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">←Vanem redaktsioon</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Redaktsioon: 12. märts 2015, kell 14:40</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l30">30. rida:</td> <td colspan="2" class="diff-lineno">30. rida:</td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* disjunktidel on küljes counterid seni määramata positiivsete ja määramata negatiivsete literaalide kohta</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* disjunktidel on küljes counterid seni määramata positiivsete ja määramata negatiivsete literaalide kohta</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>Kui tahad teha eriti vinget tõestajat (ei ole kohustuslik), tasub tutvuda Eugene Goldbergi loengutega [http://eigold.tripod.com/presentations/Lecture1.zip loeng1], [http://eigold.tripod.com/presentations/Lecture1.zip loeng2],[http://eigold.tripod.com/presentations/Lecture1.zip loeng3] ja/või googeldada ja otsida zChaffi ja SATO kohta artikleid.</div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>Kui tahad teha eriti vinget tõestajat (ei ole kohustuslik), tasub tutvuda<ins style="font-weight: bold; text-decoration: none;">:</ins></div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div> </div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">* eriti soovitav: http://minisat.se/Papers.html</ins></div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">* </ins>Eugene Goldbergi loengutega [http://eigold.tripod.com/presentations/Lecture1.zip loeng1], [http://eigold.tripod.com/presentations/Lecture1.zip loeng2],[http://eigold.tripod.com/presentations/Lecture1.zip loeng3]  </div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">* </ins>ja/või googeldada ja otsida zChaffi ja SATO <ins style="font-weight: bold; text-decoration: none;">jne </ins>kohta artikleid.</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Valmis saadud lahendajaga tuleks veidi eksperimenteerida:</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Valmis saadud lahendajaga tuleks veidi eksperimenteerida:</div></td></tr> <!-- diff cache key lambdadb:diff:1.41:old-10014:rev-12299:php=table --> </table>

Tammet http://www.lambda.ee/w/index.php?title=Prax_2:_lihtsa_DPLL_lahendaja_realiseerimine&diff=10014&oldid=prev 2013-02-14T17:20:45Z

<p></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="et"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">←Vanem redaktsioon</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Redaktsioon: 14. veebruar 2013, kell 19:20</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l30">30. rida:</td> <td colspan="2" class="diff-lineno">30. rida:</td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* disjunktidel on küljes counterid seni määramata positiivsete ja määramata negatiivsete literaalide kohta</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* disjunktidel on küljes counterid seni määramata positiivsete ja määramata negatiivsete literaalide kohta</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <tr><td class="diff-marker" data-marker="−"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>Kui tahad teha eriti vinget tõestajat, tasub tutvuda Eugene Goldbergi loengutega [http://eigold.tripod.com/presentations/Lecture1.zip loeng1], [http://eigold.tripod.com/presentations/Lecture1.zip loeng2],[http://eigold.tripod.com/presentations/Lecture1.zip loeng3] ja/või googeldada ja otsida zChaffi ja SATO kohta artikleid.</div></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>Kui tahad teha eriti vinget tõestajat <ins style="font-weight: bold; text-decoration: none;">(ei ole kohustuslik)</ins>, tasub tutvuda Eugene Goldbergi loengutega [http://eigold.tripod.com/presentations/Lecture1.zip loeng1], [http://eigold.tripod.com/presentations/Lecture1.zip loeng2],[http://eigold.tripod.com/presentations/Lecture1.zip loeng3] ja/või googeldada ja otsida zChaffi ja SATO kohta artikleid.</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Valmis saadud lahendajaga tuleks veidi eksperimenteerida:</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Valmis saadud lahendajaga tuleks veidi eksperimenteerida:</div></td></tr> <!-- diff cache key lambdadb:diff:1.41:old-10013:rev-10014:php=table --> </table>

Tammet http://www.lambda.ee/w/index.php?title=Prax_2:_lihtsa_DPLL_lahendaja_realiseerimine&diff=10013&oldid=prev 2013-02-14T17:20:29Z

<p></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="et"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">←Vanem redaktsioon</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Redaktsioon: 14. veebruar 2013, kell 19:20</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l29">29. rida:</td> <td colspan="2" class="diff-lineno">29. rida:</td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* muutujatel on küljes pointerite massiivid disjunktidele, kus ta esineb (eraldi negatiivsete ja positiivsete jaoks)</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* muutujatel on küljes pointerite massiivid disjunktidele, kus ta esineb (eraldi negatiivsete ja positiivsete jaoks)</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* disjunktidel on küljes counterid seni määramata positiivsete ja määramata negatiivsete literaalide kohta</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* disjunktidel on küljes counterid seni määramata positiivsete ja määramata negatiivsete literaalide kohta</div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"></ins></div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">Kui tahad teha eriti vinget tõestajat, tasub tutvuda Eugene Goldbergi loengutega [http://eigold.tripod.com/presentations/Lecture1.zip loeng1], [http://eigold.tripod.com/presentations/Lecture1.zip loeng2],[http://eigold.tripod.com/presentations/Lecture1.zip loeng3] ja/või googeldada ja otsida zChaffi ja SATO kohta artikleid.</ins></div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><br></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Valmis saadud lahendajaga tuleks veidi eksperimenteerida:</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Valmis saadud lahendajaga tuleks veidi eksperimenteerida:</div></td></tr> <!-- diff cache key lambdadb:diff:1.41:old-10005:rev-10013:php=table --> </table>

Tammet http://www.lambda.ee/w/index.php?title=Prax_2:_lihtsa_DPLL_lahendaja_realiseerimine&diff=10005&oldid=prev 2013-02-14T16:54:13Z

<p></p> <table style="background-color: #fff; color: #202122;" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="et"> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">←Vanem redaktsioon</td> <td colspan="2" style="background-color: #fff; color: #202122; text-align: center;">Redaktsioon: 14. veebruar 2013, kell 18:54</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l29">29. rida:</td> <td colspan="2" class="diff-lineno">29. rida:</td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* muutujatel on küljes pointerite massiivid disjunktidele, kus ta esineb (eraldi negatiivsete ja positiivsete jaoks)</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* muutujatel on küljes pointerite massiivid disjunktidele, kus ta esineb (eraldi negatiivsete ja positiivsete jaoks)</div></td></tr> <tr><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* disjunktidel on küljes counterid seni määramata positiivsete ja määramata negatiivsete literaalide kohta</div></td><td class="diff-marker"></td><td style="background-color: #f8f9fa; color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* disjunktidel on küljes counterid seni määramata positiivsete ja määramata negatiivsete literaalide kohta</div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"></ins></div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">Valmis saadud lahendajaga tuleks veidi eksperimenteerida:</ins></div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"></ins></div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">* loomulikult katsetada lihtsatel näidetel, et kas käib õieti</ins></div></td></tr> <tr><td colspan="2" class="diff-side-deleted"></td><td class="diff-marker" data-marker="+"></td><td style="color: #202122; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">* katsetada keerukamate näidete peal, et millistega veel hakkama saab ntx 5 sek vältel ja millistega mitte</ins></div></td></tr> <!-- diff cache key lambdadb:diff:1.41:old-10004:rev-10005:php=table --> </table>

Tammet http://www.lambda.ee/w/index.php?title=Prax_2:_lihtsa_DPLL_lahendaja_realiseerimine&diff=10004&oldid=prev 2013-02-14T16:53:02Z

<p>Uus lehekülg: &#039; Ülesande sisuks on lihtsa DPLL lahendaja realiseerimine nullist. Sisendiks oleks lahendajal triviaalses DIMACS formaadis CNF (conjunctive normal form ehk disjunktsioonide konj...&#039;</p> <p><b>Uus lehekülg</b></p><div><br /> Ülesande sisuks on lihtsa DPLL lahendaja realiseerimine nullist.<br /> <br /> Sisendiks oleks lahendajal triviaalses DIMACS formaadis CNF (conjunctive normal form ehk disjunktsioonide konjunktsioon) fail, näiteks:<br /> <br /> &lt;pre&gt;<br /> c Example CNF format file<br /> c<br /> p cnf 4 3<br /> 1 3 -4 0<br /> 4 0 2<br /> -3<br /> &lt;/pre&gt;<br /> <br /> Näiteid ja lisajuttu leiad: http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html<br /> <br /> Sinu programm peaks töötama lihtsalt käsurealt, võtma faili sisse, andma välja tulemuse ja soovitavalt veidi statistikat.<br /> <br /> Tehnoloogia on vaba. Hea mõte on kasutada mõnda kiiremat, kompileeritud keelt a la C, C++, Java, C#.<br /> <br /> Lahendaja peaks kindlasti sisaldama:<br /> <br /> * unit clausede propageerijat (ühikresolutsiooni tegemine)<br /> * rekursiivset splittijat (dpll põhiidee)<br /> <br /> Mõistlik oleks realiseerida lahendaja nii, et ta ei genereeri füüsiliselt uusi disjunkte, vaid<br /> <br /> * muutujate teadaolevad väärtused on integer massiivis<br /> * muutujatel on küljes pointerite massiivid disjunktidele, kus ta esineb (eraldi negatiivsete ja positiivsete jaoks)<br /> * disjunktidel on küljes counterid seni määramata positiivsete ja määramata negatiivsete literaalide kohta</div>

Tammet