GET IN TOUCH

Workshop on Counting and Sampling 2023

Registration

Please register with the SAT conference.
See: http://satisfiability.org/SAT23/pages/registration.html

Virtual Participation

For those who cannot attend due to travel preferences or restrictions,
we will prepare a hybrid option for you via Zoom. However, we cannot guarantee a stable connection
due to potential local restrictions or complications. Please contact us directly for login credentials.

Updates

See also updates on Twitter Johannes, Kuldeep.

DATE

Day: Tuesday, July 4th, 2023 (Times are given in GMT+2/CEST/Alghero, see your timezone)

Program

Time CEST	Title (Abstract)	Author(s)	Slides	Recordings
08:30	Room open	Johannes K. Fichte, Markus Hecher
08:50 - 09:00	Welcome	Johannes K. Fichte, Markus Hecher
09:00 - 09:30	Tseitin or not Tseitin? The Impact of CNF Transformations on Feature-Model Analyses This work was published at the 37th IEEE/ACM International Conference on Automated Software Engineering (ASE) 2022. It is joint work between the universities of Magdeburg and Ulm, Germany. Feature modeling is widely used to systematically model features of variant-rich software systems and their dependencies. By translating feature models into propositional formulas and analyzing them with solvers, a wide range of automated analyses across all phases of the software development process become possible. Most solvers only accept formulas in conjunctive normal form (CNF), so an additional transformation of feature models is often necessary. However, it is unclear whether this transformation has a noticeable impact on analyses. We compare three transformations for bringing feature-model formulas into CNF. We analyze which transformation can be used to correctly perform feature-model analyses and evaluate three CNF transformation tools on a corpus of 22 real-world feature models. Our empirical evaluation illustrates that some CNF transformations do not scale to complex feature models or even lead to wrong results for model-counting analyses. Further, the choice of the CNF transformation can substantially influence the performance of subsequent analyses. The talk will highlight the interactions between CNF transformations and model counting in the context of feature-model analysis. Also, we give an outlook on current challenges, such as counting the number of valid configurations of the Linux kernel by means of incremental analysis.	Elias Kuiter	Abstract (tbd)	TBD
09:30 - 10:00	Rounding Meets Approximate Model Counting The problem of model counting, also known as #SAT, is to compute the number of models or satisfying assignments of a given Boolean formula F. Model counting is a fundamental problem in computer science with a wide range of applications. In recent years, there has been a growing interest in using hashing-based techniques for approximate model counting that provide (ε,δ)-guarantees: i.e., the count returned is within a (1+ε)-factor of the exact count with confidence at least 1−δ. While hashing-based techniques attain reasonable scalability for large enough values of δ, their scalability is severely impacted for smaller values of δ, thereby preventing their adoption in application domains that require estimates with high confidence. The primary contribution of this paper is to address the Achilles heel of hashing-based techniques: we propose a novel approach based on rounding that allows us to achieve a significant reduction in runtime for smaller values of δ. The resulting counter, called RoundMC, achieves a substantial runtime performance improvement over the current state-of-the-art counter, ApproxMC. In particular, our extensive evaluation over a benchmark suite consisting of 1890 instances shows that RoundMC solves 204 more instances than ApproxMC, and achieves a 4× speedup over ApproxMC.	Jiong Yang and Kuldeep S. Meel	Abstract (tbd)	TBD
10:30 - 11:00	+++++++++ Coffee Break +++++++++
11:00 - 11:30	Probabilistic Query Evaluation: The Combined FPRAS Landscape Consider the problem of computing the probability of a query over a tuple-independent probabilistic database, known as the probabilistic query evaluation (PQE) problem. The problem is well-known to be #P-hard in data complexity for conjunctive queries in general, as well as for several subclasses of conjunctive queries (Dalvi and Suciu 2004). Existing approximation approaches for dealing with hard queries have centred on reducing the problem to approximate (weighted) model counting, by computing the lineage of the query over the database as a propositional formula. However, this approach is intractable for all but the smallest of queries due to the possibly exponential dependence of the size of this formula on the query length. In this talk, I will show how to construct a fully polynomial-time randomized approximation scheme (FPRAS) for the PQE problem for any class of self-join-free conjunctive queries of bounded hypertree width, that runs in time polynomial in both the query length and database size. An interesting consequence of this result is the existence of classes of queries that are #P-hard in data complexity to evaluate exactly, yet easy to approximate both in terms of query length and database size. The result builds on a recent breakthrough in approximating the number of fixed-size trees accepted by a non-deterministic finite tree automaton (Arenas, Croquevielle, Jayaram and Riveros 2021). Joint work with Kuldeep S. Meel. Based on a paper accepted to PODS 2023.	Timothy van Bremen and Kuldeep S. Meel	Abstract (tbd)	TBD
12:00 - 12:30	Fast Converging Anytime Model Counting This paper was accepted at AAAI 2023 Model counting is a fundamental problem which has been influential in many applications, from artificial intelligence to formal verification. Due to the intrinsic hardness of model counting, approximate techniques have been developed to solve real-world instances of model counting. This paper designs a new anytime approach called PartialKC for approximate model counting. The idea is a form of partial knowledge compilation to provide an unbiased estimate of the model count which can converge to the exact count. Our empirical analysis demonstrates that PartialKC achieves significant scalability and accuracy over prior state-of-the-art approximate counters, including satss and STS. Interestingly, the empirical results show that PartialKC reaches convergence for many instances and therefore provides exact model counting performance comparable to state-of-the-art exact counters.	Yong Lai, Kuldeep S. Meel and Roland Yap	Abstract (tbd)	TBD
12:30 - 13:00	A Fast and Accurate ASP Counting Based Network Reliability Estimator The quantiﬁcation of system reliability is crucial to assess a system’s safety and resilience, and has been of interest to decision-makers. In general, the network reliability problem is determining the probability that a network would behave as per intended speciﬁcations in the presence of unreliable components. We focus on the 2-terminal reliability problem, which is also extendable to the K-terminal reliability problem. Our graphs are probabilistic, and the probabilities are associated with their edges. The two-terminal reliability problem seeks to compute the likelihood that two nodes of interest are connected. The seminal work of Valiant showed that the network reliability problem is #P-complete. Thus, the exact methods scale to networks of small size or with certain bounded properties, such as treewidth and diameter, which highlights the necessity to develop approximate techniques for network reliability computation. In particular, we focus on (ε, δ)-approximation of network reliability, wherein the estimated reliability is within (1 + ε)-factor of the exact network reliability with a conﬁdence of at least 1 − δ. The main contribution of our work is RelNet-ASP, a framework for network reliability estimation. RelNet-ASP reduces the problem of reliability estimation to an approximate model counting problem over Answer Set Programs (ASP). RelNet-ASP combines ASP modeling and theories from weighted model counting for network reliability estimation. Our empirical evaluation demonstrates that RelNet-ASP signiﬁcantly outperforms prior state-of-the-art approaches in terms of both accuracy and runtime performance. In particular, RelNet achieved a TAP score (a performance metric assessing the accuracy and runtime eﬃciency; the lower, the better) of 2262, while the nearest scalable estimator achieved a TAP score of 2853.	Mohimenul Kabir and Kuldeep S. Meel	Abstract (tbd)	TBD
13:00 - 14:00	+++++++++ Lunch Break +++++++++
14:30 - 15:00	Discussion on the Competition	Johannes K. Fichte and Markus Hecher	Abstract (tbd)	TBD
15:00 - 15:30	Enumerating Disjoint Partial Models without Blocking Clauses Satisfiability Problem (AllSAT) is an extension of SAT that requires finding all (partial) models of a propositional formula, ensuring all models are pairwise inconsistent. Disjoint AllSAT is strictly related to model counting (#SAT): instead of simply returning the number of solutions as in model counting, we enforce the solver to generate all the assignments for enumeration. Consequently, novel algorithms and techniques for AllSAT could benefit #SAT as well. Moreover, disjoint AllSAT/AllSMT is the core of several algorithms for AI tasks, such as #SMT - an extension of #SAT enumerating models in first-order theories - and Weighted Model Integration (WMI) - a paradigm extending Weighted Model Counting (WMC) to deal with SMT formulae that contain both Boolean and first-order theory atoms. In this context, we are interested in enumerating all the assignments satisfying a probabilistic model, encoded as an SMT formula, and then performing numerical integration on the weight function defined by these assignments.When performing disjoint AllSAT we are interested in i) finding a compact representation of the set of assignments for a propositional formula; ii) scanning the search space efficiently to generate these assignments. In the literature, we can distinguish two main categories of AllSAT algorithms. Blocking AllSAT solvers rely on Conflict Driven Clause-Learning (CDCL) and non-chronological backtracking (NCB) to scan the entire search space by pruning already-visited conflicting conditions. To avoid duplicate solutions, blocking clauses are constructed from obtained assignments (i.e. the disjunction of all negated decision literals) and appended to the initial input formula. Although blocking solvers are straightforward to implement and can be adapted to retrieve partial assignments, they become inefficient when the input formula has a high number of models, as an exponential number of blocking clauses might be added to make sure the entire search space is visited. As the number of blocking clauses increases, unit propagation becomes more difficult, resulting in degraded performance. Non-blocking AllSAT solvers overcome this issue by not introducing blocking clauses and by implementing chronological backtracking (CB): after a conflict arises, we backtrack on the search tree by updating the most recently instantiated variable. Chronological backtracking guarantees not to cover the same model of a formula multiple times without the typical CPU-time blow-up caused by blocking clauses. The major drawback of this approach is that there is no method known in the literature which would allow it to be combined with partial assignments. Moreover, regions of the search space with no solution can not be escaped easily if CDCL is not integrated. In this context, a new formal calculus of a disjunctive model counting algorithm was proposed by Mohle and Biere in 2018, combining the best features of chronological backtracking and CDCL, but without providing an implementation or experimental results. Our goal is to apply these ideas in the context of AllSAT solving, and achieve better overall performance compared to existing approaches, particularly when instances with high numbers of solutions are considered. Our AllSAT solver, TabularAllSAT, combines the best of current AllSAT state-of-the-art literature: i) CDCL, to escape search branches where no satisfiable assignments can be found; ii) chronological backtracking, to ensure no blocking clauses are introduced; iii) efficient implicant shrinking, to reduce in size partial assignments, by exploiting the 2-literal watching scheme. We compared its performance against other publicly available state-of-the-art AllSAT tools using a variety of benchmarks, including both crafted and SATLIB instances. Our experimental results show that TabularAllSAT outperforms all other solvers on most benchmarks, demonstrating the benefits of our idea.	Giuseppe Spallitta, Roberto Sebastiani and Armin Biere	Abstract (tbd)	TBD
15:30 - 16:30	+++++++++ Coffee Break +++++++++
16:30 - 17:00	ABC: Automata-Based Model Counting for String and Numeric Constraints The Automata-based Model Counter (ABC) is a model counting constraint solver for string and numeric constraints. Given a mixed string and linear integer arithmetic constraint formula written in SMT-LIB2, ABC first constructs automata representing the set of solutions to the constraint formula. ABC then counts the number of solutions to the constraint by counting the number of accepting paths in the constructed automata for a given bound. Recent advances to ABC, such as the inclusion of multi-track automata for capturing relationships between variables and subformula caching for reusing prior results, have made ABC the most expressive and scalable model counting constraint solver for mixed string and numeric constraints.	William Eiers and Tevfik Bultan	Abstract (tbd)	TBD
17:00 - 17:30	Top-Down Knowledge Compilation for Counting Modulo Theories (VIRTUAL) Propositional model counting (#SAT) can be solved efficiently when the input formula is in deterministic decomposable negation normal form (d-DNNF). Translating an arbitrary formula into a representation that allows inference tasks, such as counting, to be performed efficiently, is called knowledge compilation. Top-down knowledge compilation is a state-of-the-art technique for solving #SAT problems that leverages the traces of exhaustive DPLL search to obtain d-DNNF representations. While knowledge compilation is well studied for propositional approaches, knowledge compilation for the (quantifier free) counting modulo theory setting (#SMT) has been studied to a much lesser degree. In this paper, we discuss compilation strategies for #SMT. We specifically advocate for a top-down compiler based on the traces of exhaustive DPLL(T) search.	Vincent Derkinderen, Pedro Zuidberg Dos Martires, Samuel Kolb and Paolo Morettin.	Abstract (tbd)	TBD
17:30 - 18:00	Towards Building A Scalable Bit-vector Model Counter Satisfiability Modulo Theory (SMT) solvers have transformed the field of automated reasoning owing to their established efficiency in handling problems arising from diverse domains. Given the significant progress achieved by SMT solvers over the past two decades, there has been interest in the problems that require reasoning beyond satisfiability. In this work, we focus on the problem of model counting on the quantifier-free fragment of the theory of bit-vector arithmetic. This work involves the design of a portfolio-based bitvector counter, SharpSMT, the creation of an application benchmark set for testing, and extensive empirical evaluation for different configurations of CNF-counters, propositionalization techniques, and preprocessors; ultimately resulting in a system that solves four times the number of benchmarks solved by current state-of-the-art methods. Our empirical analysis highlights the importance of careful tight integration of propositionalization, preprocessing, and CNF-counters in building such a system.	Arijit Shaw and Kuldeep S. Meel	Abstract (tbd)	TBD
18:00 - 18:30	Discussions and Closing	Johannes K. Fichte, Markus Hecher, Kuldeep S. Meel	Abstract (tbd)	TBD
19:00	++++++++++ Room Closed +++++++++

Purpose

The International Workshop on Counting and Sampling aims to provide a venue for researchers working on model counting such as model counting (mc), weighted model counting/sum of products (wmc), projected model counting (pmc) as well as sampling models within the realm but not restricting to Boolean satisfiability (SAT), satisfiability modulo theories (SMT), Answer set programming (ASP), and constraint programming (CP). It encourages to meet, communicate, and discuss the latest theoretical and practical results, in particular results on novel solvers, related solver technologies, new theoretical advances, practical academic and industrial applications as well as the linking theory and practice. The workshop is also the place for developers of model counters to present their solvers and the presentation of detailed results on the model counting competition.

Venue

The workshop will be colocated with the Workshops at the SAT 2023 Conference. We refer to the SAT 2023 Website.

Timeline

see Dates

Format

You present your best work related to counting and sampling, be it published elsewhere or yet unpublished.

Agenda / Talks

20min (Talk) + 10min (Q&A)
5min break

Submissions

Submission: We place no format requirement. We expect that you provide a reasonable description in txt or pdf-format and upload this on Easychair.

Procedures for selecting papers: All submissions will be reviewed by 1-2 program committee members and papers will be selected based on their recommendations.

Plans for dissemination: There will be no proceedings, we will make the abstract and slides video publicly available at the website. If authors additionally pre-record a video, it will be distributed among the participants.

Contact

For any questions related to the workshop, the preferred solution to contact the organizers is to send an email to mcw at modelcounting.org

Johannes Fichte and Markus Hecher
Technische Universität Wien
Institut für Logic and Computation 192-02
Forschungsbereich für Datenbanken und Artificial Intelligence
Favoritenstraße 9
A-1040 Wien, Austria

Kuldeep Meel
NUS Presidential Young Professor
School of Computing
National University of Singapore
15 Computing Dr, Singapore 117418