ABSTRACT. In 1930s Paul Erdos conjectured that for any positive integer C in any infinite +1 -1 sequence (x_n) there exists a subsequence x_d, x_{2d}, ... , x_{kd} for some positive integers k and d, such that |x_d + x_{2d} + ... + x_{kd}|> C. The conjecture has been referred to as one of the major open problems in combinatorial number theory and discrepancy theory. For the particular case of C=1 a human proof of the conjecture exists; for C=2 a bespoke computer program had generated sequences of length 1124 having discrepancy 2, but the status of the conjecture remained open even for such a small bound. We show that by encoding the problem into Boolean satisfiability and applying the state of the art SAT solvers, one can obtain a sequence of length 1160 with discrepancy 2 and a proof of the Erdos discrepancy conjecture for C=2, claiming that no sequence of length 1161 and discrepancy 2 exists. We also present our partial results for the case of C=3.

ABSTRACT. This paper presents an application of formal methods to the verification of power management modules in hardware designs. This paper identifies a distinct property of power management module and names it Dominant Controllability. This is a property of a netlist node and a subset of the inputs. The property holds if there exists an assignment to the subset of the inputs such that it sets the node to 0/1 regardless of the values of the rest of the inputs. Verification of power management modules in recent CPU and GPU designs includes hundreds of such properties. Dominant Controllability is different than controllability or random controllability which require only that the node is set to 0/1 by an assignment or random assignment to the inputs. The new application verifies Dominant Controllability using two formal methods: QBF-solver and netlist optimizer. Each method can be use independently or combined by a third algorithm that heuristically selects a method based on their performance in a specific design. The experimental results show that using QBF-solver is significantly faster when Dominant Controllability fails to hold (there is a bug in the design). Dominant Controllability fails when no assignment sets the node to 0/1, or when each such assignment is not dominant over other assignments to the rest of the inputs. In this case QBF-solver is faster because it concludes if Dominant Controllability fails without enumerating the large number of assignments. If the QBF-solver concludes that Dominant Controllability holds, netlist optimizer is used to verify the result, with a linear cost. Our experimental results show that even though using the netlist optimizer is incomplete, it is often successful when the power management module is very simple. The results also show that the third algorithm named Alternating selects the faster method successfully.

ABSTRACT. Dependency Quantified Boolean Formulas (DQBF) extend QBF with Henkin quantifiers, which allow for non-linear dependencies between the quantifiers. This extension is useful in verification problems for incomplete designs such as the partial equivalence checking problem (PEC), where a partial circuit, with some parts left open as ``black boxes'', is compared against a full circuit. The PEC problem is to decide whether the black boxes in the partial circuit can be filled in such a way that the two circuits become equivalent, while respecting that each black box only observes the subset of the signals that are designated as its input. We present a new algorithm that efficiently refutes unsatisfiable DQBF formulas. The algorithm detects situations in which already a subset of the possible assignments of the universally quantified variables suffices to rule out a satisfying assignment of the existentially quantified variables. Our experimental evaluation on PEC benchmarks shows that the new algorithm is a significant improvement both over approximative QBF-based methods, where our results are much more accurate, and over precise methods based on variable elimination, where the new algorithm scales much better in the number of Henkin quantifiers.

ABSTRACT. This is a talk in the branch of logic known as model theory, more precisely, in o-minimality. The first example of an o-minimal structure is the ordered algebraic structure on the set of real numbers and I shall focus on expansions of this structure. Being o-minimal means that the first order definable sets in the structure do not exhibit wild phenomena (this will be made precise). After discussing some basic theory of such structures I shall present some recent applications to diophantine geometry.

ABSTRACT. We propose Q(D)-resolution, a proof system for Quantified Boolean Formulas. Q(D)-resolution is a generalization of Q-resolution parameterized by a dependency scheme D. This system is motivated by the generalization of the QDPLL algorithm using dependency schemes implemented in the solver DepQBF. We prove soundness of Q(D)-resolution for a dependency scheme D that is strictly more general than the standard dependency scheme; the latter is currently used by DepQBF. This result is obtained by proving correctness of an algorithm that transforms Q(D)-resolution refutations into Q-resolution refutations and could be of independent practical interest. We also give an alternative characterization of resolution-path dependencies in terms of directed walks in a formula's implication graph which admits an algorithmically more advantageous treatment.

ABSTRACT. Modern CDCL SAT solvers routinely solve very large industrial SAT instances in relatively short periods of time. It is clear that these solvers somehow exploit the structure of real-world instances. How- ever, to-date there have been few results that precisely characterise this structure. In this paper, we provide evidence that the community structure of real-world SAT instances is correlated with the running time of CDCL SAT solvers. It has been known for some time that real-world SAT instances, viewed as graphs, have natural communities in them. A community is a sub-graph of the graph of a SAT instance, such that this sub-graph has more internal edges than outgoing to the rest of the graph. The community structure of a graph is often characterised by a quality metric called Q. Intuitively, a graph with high-quality community structure (high Q) is easily separable into smaller communities, while the one with low Q is not. We provide three results based on empirical data which show that community structure of real-world industrial instances is a better predictor of the running time of CDCL solvers than other commonly considered factors such as variables and clauses. First, we show that there is a strong correlation between the Q value and Literal Block Distance metric of quality of conflict clauses used in clause-deletion policies in Glucose-like solvers. Second, using regression analysis, we show that the the number of communities and the Q value of the graph of real-world SAT instances is more predictive of the running time of CDCL solvers than traditional metrics like number of variables or clauses. Finally, we show that randomly-generated SAT instances with 0.05 ≤ Q ≤ 0.13 are dramatically harder to solve for CDCL solvers than otherwise.

ABSTRACT. Stochastic Local Search (SLS) is considered to be one of the best solving technique for randomly generated problems and more recently also has shown great promise for several types of hard combinatorial problems. Within this work, we provide a thorough analysis of different implementation variants of SLS solvers on random and on hard combinatorial problems. By analyzing existing SLS implementations, we are able to discover new improvements inspired by CDCL solvers, which can speed up the search of all types of SLS solvers. Further, our analysis reveals that multilevel break values of variables can be easily computed and used within the decision heuristic. By augmenting the probSAT solver with the new heuristic, we are able to reach new state-of-the-art performance on several types of SAT problems, especially on those with long clauses. We further provide a detailed analysis of the clause selection policy used in focused search SLS solvers.

ABSTRACT. Blocked clause elimination is a powerful technique in SAT solving. In recent work, it has been shown that it is possible to decompose any propositional formula into two subsets (blocked sets) such that both can be solved by blocked clause elimination. We extend this work in several ways. First, we prove new theoretical properties of blocked sets. We then present additional and improved ways to efficiently solve blocked sets. Further, we propose novel decomposition algorithms for faster decomposition or which produce blocked sets with desirable attributes. We use decompositions to reencode CNF formulas and to obtain circuits, such as AIGs, which can then be simplified by algorithms from circuit synthesis and encoded back to CNF. Our experiments demonstrate that these techniques can increase the performance of the SAT solver Lingeling on hard to solve application benchmarks.

ABSTRACT. We present an encoding of pseudo-Boolean constraints based on decomposition with respect to a residual number system. We illustrate that careful selection of the base for the residual number system, and when bit-blasting modulo arithmetic, results in a powerful approach when solving hard pseudo-Boolean constraints. We demonstrate, using a range of pseudo-Boolean constraint solvers, that the obtained constraints are often substantially easier to solve.

ABSTRACT. We present novel approaches to detect cardinality constraints expressed in CNF. The first approach is based on a syntactic analysis of specific data structures used to represent binary and ternary clauses, whereas the second approach is based on a semantic analysis by unit propagation.

The syntactic approach computes an approximation of the cardinality constraints AtMost-$1$ and AtMost-$2$ constraints very fast, whereas the semantic approach has the property to be generic, i.e. it can detect cardinality constraints AtMost-$k$ for any $k$, at a higher computation cost.

Our experimental results suggest that the syntactic approach is efficient at recovering AtMost-$1$ and that the semantic one is efficient at recovering AtMost-$2$ cardinality constraints.