ABSTRACT. The B2B Scheduling Optimization Problem (B2BSOP) consists in finding the schedule of a set of meetings between persons minimizing the waiting time periods between meetings of the participants. Recent results have shown that a SAT-based approach is the-state-of-the-art. One of the interesting features of such approach is the use of implied constraints. In this work, we provide an experimental setting to study the effectiveness of using those implied constraints. Since there exists a reduced number of real-world B2B instances, we propose a random B2B instances generator, which reproduces certain features of these known to date real-world instances. We show the usefulness of some implied constraints depending on the characteristics of the problem, and the benefits of combining them. Finally, we give some insights on the exploitation of these implied constraints by the solver.

ABSTRACT. SAT solvers are increasingly being used for cryptanalysis of hash functions and symmetric encryption schemes. Inspired by this trend, we present MapleCrypt which is a SAT solver-based cryptanalysis tool for inverting hash functions. We reduce the hash function inversion problem for fixed targets into the satisfiability problem for Boolean logic, and use MapleCrypt to construct preimages for these targets. MapleCrypt has two key features, namely, a multi-armed bandit based adaptive restart (MABR) policy and a counterexample-guided abstraction refinement (CEGAR) technique. The MABR technique uses reinforcement learning to adaptively choose between different restart policies during the run of the solver. The CEGAR technique abstracts away certain steps of the input hash function, replacing them with the identity function, and verifies whether the solution constructed by MapleCrypt indeed hashes to the previously fixed targets. If it is determined that the solution produced is spurious, the abstraction is refined until a correct inversion to the input hash target is produced. We show that the resultant system is faster for inverting the SHA-1 hash function than state-of-the-art SAT-based inversion tools.

ABSTRACT. Combinatorial search with a parallel solver shares information among workers to diversify the search and to avoid duplicate work. As the number of workers increases, the amount of information significantly increases. As more information is shared, the cost of maintaining and utilizing information increases. State-of-the-art solvers allocate different search policies and share recent information, allowing the old information to decay. Randomization and restart strategies add search diversification, but do not memoize the information. We propose an approximate history map (AHM) to share information using only a small amount of memory. We have implemented the proposed AHM in a portfolio-based SAT solver and have experimentally evaluated. The AHM concept is scalable and broadly applicable to existing solvers for combinatorial searches in massively parallel environments at low cost.

ABSTRACT. CryptoMiniSat has been around since 2009, with only a single paper effectively talking about its internals. In this presentation I will try to explain the architecture and all the major trade-offs in CryptoMiniSat. I will try to go into some of the more interesting parts of CryptoMiniSat that makes it unique among the other solvers, including its history and current status. CryptoMiniSat is having a relatively successful time in the cryptographic scene. I will explain some of its use-cases and find some reasons for why so many (~180) papers used it in (mostly) that domain. I will also showcase a number of tools developed around the solver that others may find useful such as a comprehensive fuzz harness and a cloud computing-based performance test setup that rivals the size of some SAT solvers.

ABSTRACT. We present a method for improving the efficiency of SAT solver benchmarking. The increase in efficiency is achieved by removing redundant formulae from the benchmark for the evaluation and then mapping back the results on the entire benchmark. Experiments confirm the accurateness of our method along with a computation time reduction. The redundancy contained in the benchmark causes a bias in the evaluation result as well and therefore has an impact on its significance, particularly if multiple benchmarks are combined. We illustrate this effect by an example and pinpoint the structure of the benchmarks used for the competitive events performed since 2002. We focus on SAT, however, the presented results are of interest for other competitions as well.

ABSTRACT. Over the last 15--20 years there has been an astounding increase in the performance of Boolean satisfiability solvers based on the conflict-driven clause learning (CDCL) paradigm, and such CDCL solvers are now routinely used to solve real-world instances with hundreds of thousands or even millions of variables. Yet a deeper understanding of how these solvers actually work, and how they can be so successful, has proven elusive.

CDCL solvers are basically backtrack search algorithms that view the occurrence of conflicts as opportunities a) to add new clauses to the clause database and b) to adjust the variable branching order. These two mechanisms account for most of the performance gain of CDCL solvers over the classical DLL algorithm. However, on top of this basic architecture the fastest solvers typically employ dozens of heuristics to achieve further performance gains. Unfortunately, many of these heuristics tend to interact in subtle and unexpected ways making it hard to assess their contribution to performance. This is further compounded by the dearth of publicly-available benchmarks that can be used as a basis for analysis of SAT solver performance. A natural approach is to use the collected benchmarks from recent SAT competitions. This is not quite satisfactory, however, in that this is a very diverse set of benchmarks with starkly different properties, making it hard to draw general conclusions.

In this paper we propose theoretical benchmarks from proof complexity as a tool to investigate and understand CDCL solver performance. While the obvious downside is that these are combinatorial instances, and so it is not immediately obvious that they are practically relevant, we nevertheless believe that this is mitigated by that fact that such benchmarks are a) extremal along different dimensions, b) scalable, and c) \emph{easy} in the sense of having short proofs in the resolution proof system underlying CDCL. These attributes make the benchmarks particularly useful for a more systematic study of CDCL heuristics than earlier attempts.

This investigtion involves a large-scale empirical study of CDCL performance under hundreds of different parameter combinations. A major goal of the study is to compare observed performance with known theoretical results for the different benchmark families. This will help deepen our understanding of the power of CDCL as a proof system. Conversely, any unexpected anomalies may present opportunities for developing new algorithmic enhancements. In this preliminary work-in-progress report, we describe the benchmarks, the parameter configurations we plan to test, the experimental setup, and some tentative findings.

ABSTRACT. A new method to discover community structure in propositional CNF formulas is proposed, based on the new "Clashing-Neighbor Relation" for propositional CNF formulas and its analysis by eigenvectors. The main finding is that linear-algebra tools are able to handle large SAT application instances quickly and within practical memory budgets. Sparse matrix methods are crucial. Such preprocessing is intended for use on very difficult formulas, and is unlikely to be practical on moderate and easy SAT instances. The technique presented is aimed at unsat instances.

The underlying structure that has been analyzed most often is the variable-clause incidence graph, an undirected bipartite graph in which a variable has an edge to a clause if the variable appears positively or negatively in the clause. Assuming clauses are not tautologous, labeling each edge as plus or minus gives a precise representation of the formula. Two variables have been considered to have a "common-neighbor clause" if they both occur in the same clause, ignoring the polarities of their literals.

This paper introduces the clashing-neighbor relation and explains its motivation. The first idea is to consider the somewhat dual relation in which two clauses are considered to have a "common-neighbor variable" if they contain a variable in common. The second idea is to weight the strength of this connection by the combined ability of the two clauses to eliminate satisfying assignments to the variables, giving the clashing-neighbor relation as an m-by-m symetric matrix for a CNF with m clauses. Previous work weighted the strength of the connection between two variables by considering (implicitly) the ability of individual clauses to eliminate satisfying assignments.

Somewhat surprisingly the clashing-neighbor relation for an application formula with m about 155,000 can be computed and its leading eigenvector can be found with standard linear-algebra tools.