ABSTRACT. We study the parametrisation of QBF resolution calculi by dependency schemes. One of the main problems in this area is to understand for which dependency schemes the resulting calculi are sound. Towards this end we propose a semantic framework for variable independence based on `exhibition' by QBF models, and use it to express a property of dependency schemes called `full exhibition' that is known to be sufficient for soundness in Q-resolution. Introducing a generalised form of the long-distance resolution rule, we propose a complete parametrisation of classical long-distance Q-resolution, and show that full exhbition remains sufficient for soundness. We demonstrate that our approach applies to the current research frontiers by proving that the reflexive resolution path dependency scheme is fully exhibited.

ABSTRACT. Solving Quantified Boolean Formulas (QBFs) is a challenging problem due to its high complexity. Many successful methods have been proposed, including extensions of DPLL/CDCL procedures and expansion-based approaches. In this paper, we present a novel method that is inspired by concepts from the field of parameterized complexity. More specifically, we develop a dynamic programming algorithm that traverses a tree decomposition of the QBF instance. We implemented our method using Binary Decision Diagrams as key ingredient to compactly represent the partial solutions computed during dynamic programming. Experiments indicate that our prototype shows promising results for instances with few quantifier alternations and where the treewidth of the propositional formula does not exceed 50. In fact, treewidth can be understood as a measurement of structure within the formula, and to the best of our knowledge has not been used explicitly in QBF solvers yet. 
 

ABSTRACT. Harary’s generalized Tic-Tac-Toe is an achievement game for polyominoes, where two players alternately put a stone on a grid board, and the player who first achieves a given polyomino wins the game. It is known whether the first player has a winning strategy in the generalized Tic-Tac-Toe for almost all polyominoes except the one called Snaky. GTTT(p,q) is an extension of the generalized Tic-Tac-Toe, where the first player places q stones in the first move and then the players place　q stones in each turn. In this paper, in order to attack GTTT(p,q) by　QBF solvers, we propose a QBF encoding for GTTT(p,q). Our encoding　is based on Gent and Rowley’s encoding for Connect-4. We modify three　parts of the encoding: initial condition, move rule and winning condition　of the game. The experimental results show that some QBF solvers can　be used to solve GTTT(p,q) on 4 × 4 or smaller boards.

ABSTRACT. Similar to the satisfiability (SAT) problem, which can be seen to be the archetypical problem for NP, the quantified Boolean formula problem (QBF) is the archetypical problem for PSPACE. Recently, Atserias and Oliva (2014) showed that, unlike for SAT, many of the well-known decompositional parameters (such as treewidth and pathwidth) do not allow efficient algorithms for QBF. The main reason for this seems to be the lack of awareness of these parameters towards the dependencies between variables of a QBF formula. In this paper we extend the ordinary pathwidth to the QBF-setting by introducing prefix pathwidth, which takes into account the dependencies between variables in a QBF, and show that it leads to an efficient algorithm for QBF. We hope that our approach will help to initiate the study of novel tailor-made decompositional parameters for QBF and thereby help to lift the success of these decompositional parameters from SAT to QBF.

ABSTRACT. In this paper, we address the problem of random generation of realistic pseudo-industrial SAT instances. First, we review some existing generators which are based on the notions of scale-free structure and community structure. Then, we propose a new generator based on the notion of \emph{popularity} and \emph{similarity}. This new model generates instances with both scale-free and community structure, solving the drawbacks of the previous generators.

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. We consider the problem of computing Skolem functions for satisfied dependency quantified Boolean formulas (DQBFs). We show how Skolem functions can be obtained from an elimination-based DQBF solver and how to take preprocessing steps into account. The size of the Skolem functions is optimized by don't-care minimization using Craig interpolants and rewriting techniques. Experiments with our DQBF solver HQS show that we are able to effectively compute Skolem functions with very little overhead compared to the mere solution of the formula.

ABSTRACT. Structural properties of CNF formulas are often suggested as a basis for explaining the large variation in solving hardness or as instance features that could be exploited by solvers. Examples include community structure and tree-width of graphs associated with the formulas. We will describe some findings from an experimental exploration of the relevance of these properties to actual performance of CDCL SAT solvers.

ABSTRACT. We present a compilation algorithm for beta-acyclic formulas into polynomial size decision DNNF. The DNNF constructed by this algorithm are not structured and we present a proof that this cannot be improved by showing that beta-acyclic formulas may have exponential size structured DNNF.

ABSTRACT. In my talk I would like to give some insights about recent investigations into the structure of MU, minimally unsatisfiable clause-sets, organised in layers by the deficiency.

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. The talk adresses three classes of open problems for quantified Boolean formulas (QBFs). The first class of problems is related to questions of minimal falsity under the restriction of fixed deficiency. The second class deals with the satisfiability problem for quantified Horn formulas and related problems. Concluding, we will discuss the expressive power of QBFs and the size of mimimal equivalence models for some subclasses.

ABSTRACT. This is an extended abstract of our ongoing research. We report that the ordering of additions strongly affects the performance of a CNF encoding of cardinality constraints. Then we propose a new encoding that automatically decides a nice ordering by exploiting the underlying graph structure.

ABSTRACT. The complexity of various Constraint Satisfaction Problems (CSP) when parameterized by structural measures (such as treewidth or clique-width) is a very well-investigated area. In this paper, we take a fresh look at such questions from the point of view of approximation, considering four standard CSP predicates: AND, OR, PARITY, and MAJORITY. By providing new or tighter hardness results for the satisfiability versions, as well as approximation algorithms for the corresponding maximization problems, we show that already these basic predicates display a diverse set of behaviors, ranging from being FPT to optimize exactly for quite general parameters (PARITY), to being W-hard but well-approximable (OR, MAJORITY) to being W-hard and inapproximable (AND). Our results indicate the interest in posing the question of approximability during the usual investigation of CSP complexity with regards to the landscape of structural parameters.

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.

ABSTRACT. Propositional satisfiability (SAT) and related problems (like Model Counting, QBF-SAT, and CSP) are in practise often much easier to solve than suggested by their respective theoretical worst-case complexities. This "friendliness" of the real world is often explained by the presence of some kind of "hidden structure" in practical problem instances. In this talk we will review some mathematical concepts that attempt to capture the structure in problem instances and discuss their virtues and limits. We will focus rather on general questions than on  technical details.