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.

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 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 Efficient SAT-Based Encodings of Conditional Cardinality Constraints

10.29007/kfjb ◽  
2018 ◽  
Author(s):  
Abdelhamid Boudane ◽  
Said Jabbour ◽  
Badran Raddaoui ◽  
Lakhdar Sais
Keyword(s):  
Experimental Validation ◽  
Pattern Mining ◽  
Conjunctive Normal Form ◽  
Propositional Formula ◽  
Cardinality Constraint ◽  
Cardinality Constraints ◽  
Combinatorial Explosion ◽  
Arc Consistency ◽  
Consistency Property ◽  
Real World Problems

In the encoding of many real-world problems to propositional satisfiability, the cardinality constraint is a recurrent constraint that needs to be managed effectively. Several efficient encodings have been proposed while missing that such a constraint can be involved in a more general propositional formula. To avoid combinatorial explosion, the Tseitin principle usually used to translate such general propositional formula to Conjunctive Normal Form (CNF), introduces fresh propositional variables to represent sub-formulas and/or complex contraints. Thanks to Plaisted and Greenbaum improvement, the polarity of the sub-formula Φ is taken into account leading to conditional constraints of the form y → Φ, or Φ → y, where y is a fresh propositional variable. In the case where Φ represents a cardinality constraint, such translation leads to conditional cardinality constraints subject of the present paper. We first show that when all the clauses encoding the cardinality constraint are augmented with an additional new variable, most of the well-known encodings cease to maintain the generalized arc-consistency property. Then, we consider some of these encodings and show how they can be extended to recover such important property. An experimental validation is conducted on a SAT-based pattern mining application, where such conditional cardinality constraints are a cornerstone, showing the relevance of our proposed approach.

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.

scholarly journals Scoring Functions Based on Second Level Score for k-SAT with Long Clauses

2014 ◽  
Vol 51 ◽  
pp. 413-441 ◽  
Author(s):  
S. Cai ◽  
C. Luo ◽  
K. Su
Keyword(s):  
Phase Transition ◽  
Computational Complexity ◽  
Local Search ◽  
State Of The Art ◽  
Scoring Function ◽  
Experimental Results ◽  
Great Success ◽  
Stochastic Local Search ◽  
Scoring Functions ◽  
New Scoring

It is widely acknowledged that stochastic local search (SLS) algorithms can efficiently find models for satisfiable instances of the satisfiability (SAT) problem, especially for random k-SAT instances. However, compared to random 3-SAT instances where SLS algorithms have shown great success, random k-SAT instances with long clauses remain very difficult. Recently, the notion of second level score, denoted as "score_2", was proposed for improving SLS algorithms on long-clause SAT instances, and was first used in the powerful CCASat solver as a tie breaker. In this paper, we propose three new scoring functions based on score_2. Despite their simplicity, these functions are very effective for solving random k-SAT with long clauses. The first function combines score and score_2, and the second one additionally integrates the diversification property "age". These two functions are used in developing a new SLS algorithm called CScoreSAT. Experimental results on large random 5-SAT and 7-SAT instances near phase transition show that CScoreSAT significantly outperforms previous SLS solvers. However, CScoreSAT cannot rival its competitors on random k-SAT instances at phase transition. We improve CScoreSAT for such instances by another scoring function which combines score_2 with age. The resulting algorithm HScoreSAT exhibits state-of-the-art performance on random k-SAT (k>3) instances at phase transition. We also study the computation of score_2, including its implementation and computational complexity.

scholarly journals A Structural Entropy Measurement Principle of Propositional Formulas in Conjunctive Normal Form

Entropy ◽  
2021 ◽  
Vol 23 (3) ◽  
pp. 303
Author(s):  
Zaijun Zhang ◽  
Daoyun Xu ◽  
Jincheng Zhou
Keyword(s):  
Normal Form ◽  
Local Search ◽  
Structural Properties ◽  
Structural Characteristics ◽  
Complex Structure ◽  
Solution Process ◽  
Conjunctive Normal Form ◽  
Experimental Results ◽  
Entropy Measurement ◽  
Structural Entropy

The satisfiability (SAT) problem is a core problem in computer science. Existing studies have shown that most industrial SAT instances can be effectively solved by modern SAT solvers while random SAT instances cannot. It is believed that the structural characteristics of different SAT formula classes are the reasons behind this difference. In this paper, we study the structural properties of propositional formulas in conjunctive normal form (CNF) by the principle of structural entropy of formulas. First, we used structural entropy to measure the complex structure of a formula and found that the difficulty solving the formula is related to the structural entropy of the formula. The smaller the compressing information of a formula, the more difficult it is to solve the formula. Secondly, we proposed a λ-approximation strategy to approximate the structural entropy of large formulas. The experimental results showed that the proposed strategy can effectively approximate the structural entropy of the original formula and that the approximation ratio is more than 92%. Finally, we analyzed the structural properties of a formula in the solution process and found that a local search solver tends to select variables in different communities to perform the next round of searches during a search and that the structural entropy of a variable affects the probability of the variable being flipped. By using these conclusions, we also proposed an initial candidate solution generation strategy for a local search for SAT, and the experimental results showed that this strategy effectively improves the performance of the solvers CCAsat and Sparrow2011 when incorporated into these two solvers.

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.

scholarly journals GASAT: A Genetic Local Search Algorithm for the Satisfiability Problem

2006 ◽  
Vol 14 (2) ◽  
pp. 223-253 ◽  
Author(s):  
Frédéric Lardeux ◽  
Frédéric Saubion ◽  
Jin-Kao Hao
Keyword(s):  
Tabu Search ◽  
Local Search ◽  
Hybrid Algorithm ◽  
State Of The Art ◽  
Search Algorithm ◽  
Satisfiability Problem ◽  
Local Search Algorithm ◽  
Overall Performance ◽  
Genetic Local Search ◽  
Search Stage

This paper presents GASAT, a hybrid algorithm for the satisfiability problem (SAT). The main feature of GASAT is that it includes a recombination stage based on a specific crossover and a tabu search stage. We have conducted experiments to evaluate the different components of GASAT and to compare its overall performance with state-of-the-art SAT algorithms. These experiments show that GASAT provides very competitive results.

A reduction class containing formulas with one monadic predicate and one binary function symbol

1976 ◽  
Vol 41 (1) ◽  
pp. 45-49
Author(s):  
Charles E. Hughes
Keyword(s):  
Normal Form ◽  
Predicate Symbol ◽  
Conjunctive Normal Form ◽  
Function Symbol ◽  
Predicate Calculus ◽  
Binary Function ◽  
First Order ◽  
The Matrix ◽  
Reduction Class ◽  
Order Predicate Calculus

AbstractA new reduction class is presented for the satisfiability problem for well-formed formulas of the first-order predicate calculus. The members of this class are closed prenex formulas of the form ∀x∀yC. The matrix C is in conjunctive normal form and has no disjuncts with more than three literals, in fact all but one conjunct is unary. Furthermore C contains but one predicate symbol, that being unary, and one function symbol which symbol is binary.

Sign in / Sign up

Export Citation Format

Share Document