CrystalBall: SAT solving, Data Gathering, and Machine Learning

Link to the original post on CrystallBall.  

Knowledge Compilation meets Uniform Sampling

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.

WAPS: Weighted and Projected 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.

GANAK: A Scalable Probabilistic Exact Model Counter

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.

Bosphorus: An ANF and CNF simplifier and converter

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.

ApproxMCv3: A modern approximate model counter

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.