Boolean Satisfiability solvers have gone through dramatic improvements in their performances and scalability over the last few years by considering symmetries. It has been shown that by using graph symmetries and generating symmetry breaking predicates (SBPs) it is possible to break symmetries in Conjunctive Normal Form (CNF). The SBPs cut down the search space to the nonsymmetric regions of the space without affecting the satisfiability of the CNF formula. The symmetry breaking predicates are created by representing the formula as a graph, finding the graph symmetries and using some symmetry extraction mechanism (Crawford et al.). Here in this paper we take one non-trivial CNF and explore its symmetries. Finally, we generate the SBPs and adding it to CNF we show how it helps to prune the search tree, so that SAT solver would take short time. Here we present the pruning procedure of the search tree from scratch, starting from the CNF and its graph representation. As we explore the whole mechanism by a non-trivial example, it would be easily comprehendible. Also we have given a new idea of generating symmetry breaking predicates for breaking symmetry in CNF, not derived from Crawford's conditions. At last we propose a backtrack SAT solver with inbuilt SBP generator.
ENS Cachan（卡尚高等师范学校）；Inria（法国国家信息与自动化研究所）；Université Paris Diderot（巴黎狄德罗大学）；Ecole Polytechnique（巴黎综合理工学院）
We extend the knowledge about so-called structural restrictions of $\mathrm{\#SAT}$ by giving a polynomial time algorithm for $β$-acyclic $\mathrm{\#SAT}$. In contrast to previous algorithms in the area, our algorithm does not proceed by dynamic programming but works along an elimination order, solving a weighted version of constraint satisfaction. Moreover, we give evidence that this deviation from more standard algorithm is not a coincidence, but that there is likely no dynamic programming algorithm of the usual style for $β$-acyclic $\mathrm{\#SAT}$.
Unit resolution can simplify a CNF formula or detect an inconsistency by repeatedly assign the variables occurring in unit clauses. Given any CNF formula sigma, we show that there exists a satisfiable CNF formula psi with size polynomially related to the size of sigma such that applying unit resolution to psi simulates all the effects of applying it to sigma. The formula psi is said to be the reified counterpart of sigma. This approach can be used to prove that the failed literal rule, which is an inference rule used by some SAT solvers, can be entirely simulated by unit resolution. More gener…
Applying pre- and inprocessing techniques to simplify CNF formulas both before and during search can considerably improve the performance of modern SAT solvers. These algorithms mostly aim at reducing the number of clauses, literals, and variables in the formula. However, to be worthwhile, it is necessary that their additional runtime does not exceed the runtime saved during the subsequent SAT solver execution. In this paper we investigate the efficiency and the practicability of selected simplification algorithms for CDCL-based SAT solving. We first analyze them by means of their expected imp…
TU Delft（代尔夫特理工大学）；Univ. Helsinki（赫尔辛基大学）；JKU Linz（林茨约翰·开普勒大学）
Generalizing the novel clause elimination procedures developed in [M. Heule, M. Järvisalo, and A. Biere. Clause elimination procedures for CNF formulas. In Proc. LPAR-17, volume 6397 of LNCS, pages 357-371. Springer, 2010.], we introduce explicit (CCE), hidden (HCCE), and asymmetric (ACCE) variants of a procedure that eliminates covered clauses from CNF formulas. We show that these procedures are more effective in reducing CNF formulas than the respective variants of blocked clause elimination, and may hence be interesting as new preprocessing/simplification techniques for SAT solving.
Insight Centre for Data Science and Analytics（洞察数据科学与分析中心）；University College Cork（科克大学学院）；SFI Centre for Research Training in AI（SFI人工智能研究培训中心）；School of Computer Science & IT（计算机科学与信息技术学院）
Feature extraction is a fundamental task in the application of machine learning methods to SAT solving. It is used in algorithm selection and configuration for solver portfolios and satisfiability classification. Many approaches have been proposed to extract meaningful attributes from CNF instances. Most of them lack a working/updated implementation, and the limited descriptions lack clarity affecting the reproducibility. Furthermore, the literature misses a comparison among the features. This paper introduces SATfeatPy, a library that offers feature extraction techniques for SAT problems in t…
Ben-Gurion University of the Negev（内盖夫本-古里安大学）；The University of Melbourne（墨尔本大学）
We present an approach to propagation-based SAT encoding of combinatorial problems, Boolean equi-propagation, where constraints are modeled as Boolean functions which propagate information about equalities between Boolean literals. This information is then applied to simplify the CNF encoding of the constraints. A key factor is that considering only a small fragment of a constraint model at one time enables us to apply stronger, and even complete, reasoning to detect equivalent literals in that fragment. Once detected, equivalences apply to simplify the entire constraint model and facilitate f…
National University of Singapore（新加坡国立大学）；IIT Hyderabad（印度理工学院海得拉巴分校）
The runtime performance of modern SAT solvers is deeply connected to the phase transition behavior of CNF formulas. While CNF solving has witnessed significant runtime improvement over the past two decades, the same does not hold for several other classes such as the conjunction of cardinality and XOR constraints, denoted as CARD-XOR formulas. The problem of determining the satisfiability of CARD-XOR formulas is a fundamental problem with a wide variety of applications ranging from discrete integration in the field of artificial intelligence to maximum likelihood decoding in coding theory. The…
In this paper, we address the problem of enumerating all models of a Boolean formula in conjunctive normal form (CNF). We propose an extension of CDCL-based SAT solvers to deal with this fundamental problem. Then, we provide an experimental evaluation of our proposed SAT model enumeration algorithms on both satisfiable SAT instances taken from the last SAT challenge and on instances from the SAT-based encoding of sequence mining problems.
Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization
Department of Computer Science, Rice University（计算机科学系，里士大学）；Department of Applied Mathematics and Statistics, Colorado School of Mines（应用数学与统计系，科罗拉多矿业学院）；Department of Mathematics, University of California, Los Angeles（数学系，加州大学洛杉矶分校）
Indian Institute of Technology Kanpur（印度理工学院坎普尔分校）；School of Computing, National University of Singapore（新加坡国立大学计算学院）
The study of phase transition behaviour in SAT has led to deeper understanding and algorithmic improvements of modern SAT solvers. Motivated by these prior studies of phase transitions in SAT, we seek to study the behaviour of size and compile-time behaviour for random k-CNF formulas in the context of knowledge compilation. We perform a rigorous empirical study and analysis of the size and runtime behavior for different knowledge compilation forms (and their corresponding compilation algorithms): d-DNNFs, SDDs and OBDDs across multiple tools and compilation algorithms. We employ instances gene…
The Maximum Satisfiability (MaxSAT) problem is the problem of finding a truth assignment that maximizes the number of satisfied clauses of a given Boolean formula in Conjunctive Normal Form (CNF). Many exact solvers for MaxSAT have been developed during recent years, and many of them were presented in the well-known SAT conference. Algorithms for MaxSAT generally fall into two categories: (1) branch and bound algorithms and (2) algorithms that use successive calls to a SAT solver (SAT- based), which this paper in on. In practical problems, SAT-based algorithms have been shown to be more effici…
(k,s)-SAT is the satisfiability problem restricted to instances where each clause has exactly k literals and every variable occurs at most s times. It is known that there exists a function f such that for s\leq f(k) all (k,s)-SAT instances are satisfiable, but (k,f(k)+1)-SAT is already NP-complete (k\geq 3). The best known lower and upper bounds on f(k) are Omega(2^k/k) and O(2^k/k^a), where a=\log_3 4 - 1 = 0.26.... We prove that f(k) = O(2^k \cdot \log k/k), which is tight up to a \log k factor.
A propositional logic sentence in conjunctive normal form that has clauses of length two (a 2-CNF) can be associated with a multigraph in which the vertices correspond to the variables and edges to clauses. We first show that every such sentence that has been reduced, that is, which is unchanged under application of certain tautologies, is equisatisfiable to a 2-CNF whose associated multigraph is, in fact, a simple graph. Our main result is a complete characterization of graphs that can support unsatisfiable 2-CNF sentences. We show that a simple graph can support an unsatisfiable reduced 2-CN…
Institute of Information Systems（信息系统研究所）；Vienna University of Technology（维也纳工业大学）
There are various approaches to exploiting "hidden structure" in instances of hard combinatorial problems to allow faster algorithms than for general unstructured or random instances. For SAT and its counting version #SAT, hidden structure has been exploited in terms of decomposability and strong backdoor sets. Decomposability can be considered in terms of the treewidth of a graph that is associated with the given CNF formula, for instance by considering clauses and variables as vertices of the graph, and making a variable adjacent with all the clauses it appears in. On the other hand, a stron…
Institute of Information Systems（信息系统研究所）；Vienna University of Technology（维也纳工业大学）
Backdoor sets, a notion introduced by Williams et al. in 2003, are certain sets of key variables of a CNF formula F that make it easy to solve the formula; by assigning truth values to the variables in a backdoor set, the formula gets reduced to one or several polynomial-time solvable formulas. More specifically, a weak backdoor set of F is a set X of variables such that there exits a truth assignment t to X that reduces F to a satisfiable formula F[t] that belongs to a polynomial-time decidable base class C. A strong backdoor set is a set X of variables such that for all assignments t to X, t…
