• RakeSearch: Ergebnisse des SAT-CMS-Experiments

    In diesen Tagen wurde nicht nur in Zusammenarbeit mit Gerasim@Home ein neues Subprojekt begonnen (vorerst nur mit einer Anwendung für 64-Bit-Windows), sondern auch die Ergebnisse des Ende Juli/Anfang August durchgeführten SAT-CMS-Experiments veröffentlicht:

    Ergebnisse von SAT-CMS
    Als Ergebnis des SAT-CMS-Experiments wurden 29 Paare orthogonaler diagonaler lateinischer Quadrate (engl. orthogonal diagonal Latin squares, ODLS) zehnter Ordnung gefunden. Zwei Zellenzuordnungsschemen (engl. cell mapping schemas, CMS) wurden dafür verwendet. 18 gefundene Paare basieren auf dem ersten CMS, die übrigen elf auf dem zweiten. Ein CMS ist tatsächlich eine Beziehung zwischen zwei lateinischen Quadraten aus einem orthogonalen Paar: für jedes Element des ersten Quadrats zeigt es an, wo dieses Element im zweiten Quadrat zu platzieren ist. Somit kann das zweite Quadrat eines Paares aus dem ersten Quadrat konstruiert werden. Die verwendete Anwendung basiert auf einem konfliktbasierten Algorithmus (CDCL, engl.) zum Lösen des Erfüllbarkeitsproblems der Aussagenlogik (engl. satisfiability problem, SAT). Für jedes untersuchte CMS haben wir zunächst das Problem, Paare (zum CMS passender) ODLS zehnter Ordnung zu finden, auf ein SAT zurückgeführt. Dann wurde das erhaltene SAT in Teilprobleme aufgeteilt, aus denen die WUs erzeugt wurden. Schließlich haben wir aus den gefundenen erfüllenden Zuordnungen (Lösungen des SAT) die entsprechenden ODLS-Paare konstruiert. Alle gefundenen Paare sind hier aufgelistet. Wir sind allen Crunchern, die an diesem Experiment teilgenommen haben, sehr dankbar!
    27.09.2020, 18:30:31 MEZ

    Originaltext:
    Zitat Zitat von https://rake.boincfast.ru/rakesearch/forum_thread.php?id=244
    Results of SAT-CMS
    As a result of the SAT-CMS experiment, 29 pairs of orthogonal diagonal Latin squares (ODLS) of order 10 were found. 2 cell mapping schemas (CMS) were used for this purpose. 18 found pairs are based on the first CMS, the remaining 11 pairs are based on the second one. CMS is in fact a relation between 2 Latin square from an orthogonal pair: for each element of the first square it shows where this element should be placed in the second square. Therefore, one can effectively construct the second square from a pair given the first square. The computing application was based on the CDCL algorithm aimed at solving the Boolean satisfiability problem (SAT). For each studied CMS, we first reduced a problem of finding pairs of ODLS of order 10 (that match the CMS) to SAT. Then, the obtained SAT problem was splitted into subproblems which in turn formed workunits. Finally, from found satisfying assignments (solutions of the SAT problems) we constructed the corresponding pairs of ODLS. All the found pairs are listed here. We are very grateful to all the crunchers who took part in the experiment!
    27 Sep 2020, 17:30:31 UTC
    Ursprünglich wurde dieser Artikel in diesem Thema veröffentlicht: RakeSearch - Erstellt von: taurec Original-Beitrag anzeigen
Single Sign On provided by vBSSO