Wonderings of SAT geek

  • How Approximate Model Counting Works

    Approximate model counting allows to count the number of solutions (or “models”) to propositional satisfiability problems. This problem seems trivial at first given a propositional solver that can find a single solution: find one solution, ban it, ask for another one, ban it, etc. until all solutions are counted. The issue is that sometimes, the […]

  • ApproxMCv3, a modern approximate model counter

    This blogpost and its underlying work has been brewing for many years, and I’m extremely happy to be able to share it with you now. Kuldeep Meel and myself have been working very hard on speeding up approximate model counting for SAT and I think we have made real progress. The research paper, accepted at […]

  • The Cult of Security/Privacy By Design

    I have been reading a lot of privacy literature lately and the more I read, the more I got frustrated with the “Privacy by Design” motto. It somehow was not right, and made me realise that “Security by Design” motto is similarly hyped and is just as misguided. Let me explain. Why security/privacy wasn’t baked […]

  • CryptoMiniSat and Parallel SAT Solving

    Since CryptoMiniSat has been getting quite a number of awards with parallel SAT solving, it’s about time I talk about how it does that.There is a ton of literature on parallel SAT solving, and I unfortunately I have barely had time to read any of them. The only research within the parallel SAT solving area […]

  • CryptoMiniSat 5.6.3 Released

    The latest CryptoMiniSat, version 5.6.3 has been released. This release marks the 12’000th commit to this solver that has weathered more than I originally intended it to weather. It’s been an interesting ride, and I have a lot to thank Kuldeep and NSCC‘s ASPIRE-1 cluster for this release. I have burned over 200k CPU hours […]