I saw an impressive plot at the recent SAT'25 conference: Two CaDiCaLs are plotted against each other. The one on the bottom recieves instances just in their original form, while the left one recives them reencoded in some clever new way, developed by Aeacus Sheng, Joseph E. Reeves and Marijn Heule. This reencoding scheme detects Unique Literal Clauses (ULCs), and rewrites them. ...

Apparently, Cactus plots can be confusing to audiences. To see just how confusing, take this talk of Armin Biere at the 2014 BIRS workshop, in front of a partially non-SAT audience. ...

I just learned that CDF plots were introduced to SAT around the year 2020. That’s… surprisingly recent! I always assumed that Cactus and CDF had co-existed for a long time, and that Cactus was more dominant in older papers due to some personal preferences. After all, they are just flipped versions of each other, around the x=y line. But no, CDFs plots were apparently introduced to the SAT community only in 2020, at the 22:26 minute mark in the PoS 2020 Lightning Talk by Armin Biere. There, he presents this strange new plotting style and argues (in front of a partially sceptical audience) for its adoption. Who would have though that CDF (within the SAT community) is such a new concept. ...

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