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 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.

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 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.

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

scholarly journals Learning to Reason: Leveraging Neural Networks for Approximate DNF Counting

2020 ◽  
Vol 34 (04) ◽  
pp. 3097-3104
Author(s):  
Ralph Abboud ◽  
Ismail Ceylan ◽  
Thomas Lukasiewicz
Keyword(s):  
Neural Networks ◽  
Large Scale ◽  
Linear Time ◽  
Neural Model ◽  
Approximate Model ◽  
Counting Approach ◽  
Model Counting ◽  
Weighted Model ◽  
Learning To Reason ◽  
Special Case

Weighted model counting (WMC) has emerged as a prevalent approach for probabilistic inference. In its most general form, WMC is #P-hard. Weighted DNF counting (weighted #DNF) is a special case, where approximations with probabilistic guarantees are obtained in O(nm), where n denotes the number of variables, and m the number of clauses of the input DNF, but this is not scalable in practice. In this paper, we propose a neural model counting approach for weighted #DNF that combines approximate model counting with deep learning, and accurately approximates model counts in linear time when width is bounded. We conduct experiments to validate our method, and show that our model learns and generalizes very well to large-scale #DNF instances.

scholarly journals Learning the Metric of Task Constraint Manifolds for Constrained Motion Planning

Electronics ◽  
2018 ◽  
Vol 7 (12) ◽  
pp. 395 ◽  
Author(s):  
Fusheng Zha ◽  
Yizhou Liu ◽  
Wei Guo ◽  
Pengfei Wang ◽  
Mantian Li ◽  
...  
Keyword(s):  
Motion Planning ◽  
Success Rate ◽  
Configuration Space ◽  
Fundamental Problem ◽  
Approximate Model ◽  
High Dimensional ◽  
Constrained Motion ◽  
Task Constraint ◽  
Task Constraints ◽  
Planning Methods

Finding feasible motion for robots with high-dimensional configuration space is a fundamental problem in robotics. Sampling-based motion planning algorithms have been shown to be effective for these high-dimensional systems. However, robots are often subject to task constraints (e.g., keeping a glass of water upright, opening doors and coordinating operation with dual manipulators), which introduce significant challenges to sampling-based motion planners. In this work, we introduce a method to establish approximate model for constraint manifolds, and to compute an approximate metric for constraint manifolds. The manifold metric is combined with motion planning methods based on projection operations, which greatly improves the efficiency and success rate of motion planning tasks under constraints. The proposed method Approximate Graph-based Constrained Bi-direction Rapidly Exploring Tree (AG-CBiRRT), which improves upon CBiRRT, and CBiRRT were tested on several task constraints, highlighting the benefits of our approach for constrained motion planning tasks.

scholarly journals Approximate Weighted First-Order Model Counting: Exploiting Fast Approximate Model Counters and Symmetry

2020 ◽  
Author(s):  
Timothy van Bremen ◽  
Ondrej Kuzelka
Keyword(s):  
Probabilistic Models ◽  
Approximate Model ◽  
Probabilistic Logic ◽  
Markov Logic Networks ◽  
Order Model ◽  
Cardinality Constraints ◽  
Markov Logic ◽  
First Order ◽  
Model Counting ◽  
Input Sentence

We study the symmetric weighted first-order model counting task and present ApproxWFOMC, a novel anytime method for efficiently bounding the weighted first-order model count of a sentence given an unweighted first-order model counting oracle. The algorithm has applications to inference in a variety of first-order probabilistic representations, such as Markov logic networks and probabilistic logic programs. Crucially for many applications, no assumptions are made on the form of the input sentence. Instead, the algorithm makes use of the symmetry inherent in the problem by imposing cardinality constraints on the number of possible true groundings of a sentence's literals. Realising the first-order model counting oracle in practice using the approximate hashing-based model counter ApproxMC3, we show how our algorithm is competitive with existing approximate and exact techniques for inference in first-order probabilistic models. We additionally provide PAC guarantees on the accuracy of the bounds generated.

Sign in / Sign up

Export Citation Format

Share Document