scholarly journals ADDMC: Weighted Model Counting with Algebraic Decision Diagrams

2020 ◽  
Vol 34 (02) ◽  
pp. 1468-1476
Author(s):  
Jeffrey Dudek ◽  
Vu Phan ◽  
Moshe Vardi
Keyword(s):  
Dynamic Programming ◽  
Data Structure ◽  
Normal Form ◽  
Standard Model ◽  
State Of The Art ◽  
Conjunctive Normal Form ◽  
Decision Diagrams ◽  
Boolean Formulas ◽  
Model Counting ◽  
Weighted Model

We present an algorithm to compute exact literal-weighted model counts of Boolean formulas in Conjunctive Normal Form. Our algorithm employs dynamic programming and uses Algebraic Decision Diagrams as the main data structure. We implement this technique in ADDMC, a new model counter. We empirically evaluate various heuristics that can be used with ADDMC. We then compare ADDMC to four state-of-the-art weighted model counters (Cachet, c2d, d4, and miniC2D) on 1914 standard model counting benchmarks and show that ADDMC significantly improves the virtual best solver.

scholarly journals Clause/Term Resolution and Learning in the Evaluation of Quantified Boolean Formulas

2006 ◽  
Vol 26 ◽  
pp. 371-416 ◽  
Author(s):  
E. Giunchiglia ◽  
M. Narizzano ◽  
A. Tacchella
Keyword(s):  
Normal Form ◽  
Automated Reasoning ◽  
Comparative Evaluation ◽  
State Of The Art ◽  
Conjunctive Normal Form ◽  
Disjunctive Normal Form ◽  
Propositional Satisfiability ◽  
Quantified Boolean Formulas ◽  
Boolean Formulas ◽  
Input Formula

Resolution is the rule of inference at the basis of most procedures for automated reasoning. In these procedures, the input formula is first translated into an equisatisfiable formula in conjunctive normal form (CNF) and then represented as a set of clauses. Deduction starts by inferring new clauses by resolution, and goes on until the empty clause is generated or satisfiability of the set of clauses is proven, e.g., because no new clauses can be generated. In this paper, we restrict our attention to the problem of evaluating Quantified Boolean Formulas (QBFs). In this setting, the above outlined deduction process is known to be sound and complete if given a formula in CNF and if a form of resolution, called ``Q-resolution'', is used. We introduce Q-resolution on terms, to be used for formulas in disjunctive normal form. We show that the computation performed by most of the available procedures for QBFs --based on the Davis-Logemann-Loveland procedure (DLL) for propositional satisfiability-- corresponds to a tree in which Q-resolution on terms and clauses alternate. This poses the theoretical bases for the introduction of learning, corresponding to recording Q-resolution formulas associated with the nodes of the tree. We discuss the problems related to the introduction of learning in DLL based procedures, and present solutions extending state-of-the-art proposals coming from the literature on propositional satisfiability. Finally, we show that our DLL based solver extended with learning, performs significantly better on benchmarks used in the 2003 QBF solvers comparative evaluation.

METHODS OF REDUCING OF LARGE BOOLEAN FORMULAS REPRESENTED IN A CONJUNCTIVE NORMAL FORM FOR DETERMINING THEIR SATISFIABILITY

2020 ◽  
Author(s):  
N.I. Gdansky ◽  
◽  
A.A. Denisov ◽  
Keyword(s):  
Normal Form ◽  
Normal Forms ◽  
Conjunctive Normal Form ◽  
Boolean Formulas

The article explores the satisfiability of conjunctive normal forms used in modeling systems.The problems of CNF preprocessing are considered.The analysis of particular methods for reducing this formulas, which have polynomial input complexity is given.

Suffix array for multi-pattern matching with variable length wildcards

2021 ◽  
Vol 25 (2) ◽  
pp. 283-303
Author(s):  
Na Liu ◽  
Fei Xie ◽  
Xindong Wu
Keyword(s):  
Dynamic Programming ◽  
Data Structure ◽  
Pattern Matching ◽  
Edit Distance ◽  
State Of The Art ◽  
Suffix Array ◽  
Variable Length ◽  
Distance Method ◽  
Efficient Data ◽  
Comparison Algorithms

Approximate multi-pattern matching is an important issue that is widely and frequently utilized, when the pattern contains variable-length wildcards. In this paper, two suffix array-based algorithms have been proposed to solve this problem. Suffix array is an efficient data structure for exact string matching in existing studies, as well as for approximate pattern matching and multi-pattern matching. An algorithm called MMSA-S is for the short exact characters in a pattern by dynamic programming, while another algorithm called MMSA-L deals with the long exact characters by the edit distance method. Experimental results of Pizza & Chili corpus demonstrate that these two newly proposed algorithms, in most cases, are more time-efficient than the state-of-the-art comparison algorithms.

NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability

2020 ◽  
Vol 30 (7) ◽  
pp. 736-751
Author(s):  
Hans Kleine Büning ◽  
P. Wojciechowski ◽  
K. Subramani
Keyword(s):  
Normal Form ◽  
Conjunctive Normal Form ◽  
Principal Result ◽  
Satisfying Assignment ◽  
Boolean Formulas ◽  
Complete Procedure ◽  
Np Complete ◽  
Resolution Refutation ◽  
Original Formula ◽  
Cnf Formulas

AbstractIn this paper, we analyze Boolean formulas in conjunctive normal form (CNF) from the perspective of read-once resolution (ROR) refutation schemes. A read-once (resolution) refutation is one in which each clause is used at most once. Derived clauses can be used as many times as they are deduced. However, clauses in the original formula can only be used as part of one derivation. It is well known that ROR is not complete; that is, there exist unsatisfiable formulas for which no ROR exists. Likewise, the problem of checking if a 3CNF formula has a read-once refutation is NP-complete. This paper is concerned with a variant of satisfiability called not-all-equal satisfiability (NAE-satisfiability). A CNF formula is NAE-satisfiable if it has a satisfying assignment in which at least one literal in each clause is set to false. It is well known that the problem of checking NAE-satisfiability is NP-complete. Clearly, the class of CNF formulas which are NAE-satisfiable is a proper subset of satisfiable CNF formulas. It follows that traditional resolution cannot always find a proof of NAE-unsatisfiability. Thus, traditional resolution is not a sound procedure for checking NAE-satisfiability. In this paper, we introduce a variant of resolution called NAE-resolution which is a sound and complete procedure for checking NAE-satisfiability in CNF formulas. The focus of this paper is on a variant of NAE-resolution called read-once NAE-resolution in which each clause (input or derived) can be part of at most one NAE-resolution step. Our principal result is that read-once NAE-resolution is a sound and complete procedure for 2CNF formulas. Furthermore, we provide an algorithm to determine the smallest such NAE-resolution in polynomial time. This is in stark contrast to the corresponding problem concerning 2CNF formulas and ROR refutations. We also show that the problem of checking whether a 3CNF formula has a read-once NAE-resolution is NP-complete.

Model Counting of Monotone Conjunctive Normal Form Formulas with Spectra

2015 ◽  
Vol 27 (2) ◽  
pp. 406-415 ◽  
Author(s):  
Radislav Vaisman ◽  
Ofer Strichman ◽  
Ilya Gertsbakh
Keyword(s):  
Normal Form ◽  
Conjunctive Normal Form ◽  
Model Counting

scholarly journals The Model Counting Competition 2020

2021 ◽  
Vol 26 (1) ◽  
pp. 1-26
Author(s):  
Johannes K. Fichte ◽  
Markus Hecher ◽  
Florim Hamiti
Keyword(s):  
Practical Problem ◽  
Probabilistic Reasoning ◽  
Modern Society ◽  
Boolean Formula ◽  
Counting Problem ◽  
The Past ◽  
Boolean Formulas ◽  
Model Counting ◽  
Weighted Model ◽  
New Applications

Many computational problems in modern society account to probabilistic reasoning, statistics, and combinatorics. A variety of these real-world questions can be solved by representing the question in (Boolean) formulas and associating the number of models of the formula directly with the answer to the question. Since there has been an increasing interest in practical problem solving for model counting over the past years, the Model Counting Competition was conceived in fall 2019. The competition aims to foster applications, identify new challenging benchmarks, and promote new solvers and improve established solvers for the model counting problem and versions thereof. We hope that the results can be a good indicator of the current feasibility of model counting and spark many new applications. In this article, we report on details of the Model Counting Competition 2020, about carrying out the competition, and the results. The competition encompassed three versions of the model counting problem, which we evaluated in separate tracks. The first track featured the model counting problem, which asks for the number of models of a given Boolean formula. On the second track, we challenged developers to submit programs that solve the weighted model counting problem. The last track was dedicated to projected model counting. In total, we received a surprising number of nine solvers in 34 versions from eight groups.

scholarly journals Compressing Exact Cover Problems with Zero-suppressed Binary Decision Diagrams

2021 ◽  
Author(s):  
Masaaki Nishino ◽  
Norihito Yasuda ◽  
Kengo Nakamura
Keyword(s):  
Data Structure ◽  
State Of The Art ◽  
Linear Time ◽  
Binary Decision Diagrams ◽  
Experimental Results ◽  
Decision Diagrams ◽  
Binary Decision ◽  
Running Time ◽  
Order Of Magnitude ◽  
Exact Cover

Exact cover refers to the problem of finding subfamily F of a given family of sets S whose universe is D, where F forms a partition of D. Knuth’s Algorithm DLX is a state-of-the-art method for solving exact cover problems. Since DLX’s running time depends on the cardinality of input S, it can be slow if S is large. Our proposal can improve DLX by exploiting a novel data structure, DanceDD, which extends the zero-suppressed binary decision diagram (ZDD) by adding links to enable efficient modifications of the data structure. With DanceDD, we can represent S in a compressed way and perform search in linear time with the size of the structure by using link operations. The experimental results show that our method is an order of magnitude faster when the problem is highly compressed.

scholarly journals A Cardinal Improvement to Pseudo-Boolean Solving

2020 ◽  
Vol 34 (02) ◽  
pp. 1495-1503
Author(s):  
Jan Elffers ◽  
Jakob Nordstr”m
Keyword(s):  
Normal Form ◽  
Building Blocks ◽  
Conjunctive Normal Form ◽  
Conflict Analysis ◽  
Cardinality Constraints ◽  
Sat Solvers ◽  
Boolean Formulas ◽  
Clause Learning

Pseudo-Boolean solvers hold out the theoretical potential of exponential improvements over conflict-driven clause learning (CDCL) SAT solvers, but in practice perform very poorly if the input is given in the standard conjunctive normal form (CNF) format. We present a technique to remedy this problem by recovering cardinality constraints from CNF on the fly during search. This is done by collecting potential building blocks of cardinality constraints during propagation and combining these blocks during conflict analysis. Our implementation has a non-negligible but manageable overhead when detection is not successful, and yields significant gains for some SAT competition and crafted benchmarks for which pseudo-Boolean reasoning is stronger than CDCL. It also boosts performance for some native pseudo-Boolean formulas where this approach helps to improve learned constraints.

scholarly journals Extended Conjunctive Normal Form and An Efficient Algorithm for Cardinality Constraints

2020 ◽  
Author(s):  
Zhendong Lei ◽  
Shaowei Cai ◽  
Chuan Luo
Keyword(s):  
Normal Form ◽  
Local Search ◽  
State Of The Art ◽  
Scoring Function ◽  
Conjunctive Normal Form ◽  
Discrete Tomography ◽  
Cardinality Constraint ◽  
Cardinality Constraints ◽  
Important Constraint ◽  
Unit Propagation

Satisfiability (SAT) and Maximum Satisfiability (MaxSAT) are two basic and important constraint problems with many important applications. SAT and MaxSAT are expressed in CNF, which is difficult to deal with cardinality constraints. In this paper, we introduce Extended Conjunctive Normal Form (ECNF), which expresses cardinality constraints straightforward and does not need auxiliary variables or clauses. Then, we develop a simple and efficient local search solver LS-ECNF with a well designed scoring function under ECNF. We also develop a generalized Unit Propagation (UP) based algorithm to generate the initial solution for local search. We encode instances from Nurse Rostering and Discrete Tomography Problems into CNF with three different cardinality constraint encodings and ECNF respectively. Experimental results show that LS-ECNF has much better performance than state of the art MaxSAT, SAT, Pseudo-Boolean and ILP solvers, which indicates solving cardinality constraints with ECNF is promising.

Sign in / Sign up

Export Citation Format

Share Document