My first conference! Few days ago concluded the SAT 2025 conference in Glasgow. It was my very first conference, completely surrounded with others also working on SAT.
Shoutout to the professors and senior researchers – they were exceptionally friendly, cordial and open to a chat. I could just walk up and always felt welcomed. I know that this is how it should be in theory, but I am not sure how many fields can actually deliver on this promise – here it was actually the case.
Also all the other PhD students - getting to know them was fantastic, and helpful. Learning what they were working on, what went well for them and what didn’t. And what they thought about recent results, and about weaknesses of current techniques. All the good stuff that you (sadly) just don’t find that easily in papers.
One person had ideas about speeding up Unit-Propagation via a completely new watching-scheme. Unit propagationis still the most time consuming aspect of current solvers by far, so any progress in that direction would be really cool to see – I hope it will turn out well and we will see something in that direction. Another topic closer to my own research was the different attempts of parallelizing SAT solving, Cube and Conquer on the one side and Clause Sharing on the other, and whether one approach could learn something from the other.
I learned that MiniSat is still used by quite some people on the application side, even after 20 years. And that they tried the newer solves, but they performed worse. They see the yearly SAT competition, but it just doesn’t translate to their problems. Maybe because modern solvers try dozens of difficult optimizations, whereas most of their application SAT-problems are rather small and easy – something the current competition is mostly blind towards. As a service to these people, maybe a MiniSat-Replacement-Track would be interesting. Only formulas on which MiniSat is particularly strong, say, solves in less than a minute or solves faster than Kissat/CaDiCal/Glucose. This could provide some fresh rankings for people who want to replace their rusty MiniSats with more modern things the SAT community has to offer, but specifically geared towards the use-cases where MiniSat is currently still strongest.