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

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

#SatSolving #HPC #AutomatedReasoning
@informatik @KITInformatik

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.

@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.

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

@tao good to see the mentioning of topics such as #AutomatedReasoning and #SatSolving. There has been significant progress in these fields in the last 30 years as well, so I am a bit surprised that they are dubbed as GOFAI, which characterizes the limits of rule-based systems https://en.m.wikipedia.org/wiki/GOFAI

Oh, polynomial3sat.org is down and the respective code on GitHub is removed. The corresponding paper on arXiv is still accessible. Does anyone know more about what happened?

https://arxiv.org/abs/1903.10081

#satsolving #complexitytheory #PequalsNP #compsci #theoreticalcomputerscience

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!

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)

#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.

@cjmuise @terri Creating a Mosaic Knitting pattern generator could be an interesting place to start. There are quite some limitations to mosaic knitting patterns, and they are typically geometric. It could be an interesting challenge to capture the rules of mosaic knitting into a CNF and have a solver generate solutions, then visualise them as patterns and allow the user to select one they like?

#knitting #geometry #programming #SATSolving #BooleanSatisfiability