Compressing Exact Cover Problems with Zero-suppressed Binary Decision Diagrams

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.

Download Full-text

Non-clausal Redundancy Properties

Automated Deduction – CADE 28 - Lecture Notes in Computer Science ◽

10.1007/978-3-030-79876-5_15 ◽

2021 ◽

pp. 252-272

Author(s):

Lee A. Barnett ◽

Armin Biere

Keyword(s):

State Of The Art ◽

Binary Decision Diagrams ◽

Gaussian Elimination ◽

Decision Diagrams ◽

Binary Decision ◽

Refutation Systems ◽

Unit Propagation

AbstractState-of-the-art refutation systems for SAT are largely based on the derivation of clauses meeting some redundancy criteria, ensuring their addition to a formula does not alter its satisfiability. However, there are strong propositional reasoning techniques whose inferences are not easily expressed in such systems. This paper extends the redundancy framework beyond clauses to characterize redundancy for Boolean constraints in general. We show this characterization can be instantiated to develop efficiently checkable refutation systems using redundancy properties for Binary Decision Diagrams (BDDs). Using a form of reverse unit propagation over conjunctions of BDDs, these systems capture, for instance, Gaussian elimination reasoning over XOR constraints encoded in a formula, without the need for clausal translations or extension variables. Notably, these systems generalize those based on the strong Propagation Redundancy (PR) property, without an increase in complexity.

Download Full-text

Genetic algorithm for binary and functional decision diagrams optimization

Facta universitatis - series Electronics and Energetics ◽

10.2298/fuee1802169s ◽

2018 ◽

Vol 31 (2) ◽

pp. 169-187

Author(s):

Stojkovic Suzana ◽

Velickovic Darko ◽

Moraga Claudio

Keyword(s):

Genetic Algorithm ◽

Genetic Algorithms ◽

Data Structure ◽

Optimization Problems ◽

Binary Decision Diagrams ◽

Size Optimization ◽

Decision Diagrams ◽

Crossover Operator ◽

Binary Decision ◽

Discrete Functions

Decision diagrams (DD) are a widely used data structure for discrete functions representation. The major problem in DD-based applications is the DD size minimization (reduction of the number of nodes), because their size is dependent on the variables order. Genetic algorithms are often used in different optimization problems including the DD size optimization. In this paper, we apply the genetic algorithm to minimize the size of both Binary Decision Diagrams (BDDs) and Functional Decision Diagrams (FDDs). In both cases, in the proposed algorithm, a Bottom-Up Partially Matched Crossover (BU-PMX) is used as the crossover operator. In the case of BDDs, mutation is done in the standard way by variables exchanging. In the case of FDDs, the mutation by changing the polarity of variables is additionally used. Experimental results of optimization of the BDDs and FDDs of the set of benchmark functions are also presented.

Download Full-text

Linear algorithms for recognizing and parsing superpositional graphs

Facta universitatis - series Electronics and Energetics ◽

10.2298/fuee1103325p ◽

2011 ◽

Vol 24 (3) ◽

pp. 325-339 ◽

Cited By ~ 2

Author(s):

Ahti Peder ◽

Härmel Nestra ◽

Jaan Raik ◽

Mati Tombak ◽

Raimund Ubar

Keyword(s):

Test Generation ◽

Linear Time ◽

Binary Decision Diagrams ◽

Propositional Formula ◽

Decision Diagrams ◽

Binary Decision ◽

Proper Subclass ◽

History Of ◽

Linear Time Algorithms ◽

Linear Algorithms

Structurally synthesized binary decision diagrams (SSBDD) are a special type of BDDs that are generated by superposition according to the structure of propositional formula. Fast algorithms for simulation, diagnostic reasoning and test generation running on SSBDDs exploit their specific properties. Hence the correctness of SSBDDs should be checked before using those algorithms. The problem of recognizing SSBDDs can be reduced to the problem of recognizing their skeleton, namely superpositional graphs, which are a proper subclass of binary graphs. This paper presents linear time algorithms for testing whether a binary graph is a superpositional graph and for restoring the history of its generating process.

Download Full-text

Competitive Sorter-based Encoding of PB-Constraints into SAT

10.29007/hh3v ◽

2019 ◽

Cited By ~ 1

Author(s):

Michał Karpiński ◽

Marek Piotrów

Keyword(s):

Linear Inequality ◽

State Of The Art ◽

Binary Decision Diagrams ◽

Inequality Constraint ◽

Decision Diagrams ◽

Binary Decision ◽

System Description ◽

Sorting Networks ◽

Linear Inequality Constraint ◽

New Construction

A Pseudo-Boolean (PB) constraint is a linear inequality constraint over Boolean variables. A popular idea to solve PB-constraints is to transform them to CNFs (via BDDs, adders and sorting networks [5, 11]) and process them using – increasingly improving – state-of-the-art SAT-solvers. Recent research have favored the approach that uses Binary Decision Diagrams (BDDs), which is evidenced by several new constructions and optimizations [2, 21]. We show that encodings based on comparator networks can still be very competitive. We present a system description of a PB-solver based on MiniSat+ [11] which we extended by adding a new construction of selection network called 4-Way Merge Selection Network, with a few optimizations based on other solvers. Experiments show that on many instances of popular benchmarks our technique outperforms other state-of-the-art PB-solvers.

Download Full-text