Wonderings of SAT geek

  • CryptoMiniSat 5.8.0 Released

    After many months of work, CryptoMiniSat 5.8.0 has been released. In this post I’ll go through the most important changes, and how they helped the solver to be faster and win a few awards, among them 1st place at the SAT incremental track, 3rd place SAT Main track, and 2nd&3d place in the SMT BitVector […]

  • Weighted to Unweighted Counting and Sampling

    This blog post is to promote the tool here (paper here) that converts weighted counting and sampling to their unweighted counterparts. It turns out that weighted counting and sampling is a thing. It’s basically a conjunctive normal form formula, a CNF, with weights attached to each variable. One must count the number of solutions to […]

  • CrystalBall: SAT solving, Data Gathering, and Machine Learning

    This is going to be a long post, collecting many years of work, some of which was done by my colleagues Kuldeep Meel and Raghav Kulkarni. They have both significantly contributed to this work and I owe a lot to both. The research paper is available here (accepted to SAT’2019) and the code is available […]

  • SAT Solvers as Smart Search Engines

    Satisfiability problem solvers, or SAT solvers for short, try to find a solution to decidable, finite problems such as cryptography, planning, scheduling, and the like. They are very finely tuned engines that can be looked at in two main ways . One is to see them as proof generators, where the SAT solver is building […]

  • Bosphorus, an ANF and CNF simplifier and converter

    I am happy to finally release a piece of work that I have started many years ago at Security Research Labs (many thanks to Karsten Nohl there). Back in the days, it helped us to break multiple real-world ciphers. The released system is called Bosphorus and has been released with major, game-changing work by Davin […]