Chapter 27. Non-Clausal SAT and ATPG

2021 ◽  
Author(s):  
Rolf Drechsler ◽  
Tommi Junttila ◽  
Ilkka Niemelä
Keyword(s):  
General Formula ◽  
Survey Methods ◽  
Conjunctive Normal Form ◽  
Pattern Generation ◽  
Propositional Satisfiability ◽  
Propositional Formula ◽  
Related Area ◽  
Sat Solvers ◽  
Negative Effect ◽  
Efficient Data

When studying the propositional satisfiability problem (SAT), that is, the problem of deciding whether a propositional formula is satisfiable, it is typically assumed that the formula is given in the conjunctive normal form (CNF). Also most software tools for deciding satisfiability of a formula (SAT solvers) assume that their input is in CNF. An important reason for this is that it is simpler to develop efficient data structures and algorithms for CNF than for arbitrary formulas. On the other hand, using CNF makes efficient modeling of an application cumbersome. Therefore one often employs a more general formula representation in modeling and then transforms the formula into CNF for SAT solvers. Transforming a propositional formula in CNF either increases the formula size exponentially or requires the use of auxiliary variables, which can have an negative effect on the performance of a SAT solver in the worst-case. Moreover, by translating to CNF one often loses information about the structure of the original problem. In this chapter we survey methods for solving propositional satisfiability problems when the input formula is not given in CNF but as a general formula or even more compactly as a Boolean circuit. We show how the techniques applied in CNF level Davis-Putnam-Loveland-Logemann algorithm generalize to Boolean circuits and how the problem structure available in the circuit form can be exploited. Then we consider a closely related area of automatic test pattern generation (ATPG) for digital circuits and review classical ATPG algorithms, formulation of ATPG as a SAT problem, and advanced techniques for SAT-based ATPG.

Chapter 13. Symmetry and Satisfiability

2021 ◽  
Author(s):  
Karem A. Sakallah
Keyword(s):  
Group Theory ◽  
Normal Form ◽  
Boolean Functions ◽  
Search Algorithm ◽  
Conjunctive Normal Form ◽  
Search Space ◽  
Decision Problems ◽  
Mathematical Language ◽  
Sat Solvers ◽  
Speed Up

Symmetry is at once a familiar concept (we recognize it when we see it!) and a profoundly deep mathematical subject. At its most basic, a symmetry is some transformation of an object that leaves the object (or some aspect of the object) unchanged. For example, a square can be transformed in eight different ways that leave it looking exactly the same: the identity “do-nothing” transformation, 3 rotations, and 4 mirror images (or reflections). In the context of decision problems, the presence of symmetries in a problem’s search space can frustrate the hunt for a solution by forcing a search algorithm to fruitlessly explore symmetric subspaces that do not contain solutions. Recognizing that such symmetries exist, we can direct a search algorithm to look for solutions only in non-symmetric parts of the search space. In many cases, this can lead to significant pruning of the search space and yield solutions to problems which are otherwise intractable. This chapter explores the symmetries of Boolean functions, particularly the symmetries of their conjunctive normal form (CNF) representations. Specifically, it examines what those symmetries are, how to model them using the mathematical language of group theory, how to derive them from a CNF formula, and how to utilize them to speed up CNF SAT solvers.

scholarly journals FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints

2020 ◽  
Vol 34 (02) ◽  
pp. 1552-1560
Author(s):  
Anastasios Kyrillidis ◽  
Anshumali Shrivastava ◽  
Moshe Vardi ◽  
Zhiwei Zhang
Keyword(s):  
Boolean Functions ◽  
Continuous Optimization ◽  
Conjunctive Normal Form ◽  
Cardinality Constraints ◽  
Sat Solvers ◽  
Boolean Satisfiability Problem ◽  
Algebraic Framework ◽  
Clause Learning ◽  
Sat Solver ◽  
Analysis Of Boolean Functions

The Boolean SATisfiability problem (SAT) is of central importance in computer science. Although SAT is known to be NP-complete, progress on the engineering side—especially that of Conflict-Driven Clause Learning (CDCL) and Local Search SAT solvers—has been remarkable. Yet, while SAT solvers, aimed at solving industrial-scale benchmarks in Conjunctive Normal Form (CNF), have become quite mature, SAT solvers that are effective on other types of constraints (e.g., cardinality constraints and XORs) are less well-studied; a general approach to handling non-CNF constraints is still lacking. In addition, previous work indicated that for specific classes of benchmarks, the running time of extant SAT solvers depends heavily on properties of the formula and details of encoding, instead of the scale of the benchmarks, which adds uncertainty to expectations of running time.To address the issues above, we design FourierSAT, an incomplete SAT solver based on Fourier analysis of Boolean functions, a technique to represent Boolean functions by multilinear polynomials. By such a reduction to continuous optimization, we propose an algebraic framework for solving systems consisting of different types of constraints. The idea is to leverage gradient information to guide the search process in the direction of local improvements. Empirical results demonstrate that FourierSAT is more robust than other solvers on certain classes of benchmarks.

scholarly journals Satisfiability and Computing van der Waerden Numbers

10.37236/1794 ◽  
2004 ◽  
Vol 11 (1) ◽  
Author(s):  
Michael R. Dransfield ◽  
Lengning Liu ◽  
Victor W. Marek ◽  
Mirosław Truszczyński
Keyword(s):  
Positive Integer ◽  
Local Search ◽  
Ramsey Theory ◽  
Upper Bounds ◽  
General Purpose ◽  
Propositional Satisfiability ◽  
Lower And Upper Bounds ◽  
Algebraic Form ◽  
Sat Solvers ◽  
Structural Simplicity

In this paper we bring together the areas of combinatorics and propositional satisfiability. Many combinatorial theorems establish, often constructively, the existence of positive integer functions, without actually providing their closed algebraic form or tight lower and upper bounds. The area of Ramsey theory is especially rich in such results. Using the problem of computing van der Waerden numbers as an example, we show that these problems can be represented by parameterized propositional theories in such a way that decisions concerning their satisfiability determine the numbers (function) in question. We show that by using general-purpose complete and local-search techniques for testing propositional satisfiability, this approach becomes effective — competitive with specialized approaches. By following it, we were able to obtain several new results pertaining to the problem of computing van der Waerden numbers. We also note that due to their properties, especially their structural simplicity and computational hardness, propositional theories that arise in this research can be of use in development, testing and benchmarking of SAT solvers.

SOLVING INCREMENTAL SATISFIABILITY

2007 ◽  
Vol 16 (01) ◽  
pp. 139-147 ◽  
Author(s):  
MALEK MOUHOUB ◽  
SAMIRA SADAOUI
Keyword(s):  
Branch And Bound ◽  
Experimental Tests ◽  
Combinatorial Problems ◽  
Propositional Satisfiability ◽  
Propositional Formula ◽  
Stochastic Local Search ◽  
Approximation Methods ◽  
Sat Problem ◽  
Complete Problems

Propositional satisfiability (SAT) problem is fundamental to the theory of NP-completeness. Indeed, using the concept of "polynomial-time reducibility" all NP-complete problems can be polynomially reduced to SAT. Thus, any new technique for satisfiability problems will lead to general approaches for thousands of hard combinatorial problems. In this paper, we introduce the incremental propositional satisfiability problem that consists of maintaining the satisfiability of a propositional formula anytime a conjunction of new clauses is added. More precisely, the goal here is to check whether a solution to a SAT problem continues to be a solution anytime a new set of clauses is added and if not, whether the solution can be modified efficiently to satisfy the old formula and the new clauses. We will study the applicability of systematic and approximation methods for solving incremental SAT problems. The systematic method is based on the branch and bound technique while the approximation methods rely on stochastic local search and genetic algorithms. Experimental tests, conducted on randomly generated SAT instances, demonstrate the efficiency in time of the approximation methods over the branch and bound algorithm. However these approximation methods do not always guarantee the completeness of the solution returned. We show that a method we propose that uses non systematic search in a limited form together with branch and bound has the best compromise, in practice, between time and quality of the solution returned (success ratio).

Conflict-Driven Learning in Test Pattern Generation

2011 ◽  
Vol 301-303 ◽  
pp. 1089-1092
Author(s):  
Xin Liu
Keyword(s):  
Test Pattern ◽  
Level Structure ◽  
Conjunctive Normal Form ◽  
Search Space ◽  
Pattern Generation ◽  
Test Pattern Generation ◽  
Heuristic Learning ◽  
Fundamental Cause ◽  
Reconvergent Fanout ◽  
High Level

SAT-based automatic test pattern generation (ATPG) is built on a SAT-solver, which can be scalable is that it is able to take into account the information of high-level structure of formulas. Paper analyzes specific structure of circuit instances where correlations among signals have been established. This analysis is a heuristic learning method by earlier detecting assignment conflicts. Reconvergent fanout is a fundamental cause of the difficulty in testing generation, because they introduce dependencies in the values that can be assigned to nodes. Paper exploits reconvergent fanout analysis of circuit to gather information about local signal correlation through BDD learning, and then used the learned information in the conjunctive normal form (CNF) clauses to restrict and focus the overall search space of test pattern generation. The experimental results demonstrate the effectiveness of these learning techniques.

SAT-Based Data Mining

2018 ◽  
Vol 27 (01) ◽  
pp. 1840002
Author(s):  
Abdelhamid Boudane ◽  
Saïd Jabbour ◽  
Lakhdar Sais ◽  
Yakoub Salhi
Keyword(s):  
Data Mining ◽  
Propositional Satisfiability ◽  
Propositional Formula ◽  
Sequence Mining ◽  
Minimal Models ◽  
New Approach ◽  
Itemset Mining ◽  
Important Challenge ◽  
Single Formula ◽  
Frequent Closed Itemset

Several propositional satisfiability (SAT) based encodings have been proposed to deal with various data mining problems including itemset and sequence mining problems. This research issue allows to model data mining problems in a declarative way, while exploiting efficient SAT solving techniques. In this paper, we overview our contributions on the application of propositional satisfiability (SAT) to model and solve itemset mining tasks. We first present a SAT based encoding of frequent closed itemset mining task as a propositional formula whose models corresponds to the patterns to be mined. Secondly, we show that some data mining constraints can be avoided by reformulation. We illustrate this issue by reformulating the closeness constraint using the notion of minimal models. Finally, we also addressed the scalability issue, one of the most important challenge of these nice declarative framework. To this end, we proposed a complete partition based approach whose aim is to avoid encoding the whole database as a single formula. Using a partition on the set of items, our new approach leads to several propositional formulas of reasonable size. The experimental evaluation on several known datasets shows huge improvements in comparison to the direct approach without partitioning, while reducing significantly the performance gap with respect to specialized algorithms.

scholarly journals Generic CDCL -- A Formalization of Modern Propositional Satisfiability Solvers

10.29007/7n71 ◽  
2018 ◽  
Author(s):  
Steffen Hölldobler ◽  
Norbert Manthey ◽  
Tobias Philipp ◽  
Peter Steinke
Keyword(s):  
State Transition ◽  
Transition System ◽  
Propositional Satisfiability ◽  
Sat Solvers ◽  
Satisfiability Solvers ◽  
Recent Developments ◽  
Small Set ◽  
State Transition System ◽  
Combined Algorithm ◽  
Simplification Techniques

Modern propositional satisfiability (or SAT) solvers are very powerful due to recent developments on the underlying data structures, the used heuristics to guide the search, the deduction techniques to infer knowledge, and the formula simplification techniques that are used during pre- and inprocessing. However, when all these techniques are put together, the soundness of the combined algorithm is not guaranteed any more, and understanding the complex dependencies becomes non-trivial.In this paper we present a small set of rules that allows to model modern SAT solvers in terms of a state transition system. With these rules all techniques which are applied in modern SAT solvers can be modeled adequately. Furthermore, we show that this set of rules results is sound, complete and confluent. Finnaly, we compare the proposed transition system to related systems, and show how widely used solving techniques can be modeled.

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.

Sign in / Sign up

Export Citation Format

Share Document