This blogpost is based on our paper that got published in the procedings of International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), 2018. The code is available here. The primary contribution of this work is marrying knowledge compilation with uniform sampling to design a new uniform sampler KUS. The main result is that KUS is able to solve more number of benchmarks than existing state-of-the-art uniform and almost-uniform samplers beating them by orders of magnitude in terms of runtime: Uniform Sampling
This blogpost talks about our tool WAPS. Specifically, we will talk about how we are able to utilize the idea of sampling using knowledge compilations (d-DNNFs) from our previous work (KUS) and generalize it in order to achieve weighted and projected sampling. You can read the paper here and get the tool here. You can read the previous blog that describes uniform sampling using knowledge compilations, though it is not absolutely necessary for this post.
This blogpost talks about our tool GANAK that inherits current advancements in SAT solving and model counting, improves upon them and contributes new ideas, thereby outperforming state-of-the-art model counters. The source code of GANAK is available here and the paper is available here. The main result is that we can solve a lot more problems than before: Let’s first define Model Counting. Model Counting
Given a Boolean formula $F$, over a set of variable $X$, model counting (aka #SAT) seeks to compute the number of solutions of $F$.
We are happy to release our ANF and CNF simplifier and converter called Bosphorus. It has helped us break multiple real-world ciphers. It has been re-released with major work by Davin Choo & Kian Ming A. Chai from DSO National Laboratories Singapore and Mate Soos & Kuldeep Meel from NUS. The paper will be published at the DATE 2019 conference.
ANFs and CNFs Algebraic Normal Form is a form that is used by most cryptographers to describe symmetric ciphers, hash algorithms, and lately a lot of post-quantum asymmetric ciphers.
ApproxMC is a scalable, approximate model counter that provides PAC (probably approximately correct) guarantees. We have been working very hard on speeding up approximate model counting for SAT and have made real progress. The research paper, accepted at AAAI-19 is available here. The code is available here (release with static binary here). The main result is that we can solve a lot more problems than before. The speed of solving is orders(!