Dominik

@[email protected]
13 Followers
33 Following
11 Posts
Postdoctoral researcher @KIT_Karlsruhe | #SATSolving, #HPC, #SymbolicAI | 🎸🎹🪕🎤👨‍🍳🎮
KIT pagehttps://ae.iti.kit.edu/schreiber.php
Homepagehttps://dominikschreiber.de
Githubhttps://github.com/domschrei
DominikSep 26, 2024

Kleiner #ScienceSlam im Rahmen des #GI-Dissertationspreises auf der #informatik2024 :

https://www.youtube.com/watch?v=072y-d3iVWw

#SatSolving #HPC #AutomatedReasoning
@informatik @KITInformatik

Science Slam | GI-Dissertationspreis 2024

YouTube
DominikSep 14, 2024

In this year's SAT Competition, Mallob @ 1600 threads proved its worth against two other distributed systems, scoring its 5th gold in a row. In the shared-memory track, one of my submissions is (to my knowledge) the first ever parallel submission that produces and checks proof information, which drastically increases confidence in the result. See: http://doi.org/10.4230/LIPIcs.SAT.2024.25 The associated overhead was so small that it also scored some medals!

Details: https://satcompetition.github.io/2024/downloads/satcomp24slides.pdf

Trusted Scalable SAT Solving with On-The-Fly LRAT Checking

DominikSep 9, 2024
I'm very honored to have received the inaugural Fahiem Bacchus Award at #SAT'24 in Pune (India) for my dissertation entitled Scalable #SATSolving and its Application. Many thanks to the award committee, including @arminbiere, for this amazing recognition! It really encourages me to continue this research, further pushing the scalability of #AutomatedReasoning in #HPC and #Cloud systems.
DominikAug 28, 2024
Gesellschaft für Informatik eVAug 28, 2024

Bald ist September und das bedeutet: Die Award-Season der Informatik beginnt! 😎

Zusammen mit @ocg und der Schweizer Informatik Gesellschaft verleihen wir den Dissertationspreis an zwei Forschende:
🏅 Menatallah El-Assady von der ETH Zürich
🏅 https://sueden.social/@dompasch von @KIT_Karlsruhe

Alle Infos: https://gi.de/meldung/erklaerbare-und-symbolische-ki-gi-dissertationspreis

Dominik (@[email protected])

6 Beiträge, 32 Folge ich, 11 Follower · Postdoctoral researcher @[email protected] | #SATSolving, #HPC, AI planning | 🎸🎹🪕🎤👨‍🍳🎮

sueden.social
Show threadDominikAug 28, 2024
@informatik @KIT_Karlsruhe
Es ist eine große Ehre für mich, den Dissertationspreis der Gesellschaft für Informatik zu erhalten. Meine Dissertation verbessert die Skalierbarkeit von #SATSolving in verteilten Rechenumgebungen wie Supercomputern (#HPC) und #Clouds. Mit diesen Fortschritten können wir viele praxisrelevante Probleme logischer Natur (z.B. #Verifikation, #Kryptographie, #SymbolicAI, Schaltkreisdesign) wesentlich schneller lösen als zuvor.
DominikAug 23, 2024
Don't call it portfolio #SATsolver! In our latest journal article, we show that getting clause sharing right leads to scalable distributed #SATSolving even if all solver threads are initially identical. This motivates us to drop the prior portfolio-centric intuition for parallel SAT and to rather adopt the term "clause-sharing (SAT) solver" going forward. https://doi.org/10.1613/jair.1.15827 #AutomatedReasoning #KIT #SAT #HPC
MallobSat: Scalable SAT Solving by Clause Sharing | Journal of Artificial Intelligence Research

Show threadDominikApr 27, 2023
@maximaximal Indeed a great general assembly of Cloud track participants!
DominikDec 23, 2022
Today's clause-sharing portfolio #SATSolving cannot produce UNSAT proofs, which makes it unsuitable whenever trusting a result is critical. This changes! In our paper just accepted at #TACAS 2023, #AWS-affiliated researchers (D. Michaelson, M. Heule, M. Whalen, B. Kiesl-Reiter) and I have derived a scalable approach based on LRAT+CaDiCaL+Mallob producing efficiently verifiable proofs, with some interesting distributed algorithms and showing good performance on up to 800 cores. More coming soon!
Show threadDominikDec 19, 2022
Mallob in 2020 was using Lingeling(+YalSAT), and so did "Mallob-Ki" in 2022, in contrast to Mallob-Ki(ssat)Ca(dical)Li(ngeling)Glu(cose).
The data is not free from biases – for example I've been tuning Mallob on the 2020 benchmarks for a while. Still, some very nice improvement on what I'd consider to be a broad set of benchmarks.
DominikDec 19, 2022
Without running any new experiments, here's the progress of sequential, parallel, and cloud #SATSolving from 2020 to 2022 based on #SATCompetition data. I used the intersection of the 2020 benchmarks and the 2022 anniversary benchmarks (→ 354 instances). Showing the 2020 winners and the 2022 anniversary winners. (higher = better; legend is sorted according to the curves' positioning)