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

#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