Category: Uncategorized
-
Arjun, our New CNF Model Counting Preprocessor
After many years of work, I am very happy to present our new CNF model counting preprocessor, Arjun [PDF][static binary]. It improves upon our approximate model counter ApproxMC [static binary], and can be used as a stand-alone binary to preprocess CNFs for (projected) model counting . Usage is simple: ./arjun blasted_case110.cnfc Arjun Version: 43b17ef5899c461b8e947b0f3ca286efcf71464cc CMS […]
-
Proof Traces for SAT solvers
If you have a look at a modern SAT solver, say kissat or CryptoMiniSat, you’ll see that they have well over 20k lines of code. Reviewing that for bugs is basically impossible. So how can you trust that the solver is giving a correct result? Well, if the result is that the input formula is […]
-
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 […]
-
Why Most Published Research Findings Are False
I read this paper about most research findings being false. Given that most research papers in SAT take a sample size that is incredibly small (especially considering that it’s cheap to have large sample sizes relative to, e.g. medical trials), and the samples are very often hand-picked, it’s easy to see why this could be […]