ABSTRACT. Progress in satisfiability (SAT) solving has made it possible to determine the correctness of complex systems and answer long-standing open questions in mathematics. The SAT-solving approach is completely automatic and can produce clever though potentially gigantic proofs. We can have confidence in the correctness of the answers because highly trustworthy systems can validate the underlying proofs regardless of their size.

We demonstrate the effectiveness of the SAT approach by presenting some recent successes, including the solution of the Boolean Pythagorean Triples problem, computing the fifth Schur number, and resolving the remaining case of Keller’s conjecture. Moreover, we constructed and validated proofs for each of these results. The second part of the talk focuses on notorious math challenges for which automated reasoning may well be suitable. In particular, we discuss advances in applying SAT-solving techniques to the Hadwiger-Nelson problem (chromatic number of the plane), optimal schemes for matrix multiplication, and the Collatz conjecture.

ABSTRACT. Radio 2-colorings of graphs are a generalization of vertex colorings motivated by the problem of assigning frequency channels in radio networks. In a radio 2-coloring of a graph, vertices are assigned integer colors so that the color of two vertices u and v differ by at least 2 if u and v are neighbors, and by at least 1 if u and v have a common neighbor. Our work improves the best-known bounds for optimal radio 2-colorings of small hypercube graphs, a combinatorial problem that has received significant attention in the past. We do so by using automated reasoning techniques such as symmetry breaking and Cube and Conquer, obtaining that for n = 7 and n = 8, the coding-theory upper bounds of Whittlesey et al. (1995) are not tight. Moreover, we prove the answer for n=7 to be either 12 or 13, thus making a substantial step towards answering an open problem by Knuth (2015). Finally, we include several combinatorial observations that might be useful for further progress, while also arguing that fully determining the answer for n=7 is currently out of reach.

ABSTRACT. Unit propagation and conflict analysis are two essential ingredients of CDCL SAT Solving. The order in which unit propagation is computed does not matter when no conflict is found, because it is well known that there exists a unique unit-propagation fixpoint. However, when a conflict is found, current CDCL implementations stop and analyze that concrete conflict, even though other conflicts may exist in the unit-propagation closure.

In this experimental evaluation, we report on our experience in modifying this concrete aspect in the CaDiCaL SAT Solver and try to answer the question of whether we can improve the performance of SAT Solvers by the analysis of multiple conflicts.

ABSTRACT. The family of SCL (Clause Learning from Simple Models) calculi learns clauses with respect to a partial model assumption, similar to CDCL (Conflict Driven Clause Learning). The partial model always consists of ground first-order literals and is built by decisions and propagations. In contrast to propositional logic where propagation chains are always finite, in first-order logic they can become infinite. Therefore, the SCL family does not require exhaustive propagation and the size of the partial model is always finitely bounded. Any partial model not leading to a conflict constitutes a model for the respective finitely bounded ground clause set. We show that all potential partial models can be explored as part of the SCL calculus for first-order logic without equality and that any overall model is an extension of a partial model considered. Furthermore, SCL turns into a semi-decision procedure for first-order logic by extending the finite bound for any partial model not leading to a conflict.

ABSTRACT. Clause selection is a crucial choice point in modern saturation-based automatic theorem provers. A standard heuristic advises selecting small clauses, i.e., clauses with few symbol occurrences. More generally, we can prefer clauses with a small weighted symbol occurrence count, where each symbol’s occurrence count gets multiplied by a respective symbol weight. A human domain expert would traditionally supply the symbol weights. In this paper, we propose a system based on a graph neural network (GNN) that learns to predict these symbol weights to boost clause selection on an arbitrary first-order logic problem. Our experiments show that advising the automatic theorem prover Vampire on the first-order fragment of TPTP using a trained neural network allows the prover to solve 2.9 % more problems than weighting symbols uniformly.

ABSTRACT. In this work we extend an instantiation-based theorem prover iProver with machine learning (ML) guidance based on graph neural networks. For this we implement an interactive mode in iProver, which allows communication with an external agent via network sockets. The external (ML-based) agent guides the proof search by scoring generated clauses in the given clause loop. Our evaluation on a large set of Mizar problems shows that the ML guidance outperforms iProver's standard human-programmed priority queues, solving more than twice as many problems in the same time. To our knowledge, this is the first time the performance of a state-of-the-art instantiation-based system is doubled by ML guidance.

ABSTRACT. With respect to the number of variables the border of decidability lies between 2 and 3: the two-variable fragment, FO2, of first-order logic has an exponential model property and hence NExpTime-complete satisfiability problem, while for the three-variable fragment, FO3, satisfiability is undecidable. In this paper we propose a rich fragment of FO3 without equality, containing full FO2 without equality, and show that it retains the finite model property and NExpTime complexity. The fragment is obtained as an extension of the uniform one-dimensional fragment with three-variables.

ABSTRACT. Declarative programming, functional or logic, has been used for system's specification purposes, including the formal specification of programming languages. Given the formal specification of the operational semantics of a programming language we have an executable operational semantics, i.e. we have an interpreter for that programming language. Starting from a basic specification of the operational semantics of Java written in Maude, a logical framework and a programming language, we could develop an information flow extension of this Java semantics which would allow us to observe if program computation fulfills some information-flow security properties, for instance privacy. Then we could develop in Maude an abstract, finite-state version of the information-flow operational semantics which would supports finite program verification. A logic program execution can be seen as a logic inference from the logic program statements, by using language based logic. In this way Maude can be used not only for the verification of properties of Java programs but also for the formal certification of the verified properties of the Java programs. As a byproduct of the verification, a certificate of information-flow security properties is thus delivered which consists of a set of (abstract) rewriting proofs that can be checked by the code consumer using a standard rewriting logic engine. We have considered some information-flow privacy specific policies non-interference, erasure and relaxed non interference with declassification.