ABSTRACT. The boolean Pythagorean Triples problem has been a longstanding open problem in Ramsey Theory. This problem asks whether the set N = {1,2,...} of natural numbers can be divided into two parts, with no part containing a triple (a,b,c) such that a^2 + b^2 = c^2. A prize for the solution was offered by Ronald Graham over two decades ago. We solve the boolean Pythagorean Triples problem using the Cube-and-Conquer method, a hybrid SAT method for hard problems, employing both look-ahead and CDCL solvers. To tackle the problem successfully, we devised dedicated heuristics and used strong computational resources. Finally, due to the general interest in this mathematical problem, our result requires a formal proof. Exploiting recent progress in unsatisfiability proofs of SAT solvers, we produced and verified a proof in the DRAT format, which is almost 200 terabytes in size. We constructed and shared a compressed certificate of 68 gigabytes in size that allows anyone to obtain the DRAT proof for checking.

ABSTRACT. Unavoidable subgraphs have been widely studied in the context of Ramsey Theory. The research in this area focusses on highly structured graphs such as cliques, cycles, paths, stars, and wheels. We propose to study maximum unavoidable subgraphs measuring the size in the number of edges. We computed maximum unavoidable subgraphs for graphs up to order twelve via SAT solving and observed that these subgraphs are less structured, although all are bipartite. We envision that maximum unavoidable subgraphs can be exploited using an alternative approach to breaking graph symmetries. We also present the concept of multi-component unavoidable subgraphs and show that maximum multi-component subgraphs are unavoidable in small graphs.

ABSTRACT. Description Logics(DLs) are knowledge representation and reasoning formalisms widely used in many practical settings. Among them, the EL+ family of DLs stands out due to the availability of polynomial-time inference algorithms and its ability to represent knowledge from domains such as medical informatics. However, the construction of an ontology is an error-prone process which often leads to unintended inferences. This paper presents the BEACON SAT-based tool for debugging E L+ ontologies. BEACON builds on earlier work relating minimal justifications (MinAs) of EL+ ontologies and MUSes of a Horn formula, and it integrates state-of-the-art algorithms for solving different function problems in the SAT domain.

ABSTRACT. This paper describes a major revision of the OpenSMT solver developed since 2008. The version 2 significantly improves its predecessor by providing a design that supports extensions, several critical bug fixes and performance improvements. The distinguishing feature of the new version is the support for a wide range of parallelization algorithms both on multi-core and cloud-computing environments. Presently the solver implements the quantifier free theories of uninterpreted functions and equalities and linear real arithmetics, and is released under the MIT license.

ABSTRACT. The recently developed massively parallel satisfiability (SAT) solver HordeSAT was designed in a modular way to allow the integration of any sequential CDCL-based SAT solver in its core. We integrated the QCDCL-based quantified Boolean formula (QBF) solver DepQBF in HordeSAT to obtain a massively parallel QBF solver---HordeQBF. In this paper we describe the details of this integration and report on results of the experimental evaluation of HordeQBF's performance. HordeQBF achieves superlinear average and median speedup on the hard instances of the 2014 QBF Gallery (Competition).

ABSTRACT. We describe LMHS, an open source weighted partial MaxSAT solver. LMHS is a hybrid SAT-IP MaxSAT solver that implements the implicit hitting set approach to MaxSAT. In MaxSAT Evaluation 2015, LMHS solved the most instances in the weighted partial crafted and industrial categories. On top of the main algorithm, LMHS offers integrated preprocessing, solution enumeration, an incremental API, and the use of a choice of SAT and IP solvers. We describe the main features of LMHS, and give empirical results on the influence of preprocessing and the choice of the underlying SAT and IP solvers on the performance of LMHS.

ABSTRACT. Automated configuration can be used to improve the performance of a SAT solver, for example for verification problems. Increasing the space of possible parameter configurations leads to harder maintainable code and to more undiscovered bugs. We present the tool SpyBug that finds erroneous minimal parameter configurations of SAT solvers and their parameter specification to help developers to identify and narrow down bugs in their solvers. The importance of SpyBug is shown by the bugs we found for four well-known SAT solvers that won prices in international competitions.

ABSTRACT. The Model-Constructing Satisfiability Calculus (mcSAT) is a recently proposed generalisation of propositional DPLL/CDCL for reasoning modulo theories. In contrast to most DPLL(T)-based SMT solvers, which carry out conflict-driven learning only on the propositional level, mcSAT calculi can also synthesise new theory literals during learning, resulting in a simple yet very flexible framework for designing efficient decision procedures. We present an mcSAT calculus for the theory of bounded-length bit-vectors, based on tailor-made conflict-driven learning that can exploit both propositional and arithmetic properties of bit-vector operations. Our procedure can in particular avoid full bit-blasting for constraints that are mainly arithmetic in nature, and therefore performs well on problems from domains like software model checking.

ABSTRACT. We describe a new approach to deciding satisfiability of quantified bit-vector formulas using binary decision diagrams and approximations. The approach is motivated by the observation that the binary decision diagram for a quantified formula is typically significantly smaller than the diagram for the subformula within the quantifier scope. The suggested approach has been implemented and the experimental results show that it decides more benchmarks from the SMT-LIB repository than state-of-the-art SMT solvers for this theory, namely Z3 and CVC4.