ABSTRACT. We shed new light on the Literal Block Distance (LBD) and glue-based heuristics used in current SAT solvers. For this, we first introduce the concept of stickiness: given a run of a CDCL SAT solver, for each pair of literals we define, by a real value between 0 and 1, how sticky they are, basically, how frequently they are set at the same decision level. By means of a careful and detailed experimental setup and analysis, we confirm the following quite surprising fact: given a SAT instance, when running different CDCL SAT solvers on it, no matter their settings or random seeds, the stickiness relation between literals is always very similar, in a precisely defined sense. We analyze how quickly stickiness stabilizes in a run (quite quickly), and show that it is stable even under different encodings of cardinality constraints. We then describe how and why these solid new insights lead to heuristics refinements for SAT (and extensions, such as SMT) and improved information sharing in parallel solvers.

ABSTRACT. Satisfiability (SAT) solving has become an important technology in computer-aided mathematics with various successes in number and graph theory. In this paper we apply SAT solvers to color infinitely long strips in the plane with a given height and number of colors. The coloring is constrained as follows: two points that are exactly unit distance apart must be colored differently. To finitize the problem, we tile the strips and all points on a tile have the same color. We evaluated our approach using two different tile shapes: squares and hexagons. We were able to increase the lower bound for the strip height with 5 colors. The visualization of strips using 3 to 6 colors reveal patterns that are similar to the best known lower bounds.

ABSTRACT. Motivated by Gromov’s subgroup conjecture (GSC), a fundamental open conjecture in the area of geometric group theory, we tackle the problem of the existence of particular types of subgroups---arising from so-called periodic apartments---for a specific set of hyperbolic groups with respect to which GSC is currently open. This problems is equivalent to determining whether specific types of graphs with a non-trivial combination of properties exist. The existence of periodic apartments allows for ruling the groups out as some of the remaining potential counterexamples to GSC. Our approach combines both automated reasoning techniques---in particular, Boolean satisfiability (SAT) solving---with problem-specific orderly generation. Compared to earlier attempts to tackle the problem through computational means, our approach scales several magnitudes better, and allows for both confirming results from a previous computational treatment for smaller parameter values as well as ruling out further groups out as potential counterexamples to GSC.

ABSTRACT. Based our formal framework for CDCL (conflict-driven clause learning) using the proof assistant Isabelle\slash HOL, we verify an extension of CDCL computing cost-minimal models called OCDCL. It is based on branch and bound and computes models of minimal cost with respect to total valuations. The verification starts by developing a framework for CDCL with branch and bound, called \CDCLBaB{}, which is then instantiated to get OCDCL. We then apply our formalization to three different applications. Firstly, through the dual rail encoding, we reduce the search for cost-optimal models with respect to partial valuations to searching for total cost-optimal models, as derived by OCDCL. Secondly, we instantiate OCDCL to solve MAX-SAT, and, thirdly, \CDCLBaB{} to compute a set of covering models. A large part of the original CDCL verification framework could be reused without changes to reduce the complexity of the new formalization. To the best of our knowledge, this is the first rigorous formalization of CDCL with branch and bound, and its application to an optimizing CDCL calculus and the first solution that computes cost-optimal models with respect to partial valuations.

ABSTRACT. The paper describes a deep reinforcement learning framework based on self-supervised learning within the proof assistant HOL4. A close interaction between the machine learning modules and the HOL4 library is achieved by the choice of tree neural networks (TNNs) as machine learning models and the internal use of HOL4 terms to represent tree structures of TNNs. Recursive improvement is possible when a task is expressed as a search problem. In this case, a Monte Carlo Tree Search (MCTS) algorithm guided by a TNN can be used to explore the search space and produce better examples for training the next TNN. As an illustration, term synthesis tasks on combinators and Diophantine equations are specified and learned. The success rate on test sets generated for each task is respectively 65% and 78.5%. These results are compared with state-of-the-art ATPs on combinators and set a precedent for statistically guided synthesis of Diophantine equations.

ABSTRACT. We present a system that utilizes machine learning for proof search in the Coq theorem prover. In a similar vein as the TacticToe project for HOL4, our system predicts appropriate tactics and finds proofs in the form of tactic scripts. This is done by learning from previous tactic scripts, and how they are applied to proof states. An evaluation of our system was performed on the Coq Standard Library. In its current state, our predictor can identify the correct tactic to be applied on a goal 23.5% of the time. Our proof searcher can fully automatically prove 39.3% of the lemmas in the library.

ABSTRACT. This paper presents a novel algorithm for automatically learning recursive shape predicates from memory graphs, so as to formally describe the pointer-based data structures contained in a program. These predicates are expressed in separation logic and can be used, e.g., to construct efficient secure wrappers that validate the shape of data structures exchanged between trust boundaries at runtime. Our approach first decomposes memory graph(s) into sub-graphs, each of which exhibits a single data structure, and generates candidate shape predicates of increasing complexity, which are expressed as rule sets in Prolog. Under separation logic semantics, a meta-interpreter then performs a systematic search for a subset of rules that form a shape predicate that non-trivially and concisely captures the data structure. Our algorithm is implemented in the prototype tool ShaPE and evaluated on examples from the real-world and the literature. It is shown that our approach indeed learns concise predicates for many standard data structures and their implementation variations, and thus alleviates software engineers from what has been a time-consuming manual task.

ABSTRACT. The triguarded fragment of first-order logic is an extension of the guarded fragment in which quantification for subformulas with at most two variables need not be guarded. Thus, it unifies two prominent decidable logics: the guarded fragment and the two-variable fragment. Its satisfiability problem is known to be undecidable in the presence of equality, but becomes decidable when equality is forbidden. We consider an extension of the triguarded fragment without equality by transitive relations, allowing them to be used only as guards. We show that the satisfiability problem for the obtained formalism is decidable and 2ExpTime-complete, that is, it is of the same complexity as for the analogous extension of the classical guarded fragment. In fact, in our satisfiability test we use a decision procedure for the latter as a subroutine. We also show how our approach, consisting in exploiting some existing results on guarded logics, can be used to reprove some known facts, as well as to derive some new results on triguarded logics.

ABSTRACT. Inprocessing techniques have become one of the most promising advancements in SAT solving over the last decade. Some inprocessing techniques modify a propositional formula in non model-perserving ways. These operations are very problematic when Craig interpolants must be extracted: existing methods take resolution proofs as an input, but these inferences require stronger proof systems; state-of-the-art solvers generate DRAT proofs. We present the first method to transform DRAT proofs into resolution-like proofs by eliminating satisfiability-preserving RAT inferences. This solves the problem of extracting interpolants from DRAT proofs.

ABSTRACT. Globalization of integrated circuits manufacturing has led to increased security concerns, notably IP theft. In response, many logic locking techniques have been developed for protecting designs, but many of these locking techniques have been shown to be vulnerable to SAT attacks. In this paper, we explore the use of Boolean sensitivity to analyze circuits locked with these techniques. We show that in typical circuits there is an inverse relationship between input width and sensitivity. We then demonstrate the utility of this relationship for deobfuscating circuits locked with a class of ``provably secure'' logic locking techniques. We conclude with an example of how to resist this attack, although the resistance is shown to be highly circuit dependent.

ABSTRACT. In this paper we propose a number of powerful logics for information sharing and acts of publicly or privately accessing other agents' information databases. The static base of our logics builds on the already existing work in epistemic logic, in particular on the concepts of distributed knowledge and common knowledge. We assume that information is distributed in a number of information sources or `sites' (e.g. files, folders, data sets, websites, databases etc) at a given time. Each source can itself be thought of as being associated with an agent, either because it is actually the knowledge base of a real agent (natural or artificial), or simply because we think of the source itself as an abstract or virtual `agent' (possessing exactly the information that is locally stored at that site). Distributed knowledge of a group is the sum total of all (that follows from) the information possessed by any of the agents in the group, while common knowledge is only the information possessed in common by these agents. Distributed knowledge can be `actualized' or `resolved', i.e. converted into common knowledge, by full communication within the group. We axiomatize a new concept of ``common distributed knowledge" within a family of (sub)groups of agents, that lies somewhere in between the two, and can be actualized into full common knowledge by much less communication (namely, only within each subgroup). We also consider an extension of this logic with comparative epistemic assertions for individuals (``agent $b$ knows everything known to agent $c$") or groups (``group $B$ has distributed knowledge of everything known to group $C$").

On this static base, we built communication logics obtained by adding various dynamic operators for information sharing, public or private accessing etc. An agent may gain access to a number of sources, after which it can be assumed to instantly `read' all the information stored at that site, i.e. it `learns' everything that was known by the source agent. The `reading' agent gains access to a source either because it is granted such access by the source agent itself (by ``sharing" her database, in which case it is natural to assume that the source `knows' it is being accessed), or because it somehow succeeded to illegally gain such access via e.g. hacking, in which case typically the source doesn't know it's being accessed (although sometimes it does get to know it, either because the hacker publicizes all the stolen information, or because somehow the source agents is able to detect the hacking). So a reading action can be public (when it is common knowledge that it occurs) or secret, or semi-public (visible only to some agents). Multiple agents may simultaneously access multiple sources. After each such reading action, each reading agent knows everything that was known by its source agents.

We completely axiomatize several of these logics, prove their decidability, and end with a few open questions.

ABSTRACT. Deep neural networks (DNNs) are revolutionizing the way complex systems are designed, developed and maintained. As part of the life cycle of DNN-based systems, there is often a need to modify a DNN in subtle ways that affect certain aspects of its behavior, while leaving other aspects of its behavior unchanged (e.g., if a bug is discovered and needs to be fixed, without altering other functionality). Unfortunately, retraining a DNN is often difficult and expensive, and may produce a new DNN that is quite different from the original. We leverage recent advances in DNN verification and propose a technique for modifying a DNN according to certain requirements, in a way that is provably minimal, does not require any retraining, and is thus less likely to affect other aspects of the DNN’s behavior. Using a proof-of-concept implementation, we demonstrate the usefulness and potential of our approach in addressing two real-world needs: (i) measuring the resilience of DNN watermarking schemes; and (ii) bug repair in already-trained DNNs.

ABSTRACT. Isabelle/HOL augments classical higher-order logic with ad-hoc overloading of constant definitions---that is, one constant may have several definitions for non-overlapping types. In this paper, we present a mechanised proof that HOL with ad-hoc overloading is consistent. All our results have been formalised in the HOL4 theorem prover.