ABSTRACT. Cryptographic algorithms and satisfiability (SAT) solvers are intrinsically well-matched. Most cryptographic algorithms are presented in terms of a bounded number of operations on finite collections of bits: either to shuffle bits around in unpredictable ways (as typical in block ciphers or hash functions), or to perform algebraic operations on modular integers represented as vectors of bits (as in public key cryptography). This property allows many cryptographic algorithms, as well as statements about properties of those algorithms, to be represented as potentially large but purely propositional expressions.

Once cryptographic algorithms are represented as boolean terms, analyzing them with SAT solvers is straightforward. Any query that can be described using purely existential or purely universal quantifiers over the free variables in these terms can, in theory, be decided. Such queries include checking functions for injectivity (important for key expansion or random number generation); finding collisions in hash functions; comparing two alternative implementations of an algorithm for equality; and simplifying differential cryptanalysis, among others.

Many of these queries, though theoretically decidable, are not solvable in practice. Finding hash collisions with modern secure hash functions, for instance, is intractable. However, even in these cases, SAT solvers can help measure the relative security of different algorithms. Reduced-round versions of widely-used hashing or encryption algorithms are frequently analyzable by modern solvers (discovering secret keys or hash collisions), and the relative difficulty of analysis between alternative algorithms can be a useful comparison factor.

In addition to pure satisfiability queries, some other interesting problems can be stated with alternating quantifiers around purely propositional bodies. Such problems include synthesis of cryptographic implementation code from a specification. While these problems are less thoroughly researched, they are within the theoretical domain of emerging tools, such as quantified boolean formula (QBF) solvers and the exists-forall extensions in some satisfiability modulo theories (SMT) solvers.

This talk will walk through some of the properties of cryptographic code that are within the reach of existing solvers, as well as other properties that are currently infeasible but that may be solvable with future tools. It will also describe some specific tools that can be useful for applying SAT solvers to the analysis of cryptographic algorithms.

ABSTRACT. Nowadays, Conflict-Driven Clause Learning (CDCL) techniques are one of the key components of modern SAT solvers specialized in industrial instances. Last years, one of the focuses has been put on strategies to select which learnt clauses are removed during the search. Originally, one need for removing clauses was motivated by the finiteness of memory. Recently, it has been shown that more aggressive clause deletion policies may improve solvers performance, even when memory is sufficient. Also, the utility of learnt clauses has been related to the modular structure of industrial SAT instances.

In this paper, we show that augmenting SAT instances with learnt clauses does not always make them easier for the SAT solver. In fact, it makes worse the solver performance in many cases. However, we identify a set of highly useful learnt clauses, and we show that augmenting SAT instances with this set of clauses contributes to improve the solver performance in many cases, especially in satisfiable formulas. These clauses are related to the community structure of the formula, and they can be computed in a fast preprocessing step. This would suggest that the community structure may play an important role in clause deletion policies.

ABSTRACT. We introduce h-modularity, a structural parameter of CNF formulas, and present algorithms that render the decision problem SAT and the model counting problem #SAT fixed-parameter tractable when parameterized by h-modularity. The new parameter is defined in terms of a partition of the given CNF formula into strongly interconnected communities which are sparsely interconnected with each other. Each community forms a hitting formula, whereas the interconnections between communities form a graph of small treewidth. Our algorithms first identify the community structure and then use them for an efficient solution of SAT and #SAT, respectively. We further show that h-modularity is incomparable with known parameters under which SAT or \#SAT is fixed-parameter tractable.

ABSTRACT. We present a new algorithm that can efficiently extract information about nested functional dependencies between variables of a formula in CNF. Our algorithm uses the relation between gate encodings and blocked sets in CNF formulas. Our notion of "gate" emphasizes this relation. The presented algorithm is central to our new tool "cnf2aig" that produces equisatisfiable and-inverter-graphs (AIGs) from CNF formulas. We compare the novel algorithm to earlier approaches and show that the produced AIG are generally more succinct and use less input variables. As the gate-detection is related to the structure of input formulas, we furthermore analyze the gate-detection before and after applying preprocessing techniques.

ABSTRACT. Most modern SAT solvers expose a range of parameters to allow some customization to improve performance on specific instance sets. Performing this customization manually can be challenging and time-consuming, and as a consequence several automated algorithm configuration methods have been developed for this purpose. Although automatic algorithm configuration has already been applied successfully to many different SAT solvers, a comprehensive analysis of the configuration process is usually not readily available to users. Here, we present SpySMAC, the first tool to address this gap by providing an easy-to-use framework for (i) automatic configuration of SAT solvers in different settings, (ii) a thorough performance analysis comparing the best found configuration to the default one, and (iii) an assessment of each parameter's importance using the fANOVA framework. To showcase our tool, we apply it to MiniSAT and Lingeling, two well-known solvers with very different characteristics.

ABSTRACT. During the last decade, popular SMT solvers were extended step-by-step with a wide range of satisfiability-checking procedures for different theories. Many of those SMT solvers also support the user-defined tuning and combination of the procedures, typically via command-line options. However, configuring solvers this way is a tedious task with restricted options.

In this paper we present our modular and extensible C++ library SMT-RAT, which offers numerous parameterized procedure modules for different logics. These modules can be configured and combined into an SMT solver using a comprehensible but powerful strategy, which can be specified via a graphical user interface. This makes it easier to construct a solver which is tuned for a specific set of problem instances. Compared to a previous version, we extended our library with a number of new modules, and support parallelization in strategies. An additional contribution is our thread-safe and generic C++ library CArL, offering efficient data structures and basic operations for real arithmetic, which can be used for the fast implementation of new theory-solving procedures.

ABSTRACT. In this paper, we present SATGraf, a tool for visualizing the evolution of the structure of a Boolean SAT formula in real time as it is being processed by a conflict-driven clause-learning (CDCL) solver. The tool is parametric, allowing the user to define the structure to be visualised. In particular, the tool can visualise the community structure of real-world Boolean satisfiability (SAT) instances and their evolution during solving. Such visualisations have been the inspiration for several hypothesis about the connection between community structure and the running time of CDCL SAT solvers, some which we have already verified. SATGraf has allowed us to make three empirical observations regarding CDCL solvers. First, we observe that the Variable State Independent De- caying Sum (VSIDS) branching heuristic consistently chooses variables with a high number of inter-community edges. Second, we observe that backtracking from a conflict can sometimes cause unnecessary work. Fi- nally, we observe that VSIDS typically chooses decision variables with the same community as the previous decision variable.

ABSTRACT. PBLib is an easy to use and efficient library written in \CC\xspace for translating pseudo-Boolean (PB) constraints into CNF. We have implemented fifteen different encodings of PB constraints into CNF. Our aim is to use efficient encodings, in terms of formula size and whether unit propagation maintains generalized arc consistency. Moreover, PBlib normalizes PB constraints and can automatically decides which encoder provides the most effective translation. We also support incremental strengthening for optmization problems where the tighter bound is realized with few additional clauses as well as conditions for PB constraints.

ABSTRACT. This paper presents a local search SAT solver named CCAnr, which is based on the configuration checking method and has good performance on non-random SAT instances. As with the CCASat solver, CCAnr adopts the CCA (configuration checking with aspiration) heuristic and switches between two modes: it flips a variable according to the CCA heuristic if any; if there does not exist a variable allowed to be flipped by the CCA heuristic, then it flips a variable in a random unsatisfied clause. The main novelty of CCAnr lies on the greedy heuristic of picking a variable from the selected unsatisfied clause, which contributes significantly to its good performance on structured instances. Previous local search algorithms usually utilize diversification properties such as {\it age} or randomized strategy to pick a variable from the unsatisfied clause. Our experiments on crafted and application benchmarks from SAT Competition 2013 and 2014 show that CCAnr has better performance that other state of the art local search solvers on structured instances, and its performance can be further improved by using a preprocessor CP3. Our results suggest that a greedy heuristic in the focused search mode is helpful to improve local search algorithms for solving structured SAT instances.

ABSTRACT. Very large MaxSAT instances, comprising 10^20 clauses and beyond, commonly arise in a variety of domains. We present VOLT, a framework for solving such instances, using an iterative, lazy grounding approach. In each iteration, VOLT grounds a subset of clauses in the MaxSAT problem, and solves it using an off-the-shelf MaxSAT solver. VOLT provides a common ground to compare and contrast different lazy grounding approaches for solving large MaxSAT instances. We cast four diverse approaches from the literature on information retrieval and pro- gram analysis as instances of VOLT. We have implemented VOLT and evaluate its performance under different state-of-the-art MaxSAT solvers.

ABSTRACT. We consider the incremental computation of minimal unsatisfiable cores (MUCs) of QBFs. To this end, we equipped our incremental QBF solver DepQBF with a novel API which allows for incremental solving based on clause groups. A clause group is a set of clauses which is incrementally added to or removed from a previously solved QBF. Our implementation of this API is related to incremental SAT solvers which rely on selector variables and solving under assumptions. However, in contrast to SAT solvers the API entirely hides selector variables and assumptions from the user. This property facilitates the integration of DepQBF as a library in other tools. We present implementation details and show that the API can be implemented in any DPLL-based SAT and QBF solver. For the first time, we report on experiments related to the incremental computation of MUCs of QBFs using DepQBF's novel clause group API. Our results illustrate its efficiency and applicability.

ABSTRACT. Most recent MaxSAT algorithms rely on a succession of calls to a SAT solver in order to find an optimal solution. In particular, several algorithms take advantage of the ability of SAT solvers to identify unsatisfiable subformulas. Usually, these MaxSAT algorithms perform better when small unsatisfiable subformulas are found early. However, this is not the case in many problem instances, since the whole formula is given to the SAT solver in each call. In this paper, we propose to partition the MaxSAT formula using a resolution-based graph representation. Partitions are then iteratively joined by using a proximity measure extracted from the graph representation of the formula. The algorithm ends when only one partition remains and the optimal solution is found. Experimental results show that this new approach further enhances a state of the art MaxSAT solver to optimally solve a larger set of industrial problem instances.

ABSTRACT. We consider the algorithmic task of computing a maximal autarky for a clause-set F, i.e., a partial assignment which satisfies every clause of F it touches, and where this property is destroyed by adding any non-empty set of further assignments. We employ SAT solvers as oracles, using various capabilities. Using the standard SAT oracle, log_2(n(F)) oracle calls suffice, where n(F) is the number of variables, but the drawback is that (translated) cardinality constraints are employed, which makes this approach less efficient in practice. Using an extended SAT oracle, motivated by the capabilities of modern SAT solvers, we show how to compute maximal autarkies with 2 n(F)^{1/2} simpler oracle calls. The novel algorithm combines the previous two main approaches, based on the autarky-resolution duality and on SAT translations.

ABSTRACT. We give improved deterministic algorithms solving sparse instances of MAX-SAT and MAX-$k$-CSP. For instances with $n$ variables and $cn$ clauses (constraints), we give algorithms running in time $\poly(n)\cdot 2^{n(1-\mu)}$ for \begin{itemize} \item $\mu = \Omega(\frac{1}{c} )$ and polynomial space solving MAX-SAT and MAX-$k$-SAT, \item $\mu = \Omega(\frac{1}{\sqrt{c}} )$ and exponential space solving MAX-SAT and MAX-$k$-SAT, \item $\mu = \Omega(\frac{1}{ck^2} )$ and polynomial space solving MAX-$k$-CSP, \item $\mu = \Omega(\frac{1}{\sqrt{ck^3}} )$ and exponential space solving MAX-$k$-CSP. \end{itemize} The previous MAX-SAT algorithms have savings $\mu=\Omega(\frac{1}{c^2 \log^2 c})$ for running in polynomial space~\cite{SST14} and $\mu=\Omega(\frac{1}{c \log c})$ for exponential space~\cite{DW06}. We also give an algorithm with improved savings for satisfiability of depth-2 threshold circuits with $cn$ wires.