GET IN TOUCH

Workshop on Counting, Sampling, and Synthesis 2024

Registration

Please register for the SAT conference.

Purpose

The Workshop on Counting, Sampling, and Synthesis is an event for researchers in model counting and sampling. It covers advanced topics such as weighted and projected counters/samplers and various domains such as SAT, SMT, ASP, and CP. This year, the workshop has expanded its focus to include the role of model counters, samplers, and solvers in automated synthesis. The goal of the workshop is to facilitate the exchange of cutting-edge theoretical and practical insights, with a particular emphasis on innovative solver technologies and their real-world applications. Additionally, the workshop provides an opportunity for developers of model counters to showcase their work and share detailed competition results, to encourage discussions that bridge theory and practice.

Venue

This year’s event will be held alongside other workshops at the SAT 2024 conference. For more information, please visit the SAT 2024 website.

Date

Day: Tuesday, August 20th, 2024

Schedule

Time	Title	Author(s)/ Presenter
9.20-9.30	Opening Remarks	——-
9.30-10.00	Proof Systems for Tensor-based Model Counting The model counting problem #SAT, asking for the number of satisfying assignments of a propositional formula, has been explored intensively in the #SAT solving community. One of the main algorithmic approaches for #SAT solving is through contraction in tensor hypernetworks. We perform a theoretical proof-complexity analysis of this approach. For this, we design two new tensor-based proof systems that we show to tightly correspond to tensor-based #SAT solving. We determine the simulation order of #SAT proof systems and prove exponential separations between the systems. This sheds light on the relative performance of different #SAT solving approaches.	Olaf Beyersdorff, Joachim Giesen, Andreas Goral, Tim Hoffmann, Kaspar Kasche and Christoph Staudt
10.00-10.30	An Approximate Skolem Function Counter Motivated by the recent development of scalable approaches to Boolean function synthesis, we study the following problem: Given a Boolean specification between a set of inputs and outputs, count the number of functions of inputs such that the specification is met. Counting Skolem functions poses considerable new challenges. From the complexity-theoretic standpoint, counting Skolem functions is not only #P -hard; it is quite unlikely to have an FPRAS as the problem of synthesizing a Skolem function remains challenging, even given access to an NP oracle. The primary contribution of this work is the first algorithm, SkolemFC, that computes an estimate of the number of Skolem functions. SkolemFC relies on technical connections between counting functions and propositional model counting: our algorithm makes a linear number of calls to an approximate model counter and computes an estimate of the number of Skolem functions with theoretical guarantees. Moreover, we show that Skolem function count can be approximated through a polynomial number of calls to a SAT oracle. Our prototype displays impressive scalability, handling benchmarks comparably to state-of-the-art Skolem function synthesis engines, even though counting all such functions ostensibly poses a greater challenge than synthesizing a single function.	Arijit Shaw , Kuldeep S. Meel and Brendan Juba
10.30-11.00	Tea/Coffee Break	——-
11.00-11.30	Testing Self-Reducible Samplers Samplers are the backbones of randomized algorithms. Unfortunately, obtaining an efficient algorithm to test the correctness of samplers is very hard. Recently, in a series of works, testers like Barbarik, Teq, and Flash for testing some particular samplers, such as Cnf-samplers, were developed. However, their techniques have significant limitations because one cannot expect to use their methods to test other samplers, such as samplers for graphs. In this paper, we present a new testing algorithm that works for such samplers and can estimate the distance of a target sampler from an ideal sampler (say, uniform sampler). This paper’s main contribution is a new distance estimation algorithm for distributions over high-dimensional cubes using the recently proposed sub-cube conditioning model. Given subcube conditioning access to an unknown distribution, and a known distribution defined over n dimensional hypercube, our algorithm estimates the variation distance between the distributions within an additive error. The estimation algorithm in the sub-cube conditioning model helps us to design the first tester for self-reducible samplers. We also implement our algorithm and use it to test the quality of three state-of-the-art graph samplers.	Rishiraj Bhattacharyya, Sourav Chakraborty, Yash Pote, Uddalok Sarkar and Sayantan Sen
11.30-12.00	Circuits, Proofs and Propositional Model Counting In this paper we present a new proof system framework CLIP (Circuit Linear Induction Proposition) for propositional model counting.A CLIP proof firstly involves a circuit, calculating the cumulative function (or running count) of models counted up to a point, and secondly a propositional proof arguing for the correctness of the circuit. This concept is remarkably simple and CLIP is modular so allows us to use existing checking formats from propositional logic, especially strong proof systems. Despite model counting being a harder problem than unsatisfiability, we find that CLIP only has lower bounds from its propositional proof system or if P^{#P} is not contained in P/poly, similar to results in QBF proof complexity (Beyersdorff et al. Journal of the ACM 2020). From a proof complexity point of view we find it is exponentially stronger than existing proof systems MICE (Fichte et al. SAT 2022) and KCPS(#SAT) (Capelli SAT 2019) for propositional model counting.	Sravanthi Chede , Leroy Chew and Anil Shukla
12.00-14.00	Lunch	——-
14.00-14.30	Using Counterexamples to Improve Robustness Verification in Neural Networks Given the pervasive use of neural networks in safety-critical systems it is important to ensure that they are robust. Recent research has focused on the question of verifying whether networks do not alter their behavior under small perturbations in inputs. Most successful methods are based on the paradigm of branch-and-bound, an abstraction-refinement technique. However, despite tremendous improvements in the last five years, there are still several benchmarks where these methods fail. One reason for this is that many methods use off-the-shelf methods to find the cause of imprecisions. In this paper, our goal is to develop an approach to identify the precise source of imprecision during abstraction. We present a novel counterexample guided approach that can be applied alongside many abstraction techniques. As a specific case, we implement our technique on top of a basic abstraction framework provided by the tool DeepPoly and demonstrate how we can remove imprecisions in a targetted manner. This allows us to go past DeepPoly’s performance as well as outperform other refinement approaches in literature. Surprisingly, we are also able to verify several benchmark instances on which all leading tools fail.	Mohammad Afzal
14.30-15.00	Formally Certified Approximate Model Counting Approximate model counting is the task of approximating the number of solutions to an input Boolean formula. The state-of-the-art approximate model counter for formulas in conjunctive normal form (CNF), ApproxMC, provides a scalable means of obtaining model counts with probably approximately correct (PAC)-style guarantees. Nevertheless, the validity of ApproxMC’s approximation relies on a careful theoretical analysis of its randomized algorithm and the correctness of its highly optimized implementation. We present the first certification framework for approximate model counting with formally verified guarantees on the quality of its output approximation. Our approach combines: (i) a static, once-off, formal proof of the algorithm’s PAC guarantee in the Isabelle/HOL proof assistant; and (ii) dynamic, per-run, verification of ApproxMC’s calls to an external CNF-XOR solver using proof certificates. We detail our general approach to establish a rigorous connection between these two parts of the verification, including our blueprint for turning the formalized, randomized algorithm into a verified proof checker, and our design of proof certificates for both ApproxMC and its internal CNF-XOR solving steps. Experimentally, we show that certificate generation adds little overhead to an approximate counter implementation, and that our certificate checker is able to fully certify 84.7\% of instances with generated certificates.	Yong Kiam Tan, Jiong Yang , Mate Soos, Magnus O. Myreen and Kuldeep S. Meel
15.00-15.30	Exact ASP Counting with Compact Encodings Answer Set Programming (ASP) has established itself as a robust paradigm for knowledge representation and automated reasoning, adept at handling complex combinatorial problems across various domains. Leveraging developments in propositional SAT solving, the last two decades have seen the advent of sophisticated systems capable of addressing the answer set satisfiability problem, which involves identifying models or answer sets for specific ASP programs. Recently, interest has expanded to include more complex problems, such as model counting within ASP. This work introduces a novel framework for ASP counting, named sharpASP, designed to efficiently count answer sets without heavyweight propositional encoding. It employs an innovative approach to defining answer sets, incorporating advanced techniques from propositional model counting. Our comprehensive empirical evaluation, involving 1470 benchmarks, reveals that sharpASP significantly outperforms existing exact answer set counters. Specifically, sharpASP resolved 1062 benchmarks with a PAR2 score of 3082, compared to the previous best of 895 benchmarks with a PAR2 score of 4205 under identical experimental conditions.	Mohimenul Kabir , Supratik Chakraborty and Kuldeep S Meel
15.30-16.00	Tea/Coffee break	—-
16.00-16.30	Efficient and Practical Methods for Quantifier Elimination and Program Synthesis This talk will begin with a brief introduction to Quantifier Elimination (QE) for Non-Linear Real Arithmetic (NRA) and its application in program synthesis. I will then introduce the notations and techniques from Real Algebraic Geometry that form the foundation of our algorithms. Building on this background, I will present the key ideas of our algorithms. First, I will discuss an approximate yet efficient method for QE over NRA, which leverages a Boolean combination of linear constraints. Our approach approximates the solution space of NRA constraints using adaptive dynamic gridding and Handelman’s Theorem, solving the problem through a sequence of linear programs (LP). We provide rigorous approximation guarantees and proofs of soundness and completeness under mild assumptions. This method, implemented in a preprocessor for Z3 called POQER, has demonstrated superior performance on non-trivial benchmarks compared to state-of-the-art SMT solvers. Next, I will address the synthesis of the weakest pre-condition and the corresponding program for a given post-condition over integer variables. Utilizing Farkas’ Lemma and Handelman’s Theorem, we propose a novel, practical, and exact algorithm to synthesize both the program and the pre-condition over bounded integer variables. Our method ensures the weakest pre-condition is found and outputs simple, analyzable linear decision lists for both the program and pre-condition. Experimental results validate the real-world applicability and significant performance gains of our approach.	Akshay S, Chakraborty S, Goharshady AK, Govind R, Motwani HJ, and Varanasi ST
16.30-17.00	Discussion on the Model Counting Competition	Arijit Shaw
17.00-17.10	Concluding Remarks	—

Contact

If you have any questions about the workshop, the best way to contact the organizers is by emailing mcw at modelcounting.org.