Chapter 26. Approximate Model Counting

2021 ◽  
Author(s):  
Supratik Chakraborty ◽  
Kuldeep S. Meel ◽  
Moshe Y. Vardi
Keyword(s):  
Fundamental Problem ◽  
Scale Up ◽  
Approximate Model ◽  
Approximate Counting ◽  
Universal Hashing ◽  
Exact Counting ◽  
Model Counting ◽  
Satisfiability Solving ◽  
Problem Instances ◽  
Counting Solutions

Model counting, or counting solutions of a set of constraints, is a fundamental problem in Computer Science with diverse applications. Since exact counting is computationally hard (#P complete), approximate counting techniques have received much attention over the past few decades. In this chapter, we focus on counting models of propositional formulas, and discuss in detail universal-hashing based approximate counting, which has emerged as the predominant paradigm for state-of-the-art approximate model counters. These counters are randomized algorithms that exploit properties of universal hash functions to provide rigorous approximation guarantees, while piggybacking on impressive advances in propositional satisfiability solving to scale up to problem instances with a million variables. We elaborate on various choices in designing such approximate counters and the implications of these choices. We also discuss variants of approximate model counting, such as DNF counting and weighted counting.

scholarly journals GANAK: A Scalable Probabilistic Exact Model Counter

2019 ◽  
Author(s):  
Shubham Sharma ◽  
Subhajit Roy ◽  
Mate Soos ◽  
Kuldeep S. Meel
Keyword(s):  
Probabilistic Reasoning ◽  
State Of The Art ◽  
Fundamental Problem ◽  
Approximate Model ◽  
Boolean Formula ◽  
Sat Solvers ◽  
Exact Model ◽  
Universal Hashing ◽  
Model Counting ◽  
Dynamic Decomposition

Given a Boolean formula F, the problem of model counting, also referred to as #SAT, seeks to compute the number of solutions of F. Model counting is a fundamental problem with a wide variety of applications ranging from planning, quantified information flow to probabilistic reasoning and the like. The modern #SAT solvers tend to be either based on static decomposition, dynamic decomposition, or a hybrid of the two. Despite dynamic decomposition based #SAT solvers sharing much of their architecture with SAT solvers, the core design and heuristics of dynamic decomposition-based #SAT solvers has remained constant for over a decade. In this paper, we revisit the architecture of the state-of-the-art dynamic decomposition-based #SAT tool, sharpSAT, and demonstrate that by introducing a new notion of probabilistic component caching and the usage of universal hashing for exact model counting along with the development of several new heuristics can lead to significant performance improvement over state-of-the-art model-counters. In particular, we develop GANAK, a new scalable probabilistic exact model counter that outperforms state-of-the-art exact and approximate model counters sharpSAT and ApproxMC3 respectively, both in terms of PAR-2 score and the number of instances solved. Furthermore, in our experiments, the model count returned by GANAK was equal to the exact model count for all the benchmarks. Finally, we observe that recently proposed preprocessing techniques for model counting benefit exact model counters while hurting the performance of approximate model counters.

Gaussian Elimination Meets Maximum Satisfiability

2021 ◽  
Author(s):  
Mate Soos ◽  
Kuldeep S. Meel
Keyword(s):  
Weight Function ◽  
Network Reliability ◽  
Fundamental Problem ◽  
Gaussian Elimination ◽  
Approximate Model ◽  
Maximum Satisfiability ◽  
Practical Evaluation ◽  
Model Counting ◽  
Primary Contribution ◽  
Discrete Integration

Given a set of constraints F and a weight function W over the assignments, the problem of MaxSAT is to compute a maximum weighted solution of F. MaxSAT is a fundamental problem with applications in numerous areas. The success of MaxSAT solvers has prompted researchers in AI and formal methods communities to develop algorithms that can use MaxSAT solver as oracle. One such problem that stands to benefit from advances in MaxSAT solving is discrete integration. Recently, Ermon et al. achieved a significant breakthrough by reducing the problem of integration to polynomially many queries to an optimization oracle where $F$ is conjuncted with randomly chosen XOR constraints. Unlike approximate model counting, where hashing-based approaches have been able to achieve scalability as well as rigorous formal guarantees, the practical evaluation of Ermon et al's approach, called WISH, often sacrifice theoretical guarantees, largely due to lack of existing MaxSAT solvers with native XOR support. The primary contribution of this paper is a new MaxSAT solver, GaussMaxHS, with built-in XOR support. The architecture of GaussMaxHS is inspired by CryptoMiniSAT, which has been the workhorse of hashing-based approximate model counting techniques. The resulting solver, GaussMaxHS, outperforms MaxHS over 9628 benchmarks arising from spin glass models and network reliability domains. In particular, with a timeout of 5000 seconds, MaxHS could solve only 5473 benchmarks while GaussMaxHS could solve 6120 benchmarks.

scholarly journals BIRD: Engineering an Efficient CNF-XOR SAT Solver and Its Applications to Approximate Model Counting

2019 ◽  
Vol 33 ◽  
pp. 1592-1599 ◽  
Author(s):  
Mate Soos ◽  
Kuldeep S. Meel
Keyword(s):  
Probabilistic Reasoning ◽  
State Of The Art ◽  
Fundamental Problem ◽  
Approximate Model ◽  
Affirmative Answer ◽  
The State ◽  
Boolean Formula ◽  
Wide Range ◽  
Model Counting ◽  
Sat Solver

Given a Boolean formula φ, the problem of model counting, also referred to as #SAT is to compute the number of solutions of φ. Model counting is a fundamental problem in artificial intelligence with a wide range of applications including probabilistic reasoning, decision making under uncertainty, quantified information flow, and the like. Motivated by the success of SAT solvers, there has been surge of interest in the design of hashing-based techniques for approximate model counting for the past decade. We profiled the state of the art approximate model counter ApproxMC2 and observed that over 99.99% of time is consumed by the underlying SAT solver, CryptoMiniSat. This observation motivated us to ask: Can we design an efficient underlying CNF-XOR SAT solver that can take advantage of the structure of hashing-based algorithms and would this lead to an efficient approximate model counter? The primary contribution of this paper is an affirmative answer to the above question. We present a novel architecture, called BIRD, to handle CNF-XOR formulas arising from hashingbased techniques. The resulting hashing-based approximate model counter, called ApproxMC3, employs the BIRD framework in its underlying SAT solver, CryptoMiniSat. To the best of our knowledge, we conducted the most comprehensive study of evaluation performance of counting algorithms involving 1896 benchmarks with computational effort totaling 86400 computational hours. Our experimental evaluation demonstrates significant runtime performance improvement for ApproxMC3 over ApproxMC2. In particular, we solve 648 benchmarks more than ApproxMC2, the state of the art approximate model counter and for all the formulas where both ApproxMC2 and ApproxMC3 did not timeout and took more than 1 seconds, the mean speedup is 284.40 – more than two orders of magnitude.

Approximate Model Counting Via Extension Rule and Clause Reduction

2018 ◽  
Author(s):  
Hao Liu ◽  
Ziao Ni ◽  
Wenyang Zhou ◽  
Tongbo Zhang ◽  
Shuai Lü
Keyword(s):  
Approximate Model ◽  
Extension Rule ◽  
Model Counting

Hybrid Evolutionary Optimization of Two-Stage Stochastic Integer Programming Problems: An Empirical Investigation

2009 ◽  
Vol 17 (4) ◽  
pp. 511-526 ◽  
Author(s):  
Thomas Tometzki ◽  
Sebastian Engell
Keyword(s):  
Evolutionary Algorithm ◽  
Empirical Investigation ◽  
Scale Up ◽  
Exact Algorithm ◽  
Integer Program ◽  
Mixed Integer ◽  
Two Stage ◽  
Integer Programming Problems ◽  
Problem Instances ◽  
Feasible Solutions

In this contribution, we consider decision problems on a moving horizon with significant uncertainties in parameters. The information and decision structure on moving horizons enables recourse actions which correct the here-and-now decisions whenever the horizon is moved a step forward. This situation is reflected by a mixed-integer recourse model with a finite number of uncertainty scenarios in the form of a two-stage stochastic integer program. A stage decomposition-based hybrid evolutionary algorithm for two-stage stochastic integer programs is proposed that employs an evolutionary algorithm to determine the here-and-now decisions and a standard mathematical programming method to optimize the recourse decisions. An empirical investigation of the scale-up behavior of the algorithms with respect to the number of scenarios exhibits that the new hybrid algorithm generates good feasible solutions more quickly than a state of the art exact algorithm for problem instances with a high number of scenarios.

scholarly journals A New Probabilistic Algorithm for Approximate Model Counting

2018 ◽  
pp. 312-328
Author(s):  
Cunjing Ge ◽  
Feifei Ma ◽  
Tian Liu ◽  
Jian Zhang ◽  
Xutong Ma
Keyword(s):  
Approximate Model ◽  
Probabilistic Algorithm ◽  
Model Counting

Approximate Model Counting via Extension Rule

2015 ◽  
pp. 229-240
Author(s):  
Jinyan Wang ◽  
Minghao Yin ◽  
Jingli Wu
Keyword(s):  
Approximate Model ◽  
Extension Rule ◽  
Model Counting

Nanoporous Silica for Low κ Dielectrics

1997 ◽  
Vol 495 ◽  
Author(s):  
Teresa Ramos ◽  
Steve Wallace ◽  
Douglas M. Smith
Keyword(s):  
Dielectric Constant ◽  
Integrated Circuit ◽  
Dielectric Material ◽  
Fundamental Problem ◽  
Scale Up ◽  
Current Status ◽  
Nanoporous Silica ◽  
Interconnect Delay ◽  
Small Pore ◽  
Deposition Processes

ABSTRACTAs integrated circuit sizes decrease below 0.25 microns, device performance will no longer improve at the same rate as for past generations because of RC interconnect delay which becomes significant as compared to the intrinsic gate delay. The parallel approaches to partially address this fundamental problem are to use a lower resistance metal (i.e., copper instead of aluminum) and to use a dielectric material with a dielectric constant significantly below that of dense silica (∼4). Recently, considerable progress has been made in development of thin films of nanoporous silica (also known as aerogels or low density xerogels) for these ILD and IMD applications. Advantages of these materials include high thermal stability, small pore size, and similarity to conventional spin-on deposition processes, spin-on glass precursors and final material (silica). The dielectric constant of nanoporous silica can be tailored between ∼1 and 3 which allows its’ implementation at multiple technology nodes in integrated circuit manufacture starting with the 0.18 micron node.Research and development efforts at Nanoglass over the last several years have focused on; 1) simpler and more reproducible deposition processes, 2) a more complete understanding of processing-property relationships for this material, 3) scale-up of manufacturing to yield a range of precursor products with stability for at least six months and very high purity, and 4) working with customers to integrate this material into both aluminum/gapfill and copper/damascene process flows. Nanoglass has now developed a new process which considerably reduces the number of process steps and allows independent control of both film thickness and porosity. The current status of process and precursor development and device integration efforts for nanoporous silica is discussed.

scholarly journals On the Hardness of Probabilistic Inference Relaxations

2019 ◽  
Vol 33 ◽  
pp. 7785-7792
Author(s):  
Supratik Chakraborty ◽  
Kuldeep S. Meel ◽  
Moshe Y. Vardi
Keyword(s):  
Decision Making ◽  
Computational Efficiency ◽  
Probabilistic Inference ◽  
Approximation Error ◽  
Common Belief ◽  
Approximate Counting ◽  
Efficient Computation ◽  
Probability Estimates ◽  
Model Counting ◽  
Recent Attention

A promising approach to probabilistic inference that has attracted recent attention exploits its reduction to a set of model counting queries. Since probabilistic inference and model counting are #P-hard, various relaxations are used in practice, with the hope that these relaxations allow efficient computation while also providing rigorous approximation guarantees. In this paper, we show that contrary to common belief, several relaxations used for model counting and its applications (including probablistic inference) do not really lead to computational efficiency in a complexity theoretic sense. Our arguments proceed by showing the corresponding relaxed notions of counting to be computationally hard. We argue that approximate counting with multiplicative tolerance and probabilistic guarantees of correctness is the only class of relaxations that provably simplifies the problem, given access to an NP-oracle. Finally, we show that for applications that compare probability estimates with a threshold, a new notion of relaxation with gaps between low and high thresholds can be used. This new relaxation allows efficient decision making in practice, given access to an NP-oracle, while also bounding the approximation error.

Sign in / Sign up

Export Citation Format

Share Document