Mastodawn

Dominik Sep 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

Dominik Sep 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

Dominik Sep 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.

Dominik Aug 28, 2024

Gesellschaft für Informatik eV Aug 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

Dominik Aug 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

Dominik Dec 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 thread

Dominik Dec 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.

Dominik Dec 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)

Dominik Dec 16, 2022

#Introduction #AcademicMastodon
Hi there! I'm a #CompSci doctoral researcher at @KIT_Karlsruhe, Algorithm Engineering group, with a focus on distributed algorithms, #HPC, and automated reasoning. Author of Mallob (#Cpp, LGPL) – a decentralized job processing platform and the current state of the art in large-scale #SATSolving. Might post some insights or results on here from time to time.

Dominik Nov 23, 2022