The maximal clique enumeration (MCE) problem consists of computing and listing all maximal cliques in a finite graph. The problem is NP-complete since it subsumes the classic version of the NP-complete clique decision problem. The most well-known algorithm to solve this problem has been proposed by Bron & Kerbosch (BK). Generalizing this algorithm to hypergraphs presents significant challenges and admits multiple solutions. The primary difficulty stems from the fundamental difference in structure: while in standard graphs a vertex has a bounded number of incident edges, in hypergraphs a vertex can participate in an exponential number of hyperedges. Specifically, in a hypergraph with$n$vertices where hyperedges have arity$r$, a single vertex may belong to up to$\binom{n-1}{r-1}$hyperedges. This structural complexity renders the direct generalization of BK computationally inefficient. In this article, we propose three new approaches to solve the MHE problem. First, a relaxation method based on the relaxation of a hypergraph in a graph. Then, a method based on an efficiently computation of the hypercliques containing a set of vertices. Finally, a method combining the previous ones. We conducted an experimental study on a set of benchmarks, showing one or two orders of magnitude performance improvements of our approach with regards to the direct generalization of BK to hypergraphs.

As more and more data is generated and stored, and as longer data streams become available, concept drift detection is becoming crucial for most real world applications. We introduce Partially Supervised Drift Detection, PSDD, a drift detection method based on Decision Trees that does not suppose any knowledge of true class labels during inference. Our approach works in any number of dimensions and is able to distinguish real from virtual drift. We successfully evaluated our method with well established datasets in the drift detection field.

Bayesian optimization (BO) aims to minimize a given blackbox function using a model that is updated whenever new evidence about the function becomes available. Here, we address the problem of BO under partially right-censored response data, where in some evaluations we only obtain a lower bound on the function value. The ability to handle such response data allows us to adaptively censor costly function evaluations in minimization problems where the cost of a function evaluation corresponds to the function value. One important application giving rise to such censored data is the runtime-minimizing variant of the algorithm configuration problem: finding settings of a given parametric algorithm that minimize the runtime required for solving problem instances from a given distribution. We demonstrate that terminating slow algorithm runs prematurely and handling the resulting right-censored observations can substantially improve the state of the art in model-based algorithm configuration.

Fuzzing is a key tool used to reduce bugs in production software. At Google, fuzzing has uncovered tens of thousands of bugs. Fuzzing is also a popular subject of academic research. In 2020 alone, over 120 papers were published on the topic of improving, developing, and evaluating fuzzers and fuzzing techniques. Yet, proper evaluation of fuzzing techniques remains elusive. The community has struggled to converge on methodology and standard tools for fuzzer evaluation.

Modern SAT solvers have experienced a remarkable progress on solving industrial instances. It is believed that most of these successful techniques exploit the underlying structure of industrial instances. Recently, there have been some attempts to analyze the structure of industrial SAT instances in terms of complex networks, with the aim of explaining the success of SAT solving techniques, and possibly improving them. In this paper, we study the community structure, or modularity, of industrial SAT instances. In a graph with clear community structure, or high modularity, we can find a partition of its nodes into communities such that most edges connect variables of the same community. Representing SAT instances as graphs, we show that most application benchmarks are characterized by a high modularity. On the contrary, random SAT instances are closer to the classical Erdös-Rényi random graph model, where no structure can be observed. We also analyze how this structure evolves by the effects of the execution of a CDCL SAT solver, and observe that new clauses learned by the solver during the search contribute to destroy the original structure of the formula. Motivated by this observation, we finally present an application that exploits the community structure to detect relevant learned clauses, and we show that detecting these clauses results in an improvement on the performance of the SAT solver. Empirically, we observe that this improves the performance of several SAT solvers on industrial SAT formulas, especially on satisfiable instances.

Coverage-guided fuzz testing has gained prominence as a highly effective method of finding security vulnerabilities such as buffer overflows in programs that parse binary data. Recently, researchers have introduced various specializations to the coverage-guided fuzzing algorithm for different domain-specific testing goals, such as finding performance bottlenecks, generating valid inputs, handling magic-byte comparisons, etc. Each such solution can require non-trivial implementation effort and produces a distinct variant of a fuzzing tool. We observe that many of these domain-specific solutions follow a common solution pattern. In this paper, we present FuzzFactory, a framework for developing domain-specific fuzzing applications without requiring changes to mutation and search heuristics. FuzzFactory allows users to specify the collection of dynamic domain-specific feedback during test execution, as well as how such feedback should be aggregated. FuzzFactory uses this information to selectively save intermediate inputs, called waypoints, to augment coverage-guided fuzzing. Such waypoints always make progress towards domain-specific multi-dimensional objectives. We instantiate six domain-specific fuzzing applications using FuzzFactory: three re-implementations of prior work and three novel solutions, and evaluate their effectiveness on benchmarks from Google's fuzzer test suite. We also show how multiple domains can be composed to perform better than the sum of their parts. For example, we combine domain-specific feedback about strict equality comparisons and dynamic memory allocations, to enable the automatic generation of LZ4 bombs and PNG bombs.

Model Checking is at the heart of formal methods for software and hardware verification. In this area of active research, Bounded Model Checking (BMC) and k-induction have reached very impressive results, especially when both methods are working together. They are based on a common approach that unrolls the transition relation, but each method serves a different purpose in practice. BMC is usually used for bugs findings, while k-induction aims at building inductive invariants. The ZigZag approach, proposed 15 years ago, takes benefit from both strategies by successively calling each one of them, while trying to share a lot of information between calls thanks to the mechanism of SAT clauses learning. Despite the practical importance of the ZigZag algorithm, it was mainly used forwardly until last year. The transition relation was unrolled by increasing depths only. However, as stated by the authors of ZigZag themselves, it was possible to consider the ZigZag approach backwardly. The experimental study of backward zigzag performances was only proposed one year ago. In this paper, we propose to extend the idea of the ZigZag algorithm by allowing to unroll the transitions from the middle. This has the nice property of allowing the SAT solver to keep learnt clauses that are both close to the initial state and to the bad state in the search. Our experimental study however shows that the best option for ZigZag is still to perform it backward, as stated in a previous work. However, we also show that our hybrid approach offers the same performances as forward ZigZag, while allowing more flexible strategies to be developed in the future, for example by choosing the right transition to expand.

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 shed light on CDCL performance by using theoretical benchmarks, which 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 efficiently they search for proofs. We report results from extensive experiments on a wide range of benchmarks. Our findings include several examples where theory predicts and explains CDCL behaviour, but also raise a number of intriguing questions for further study.

Model Checking is an important formal method for software and hardware verification. Bounded Model Checking (BMC) and k-induction are both parameterized methods, often working together: BMC focus on bug finding, while k-induction searches for an inductive invariant. Both of them greatly rely on their underlying decision procedure, e.g. on their SAT/SMT solver. By construction, BMC and k-induction formulas can be partitioned into 3 sets, one of them being perfectly symmetric (w.r.t. the unrolling mechanism). We propose in this paper to efficiently take advantage of these symmetries in order to perform learnt clauses replications. Replicating learnt clauses was already suggested in the early years of BMC, but unfortunately abandoned because of its tendency to drown the solver with too many clauses. Recently, constraints replication has been extended to temporal induction, a technique that combines BMC and k-induction, using assumption literals to detect replicable clauses. We propose to revisit constraints replications for temporal induction in a number of new ways. First, we highlight that adding assumption literals to transition relations, as it was done recently, have a non-negligible negative impact in practice. Then, we confirm that the replication of too many clauses in the learnt clause database is also prejudicial in most of the cases, even in temporal induction. Hence, we propose to limit the replication to external (outside the solver) replication only. This allows an even simpler strategy to detect replicable clauses, which requires almost no modification of both the SAT solver and the encoding strategy used in the model checker. Then, we show that, by carefully selecting learnt clauses to replicate, we improve our model checker performance, thus challenging the common belief about clauses replications. As a last contribution, we show that ZigZag, an algorithm that combines BMC and k-induction inside a single solver, is more efficient when performed backward.

Recent attempts to create versions of Satisfiability (SAT) solversthat exploit parallel hardware and information sharing have met withlimited success. In fact,the most successful parallel solvers in recent competitions were basedon portfolio approaches with little to no exchange of informationbetween processors. This experience contradicts the apparentparallelizability of exploring a combinatorial search space. Wepresent evidence that this discrepancy can be explained by studyingSAT solvers through a proof complexity lens, as resolution refutationengines. Starting with theobservation that a recently studied measure of resolution proofs,namely depth, provides a (weak) upper bound to the best possiblespeedup achievable by such solvers, we empirically show the existenceof bottlenecks to parallelizability that resolution proofs typicallygenerated by SAT solvers exhibit. Further, we propose a new measureof parallelizability based on the best-case makespan of an offlineresource constrained scheduling problem. This measureexplicitly accounts for a bounded number of parallel processors andappears to empirically correlate with parallel speedups observed inpractice. Our findings suggest that efficient parallelization of SATsolvers is not simply a matter of designing the right clause sharingheuristics; even in the best case, it can be --- and indeed is ---hindered by the structure of the resolution proofs current SAT solverstypically produce.

Modern complete SAT solvers almost uniformly implement variations of the clause learning framework introduced by Grasp and Chaff. The success of these solvers has been theoretically explained by showing that the clause learning framework is an implementation of a proof system which is as poweful as resolution. However, exponential lower bounds are known for resolution, which suggests that significant advances in SAT solving must come from implementations of more powerful proof systems. We present a clause learning SAT solver that uses extended resolution. It is based on a restriction of the application of the extension rule. This solver outperforms existing solvers on application instances from recent SAT competitions as well as on instances that are provably hard for resolution.

In a peer-to-peer inference system, each peer can reason locally but can also solicit some of its acquaintances, which are peers sharing part of its vocabulary. In this paper, we consider peer-to-peer inference systems in which the local theory of each peer is a set of propositional clauses defined upon a local vocabulary. An important characteristic of peer-to-peer inference systems is that the global theory (the union of all peer theories) is not known (as opposed to partition-based reasoning systems). The main contribution of this paper is to provide the first consequence finding algorithm in a peer-to-peer setting: DeCA. It is anytime and computes consequences gradually from the solicited peer to peers that are more and more distant. We exhibit a sufficient condition on the acquaintance graph of the peer-to-peer inference system for guaranteeing the completeness of this algorithm. Another important contribution is to apply this general distributed reasoning setting to the setting of the Semantic Web through the Somewhere semantic peer-to-peer data management system. The last contribution of this paper is to provide an experimental analysis of the scalability of the peer-to-peer infrastructure that we propose, on large networks of 1000 peers.