ABSTRACT. In this paper we present new implementation details and benchmarking results for our parallel portfolio solver \topo. In particular, we discuss ideas and implementation details for the exchange of learned clauses in a massively-parallel SAT solver which is designed to run more that $1,000$ solver threads in parallel. Furthermore, we go back to the roots of portfolio SAT solving, and discuss the impact of diversifying the solver by using different restart- , branching- and clause database management heuristics. We show that these techniques can be used to tune the solver towards different problems. However, in a case study on formulas derived from Bounded Model Checking problems we see the best performance when using a rather simple clause exchange strategy. We show details of these tests and discuss possible explanations for this phenomenon.

As computing times on massively-parallel clusters are expensive, we consider it especially interesting to share these kind of experimental results.

ABSTRACT. Performing hundreds of test runs and a source-code analysis, we empirically identified improved parameter configurations for the CryptoMiniSat (CMS) 5 for solving cryptographic CNF instances originating from algebraic known-plaintext attacks on 3 rounds encryption of the Small AES-64 model cipher SR(3, 4, 4, 4). We finally became able to reconstruct 64-bit long keys in under an hour real time which, to our knowledge, has never been achieved so far. Especially, not without any assumptions or previous knowledge of key-bits (for instance in the form of side-channels, as in Mohamed et al., Improved Algebraic Side-Channel Attack on AES, 2012). A statistical analysis of the non-deterministic solver runtimes was carried out and command line parameter combinations were defined to yield best runtimes which ranged from under an hour to a few hours in median at the beginning. We proceeded using an Automatic Algorithm Configuration (AAC) tool to systematically extend the search for even better solver configurations with success to deliver even shorter solving times. In this work we elaborate on the systematics we followed to reach our results in a traceable and reproducible way. The ultimate focus of our investigations is to find out if CMS, when appropriately tuned, is indeed capable to attack even bigger and harder problems than the here solved ones. For the domain of cryptographic research, the duration of the solving time plays an inferior role as compared to the practical feasibility of finding a solution to the problem. The perspective scalability of the here presented results is the object of further investigations.

ABSTRACT. A very old quest in campanology is the search for peals, which can be considered as constrained searches for Hamiltonian cycles of a Cayley graph. Two particularly hard problems are finding bobs-only peals of Stedman Triples and Erin Triples. We show how to efficiently reduce them to boolean satisfiability and use a SAT solver to help find bobs-only peals of Stedman Triples, and express the unsolved problem of bobs-only Erin Triples as an unsolved SAT problem. This approach is based on the author's very efficient general reduction of the Hamiltonian Cycle Problem (HCP) to Boolean Satisfiability (SAT) converting any Hamiltonian Cycle problem with n vertices and m directed edges to a SAT problem with approximately n.log2(m) variables and 2m.(log2(n)+1) clauses.

ABSTRACT. DRAT proofs have become the de facto standard for certifying SAT solvers' results. State-of-the-art DRAT checkers are able to efficiently establish the unsatisfiability of a formula. However, DRAT checking requires unit propagation, and so it is computationally non-trivial. Due to design decisions in the development of early DRAT checkers, the class of proofs accepted by state-of-the-art DRAT checkers differs from the class of proofs accepted by the original definition. In this paper, we formalize the operational definition of DRAT proofs, and discuss practical implications of this difference for generating as well as checking DRAT proofs. We also show that these theoretical differences have the potential to affect whether some proofs generated in practice by SAT solvers are correct or not.

ABSTRACT. A Pseudo-Boolean (PB) constraint is a linear inequality constraint over Boolean variables. A popular idea to solve PB-constraints is to transform them to CNFs (via BDDs, adders and sorting networks) and process them using -- increasingly improving -- state-of-the-art SAT-solvers. Recent research have favored the approach that use Binary Decision Diagrams (BDDs), which is evidenced by several new constructions and optimizations. We show that encodings based on comparator networks can still be very competitive. We present a system description of a PB-solver based on MiniSat+ which we extended by adding a new construction of a selection network called 4-Way Merge Selection Network, with a few optimizations based on other solvers. Experiments show that on many instances of popular benchmarks our technique outperforms other state-of-the-art PB-solvers.

ABSTRACT. The last 20 years have seen dramatic improvements in performance of algorithms for Boolean satisfiability---so-called SAT solvers---and today conflict-driven clause learning (CDCL) solvers are routinely used for real-world problems in a wide range of application areas. One serious short-coming of CDCL, however, is that the underlying method of reasoning is quite weak, which can lead to exponential running times for many simple combinatorial problems. A tantalizing solution is to instead use stronger pseudo-Boolean (PB) reasoning, but so far the promise of exponential gains in performance has failed to materialize---the increased theoretical strength seems hard to harness algorithmically, and in many applications CDCL-based methods are still superior.

We propose a modified approach to pseudo-Boolean solving, using division instead of the saturation rule in [Chai and Kuehlmann '05] and other PB solvers. In addition to resulting in a stronger conflict analysis, this also keeps integer coefficient sizes down, which further improves performance. Together with some other optimizations, this yields a solver that performed very well in the Pseudo-Boolean Competitions 2015 and 2016, and that has speed approaching that of CDCL-based methods measured in terms of number of conflicts per second.

This is a presentation-only submission of a paper to be published at IJCAI '18.

ABSTRACT. We study solution-based phase saving in the linear maxSAT algorithm. Contrary to conventional phase saving, which assigns values to variables based on their most recent assignment during the search, solution-based phasing selects the values according to the best solution found so far. Thus, the algorithm focuses its efforts in the region ``close'' to the current best solution. Such an approach resembles techniques used in local search algorithms, where small incremental perturbations are performed on the best known solution. Although the algorithm has appeared in the literature before, it has not been used in the annual maxSAT evaluations and thus its position among modern solvers is not clear. We implemented solution-based phase saving in Open-WBO and evaluated its performance on benchmarks from the incomplete track of the latest maxSAT evaluation 2017 and the international timetabling competition 2011. The experimental results demonstrate that the approach is highly effective when compared to the baseline linear maxSAT algorithm, outperforming the rank one solvers from the 60 and 300 seconds unweighted competition tracks. When compared to winner of the weighted categories, maxroster, our analysis reveals that the approach provides substantially better results for a number of applications, even competing against specialized timetabling algorithms, although maxroster achieves a higher overall competition score. Hence, we argue solution-based phase saving should be part of the standard machinery for maxSAT.

ABSTRACT. The wide adoption of machine learning approaches in the industry, government, medicine and science has renewed the interest in interpretable machine learning: many decisions are too important to be delegated to black-box techniques such as deep neural networks or kernel SVMs. Historically, problems of learning interpretable classifiers, including classification rules or decision trees, have been approached by greedy heuristic methods as essentially all the exact optimization formulations are NP-hard. Our primary contribution is a MaxSAT-based framework, called MLIC, which allows principled search for interpretable classification rules expressible in propositional logic. Our approach benefits from the revolutionary advances in the constraint satisfaction community to solve large-scale instances of such problems. In experimental evaluations over a collection of benchmarks arising from practical scenarios we demonstrate its effectiveness: we show that the formulation can solve large classification problems with tens or hundreds of thousands of examples and thousands of features, and to provide a tunable balance of accuracy vs. interpretability. Furthermore, we show that in many problems interpretability can be obtained at only a minor cost in accuracy.

The primary objective of the paper is to show that recent advances in the MaxSAT literature make it realistic to find optimal (or very high quality near-optimal) solutions to large-scale classification problems. We also hope to encourage researchers in both interpretable classification and in the constraint programming community to take it further and develop richer formulations, and bespoke solvers attuned to the problem of interpretable ML.

[We have submitted the paper concurrently to CP-18 and therefore marked the paper in "presentaiton-only" category]

ABSTRACT. Experimental data and benchmarks play a crucial role in developing new algorithms and implementations of SAT solvers. Besides comparing and evaluating solvers, they provide the basis for all kinds of experiments, for setting up hypothesis and for testing them. Currently -- even though some initiatives for setting up benchmark databases have been undertaken, and the SAT Competitions provide a ``standardized'' collection of instances -- it is hard to assemble benchmark sets with prescribed properties. Moreover, the origin of SAT instances is often not clear, and benchmark collections might contain duplicates. In this paper we suggest a framework to store meta-data information about SAT instances and provide a framework for collecting, assessing and distributing benchmark metadata.

ABSTRACT. It has been an ongoing debate for a long time about how SAT solvers and in general different or new algorithms should be evaluated and compared both in competitions and more importantly in papers. Evaluations are usually performed on existing benchmarks. Cross-validation and other means to avoid over-fitting are rarely used. In this paper we revisit the old idea of scrambling benchmarks also used in early competitions. Scrambling has the goal to make results of such evaluations more robust. We present a new method for scrambling CNFs, which allows to gradually increase the effect of scrambling, from keeping the scrambled CNF close to the original CNF, to complete random permutation of variables, clauses, and phases of literals. We used this method to scramble benchmarks from the last two SAT competitions and solved them with the best solvers in the main track of the last SAT competition. As expected our experimental results suggest that scrambling has a substantial effect on the performance of individual solvers but surprisingly has little effect on rankings among solvers. As a consequence we argue that only using our method of scrambling is not enough to increase robustness of competitions and evaluations in general.

ABSTRACT. Over the last decades Boolean satisfiability (SAT) solvers based on conflict-driven clause learning (CDCL) have developed to the point where they can handle formulas with millions of variables. Yet a deeper understanding of how these solvers can be so successful has remained elusive.

In this work we try to shed light on CDCL performance by using theoretical benchmarks. While these are crafted instances, they have the attractive features of being a) scalable, b) extremal with respect to different proof search parameters, and c) theoretically *easy* in the sense of having short proofs in the resolution proof system underlying CDCL. This allows for a systematic study of solver heuristics and how successfully they implement efficient proof search.

We report results from extensive experiments with different CDCL parameter configurations on a wide range of benchmarks. Our findings include several examples where theory predicts and explains CDCL behaviour, but also raises a number of intriguing questions for further study.

This is a presentation-only submission of a paper that (we hope and believe) will be published at IJCAI '18.

ABSTRACT. A convenient way to deploy services on a computer is to use a lightweight virtualization approach like docker.

This talk will present some observations made in the context of deploying SAT solvers on the cloud. 

ABSTRACT. Questions and answers with the audience