LPAR 2024: 25TH CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING
Accepted Papers

S. Akshay (IIT Bombay)
Supratik Chakraborty (IIT Bombay)
Amir Kafshdar Goharshady (Hong Kong University of Science and Technology)
R Govind (Uppsala University)
Harshit Jitendra Motwani (Ghent University)
Sai Teja Varanasi (IIT Bombay)
Automated Synthesis of Decision Lists for Polynomial Specifications over Integers

ABSTRACT. In this work, we consider two sets I and O of bounded integer variables, modeling the inputs and outputs of a program. Given a specification Post, which is a Boolean combination of linear or polynomial inequalities with real coefficients over I ∪ O, our goal is to synthesize the weakest possible pre-condition Pre and a program P satisfying the Hoare triple {Pre}P{Post}. We provide a novel, practical, sound and complete algorithm, based on dynamic gridding, Farkas’ Lemma and Handelman’s Theorem, that synthesizes both the program P and the pre-condition Pre, over a bounded integral region. Our approach is exact and guaranteed to find the weakest pre-condition. Moreover, it always synthesizes both P and Pre as linear decision lists. Thus, our output consists of simple programs and pre-conditions that facilitate further static analysis. We also provide experimental results over benchmarks showcasing the real-world applicability of our approach and considerable performance gains over the state-of-the-art.

Kristina Aleksandrova (University of Innsbruck)
Jan Jakubuv (University of Innsbruck)
Cezary Kaliszyk (University of Innsbruck)
Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery

ABSTRACT. While many of the state-of-art Automated Theorem Provers (ATP) like E and Vampire, were subject to extensive tuning of strategy schedules in the last decade, the classical ATP prover Prover9 has never been optimized in this direction. Both E and Vampire provide the user with an automatic mode to select good proof search strategies based on the properties of the input problem, while Prover9 provides by default only a relatively weak auto mode. Interestingly, Prover9 provides more varied means for proof control than its competitors. These means, however, must be manually investigated and that is possible only by experienced Prover9 users with a good understanding of how Prover9 works.

In this paper, we investigate the possibilities of automatic configuration of Prover9 for user-specified benchmark problems. We employ the automated strategy invention system Grackle to generate Prover9 strategies with both basic and advanced proof search options which require sophisticated strategy space features for Grackle. We test the strategy invention on AIM train/test problem collection and we show that Prover9 can outperform both E and Vampire on these problems. To test the generality of our approach we train and evaluate strategies also on TPTP problems, showing that Prover9 can achieve reasonable complementarity with other ATPs.

Pablo Barenbaum (Universidad Nacional de Quilmes (CONICET) and ICC, Universidad de Buenos Aires)
Delia Kesner (Université Paris Cité)
Mariana Milicich (Université Paris Cité)
Hybrid Intersection Types for PCF

ABSTRACT. Intersection type systems have been independently applied to different evaluation strategies, such as call-by-name (CBN) and call-by-value (CBV). These type systems have been generalized to different subsuming paradigms being able, in particular, to encode CBN and CBV in a unique unifying framework. However, there are no intersection type systems that explicitly enable CBN and CBV to cohabit together without making use of an encoding into a common target framework. This work proposes an intersection type system for PCF with a specific notion of evaluation, called PCFH. Although this form of evaluation is sometimes referred to as “call-by-value”, evaluation in PCFH actually has a hybrid nature, in the sense that CBN and CBV operational behaviors cohabit together. Indeed, PCFH combines a CBV-like operational behavior for function application with a CBN-like behavior for recursion. This hybrid nature is reflected in the type system, which turns out to be sound and complete with respect to PCFH: not only that typability implies normalization, but also the converse holds. Moreover, the type system is quantitative, in the sense that the size of typing derivations provides upper bounds for the length of the normalization sequences to normal form. This type system is then refined to a tight one, offering exact information regarding the length of normalization sequences.

Translating HOL-Light proofs to Coq

ABSTRACT. We present a method and a tool, hol2dk, to automatically translate proofs from the proof assistant HOL-Light to the proof assistant Coq, by using Dedukti as intermediate language. Moreover, a number of types, functions and predicates that are defined in HOL-Light are mapped to their counterparts in the Coq standard library, and these mappings are certified in Coq. Therefore, the obtained library can directly be used and applied in other Coq developments.

Martin Bromberger (Max Planck Institute for Informatics)
Simon Schwarz (Max Planck Institute for Informatics)
Christoph Weidenbach (Max Planck Institute for Informatics)
Automatic Bit- and Memory-Precise Verification of eBPF Code

ABSTRACT. We propose a translation from eBPF (extended Berkeley Packet Filter) code to CHC (Constrained Horn Clause sets) over the combined theory of bitvectors and arrays. eBPF is in particular used in the Linux kernel where user code is executed under kernel privileges. In order to protect the kernel, a well-known verifier statically checks the code for any harm and a number of research efforts have been performed to secure and improve the performance of the verifier. This paper is about verifying the functional properties of the eBPF code itself. Our translation procedure bpfverify is precise and covers almost all details of the eBPF language. Functional properties are automatically verified using z3. We prove termination of the procedure and show by real world eBPF code examples that full-fledged automatic verification is actually feasible.

Mark Chimes (TU Wien)
Radu Iosif (Verimag, CNRS, University of Grenoble Alpes)
Florian Zuleger (TU Wien)
Tree-Verifiable Graph Grammars

ABSTRACT. Hyperedge-Replacement grammars (HR) have been introduced by Courcelle in order to extend the notion of context-free sets from words and trees to graphs of bounded tree-width. While for words and trees syntactic grammar restrictions are known that guarantee that the associated languages of words resp. trees are regular - and hence, MSO definable - the situation is more complicated for graphs. Here, Courcelle proposed the notion of regular graph grammars, a syntactic restriction of HR grammars that guarantees the definability of the associated languages of graphs in Counting Monadic Second Order Logic (CMSO). However, these grammars are not complete in the sense that not every CMSO definable set of graphs of bounded tree-width can be generated by a regular graph grammar. In this paper, we introduce a new syntactic restriction of HR grammars, called tree-verifiable graph grammars, and a new notion of bounded tree-width, called embeddable bounded tree-width, where the later restricts the trees of a tree-decomposition to be a subgraph of the analyzed graph. The main property of tree-verifiable graph grammars is that their associated languages are CMSO definable and that the have bounded embeddable tree-width. We show further that they strictly generalize the regular graph grammars of Courcelle. Finally, we establish a completeness result, showing that every language of graphs that is CMSO definable and of bounded embeddable tree-width can be generated by a tree-verifiable graph grammar.

Luís Cruz-Filipe (Dept. of Mathematics and Computer Science, University of Southern Denmark)
Peter Schneider-Kamp (University of Southern Denmark)
Minimizing Sorting Networks at the Sub-Comparator Level

ABSTRACT. Sorting networks are sorting algorithms that execute a sequence of operations independently of the input. Since they can be implemented directly as circuits, sorting networks are easy to implement in hardware -- but they are also used often in software to improve performance of base cases of standard recursive sorting algorithms. For this purpose, they are translated them into machine-code instructions in a systematic way.

Recently, a deep-learning system discovered better implementations than previously known of some sorting networks with up to 8 inputs. In this article, we show that all these examples are instances of a general pattern whereby some instructions are removed. We show that this removal can be done when a particular set of constraints on integers is satisfiable, and identify conditions where we can reduce this problem to propositional satisfiability. We systematically apply this general construction to improve the best-known implementations of sorting networks of size up to 128, which are the ones most commonly found in software implementations.

Katalin Fazekas (TU Wien)
Florian Pollitt (University of Freiburg)
Mathias Fleury (University of Freiburg)
Armin Biere (University of Freiburg)
Certifying Incremental SAT Solving

ABSTRACT. Certifying results by checking proofs and models is an essential feature of modern SAT solving. Even though incremental solving with assumptions and core extraction is crucial for many applications support for incremental proof certificates is lacking. We propose a proof format for incremental SAT solving and corresponding checkers. We further extend it to make use of resolution hints. Experiments on incremental SAT solving for satisfiability modulo theories and bounded model checking show the feasibility of our approach, again also confirming that resolution hints substantially reduce checking time.

Christian Fermüller (Vienna University of Technology)
Robert Freiman (Vienna University of Technology)
Timo Lang (University College London)
A Simple Token Game and its Logic

ABSTRACT. We introduce a simple game of resource-conscious reasoning. In this two-player game, players Proponent and Opponent simultaneously place tokens of positive and negative polarity onto a game board. Proponent wins if she manages to match every negative token with a corresponding positive token.

We study the game using methods from computational complexity and proof theory. Specifically, we show complexity results for various fragments of the game, including PSPACE-completeness of a finite restriction of the game and undecidability of the full game featuring infinite plays. Determinacy, that is the existence of a winning strategy for one of the players, can be shown for the full game. Moreover, we show that the finitary version of the game is axiomatisable and can be faithfully embedded into exponential-free linear logic. The full game satisfies the exponential rules of linear logic, but is not fully captured by it.

Robert Freiman (Vienna University of Technology)
Carlos Olarte (LIPN, Université Sorbonne Paris Nord)
Elaine Pimentel (UCL)
Christian Fermüller (Vienna University of Technology)
Reasoning About Group Polarization: From Semantic Games to Sequent Systems

ABSTRACT. Group polarization, the phenomenon where individuals' opinions become more extreme after interacting, has gaining attention, specially with the rise of social media influencing social, political, and democratic processes. Recent interest has emerged in formal reasoning about group polarization using logical systems. In this paper we consider the modal logic PNL that captures the notion of agents agreeing or disagreeing on a given topic.Our contribution is to endow PNL with more effective formal reasoning techniques, instead of reasoning about group polarization using Hilbert axiomatic systems. First, we introduce a semantic game for (hybrid) extensions of PNL, which supports a dynamic form of reasoning about concrete network models. We show how this semantic game leads to a provability game, by systemically exploring the truth in all models. This leads to the first Gentzen-style cut-free sequent systems for some variants of PNL. Interestingly enough, using polarization of formulas, the proposed sequent systems can be modularly adapted to consider different frame properties of the underlying model.

Pamina Georgiou (Vienna University of Technology)
Marton Hajdu (Vienna University of Technology)
Laura Kovács (TU Wien)
Sorting without Sorts

ABSTRACT. We present a reasoning framework in support of establishing the functional correctness of programs with recursive data structures with automated first-order theorem proving. Specifically, we focus on functional programs implementing sorting algorithms.

We formalize the semantics of recursive programs in many-sorted first-order logic while introducing sortedness/permutation properties as part of our first-order formalization. Rather than focusing on sorting lists of elements of specific first-order theories such as integer arithmetic, our list formalization relies on a sort parameter abstracting (arithmetic) theories and, hence, concrete sorts. Additionally we formalize the permutation property of lists in first-order logic in an effective way that allows to automatically discharge verification conditions of such algorithms purely by means of first-order theorem proving.

Proof search is powered by automated theorem proving: we adjust recent efforts for automating inductive reasoning in saturation-based first-order theorem proving. Importantly, we advocate a compositional reasoning approach for automating proofs by induction required to verify functional programs implementing and preserving sorting and permutation properties over parameterized list structures. We showcase the applicability of our framework over recursive sorting algorithms, including Mergesort and Quicksort; to this end, we turn first-order theorem proving into an automated verification engine by guiding automated inductive reasoning with manual proof splits.

Giulio Guerrieri (University of Sussex)
Giulia Manara (Institut de Mathématiques de Marseille, Aix-Marseille Université)
Lorenzo Tortora de Falco (Università Roma Tre)
Lionel Vaux Auclair (Aix Marseille Université)
Confluence for Proof-Nets via Parallel Cut Elimination

ABSTRACT. We provide the first proof of confluence for cut elimination in multiplicative-exponential linear logic proof-nets that is not based on Newman's lemma or strong normalization, not even indirectly. To achieve our goal, we take inspiration from Tait and Martin-Lof's method based on parallel reduction for the lambda-calculus, even though the wilder realm of untyped proof-nets makes the proof subtler and more challenging.

Marton Hajdu (TU Wien)
Laura Kovács (TU Wien)
Michael Rawson (TU Wien)
Rewriting and Inductive Reasoning

ABSTRACT. Rewriting techniques based on reduction orderings generate “just enough” consequences to retain first-order completeness. This is ideal for superposition-based first-order theorem proving, but for at least one approach to inductive reasoning we show that we are missing crucial consequences. We therefore extend the superposition calculus with rewriting-based techniques to generate sufficient consequences for automating induction in saturation. When applying our work within the unit-equational fragment, our experiments with the theorem prover Vampire show significant improvements for inductive reasoning.

Rolf Hennicker (LMU Munich)
Alexander Knapp (University of Augsburg)
Martin Wirsing (LMU Munich)
Symbolic Realisation of Epistemic Processes

ABSTRACT. Epistemic processes describe the dynamic behaviour of multi-agent systems driven by the knowledge of agents, which perform epistemic actions that may lead to knowledge updates. Executing epistemic processes directly on epistemic states, given in the traditional way by pointed Kripke structures, quickly becomes computationally expensive due to the semantic update constructions. Based on an abstraction to formulae of interest, we introduce a symbolic epistemic state representation and a notion of representable epistemic action with efficient symbolic updates. In contrast to existing work on belief or knowledge bases, our approach can handle epistemic actions modelled by arbitrary action models. We introduce an epistemic process calculus and a propositional dynamic logic for specifying process properties that can be interpreted both on the concrete semantic and the symbolic level. We show that our abstraction technique preserves and reflects dynamic epistemic process properties whenever processes are started in a symbolic state that is an abstraction of a semantic epistemic state.

Aaron Hunter (British Columbia Institute of Technology)
Alberto Iglesias (British Columbia Institute of Technology)
A Tool for Reasoning about Trust and Belief

ABSTRACT. We introduce a software tool for reasoning about belief change in situations where information is received from reports and observations. Our focus is on the interaction between trust and belief. The software is based on a formal model where the level of trust in a reporting agent increases when they provide accurate reports and it decreases when they provide innaccurate reports. If trust in an agent drops below a given threshold, then their reports no longer impact our beliefs at all. The notion of accuracy is determined by comparing reports to observations, as well as to reports from more trustworthy agents. The emphasis of this paper is not on the formalism; the emphasis is on the development of the prototype system for automatically calculating the result of iterated revision problems involving trust. We present an implemented system that allows users to flexibly specify and solve complex revision problems involving reports from partially trusted sources.

Ozan Kahramanogullari (Free Unversity of Bolzano-Bozen, Faculty of Computer Science)
Deep Inference in Proof Search: The Need for Shallow Inference

ABSTRACT. Deep inference is a proof theoretical formalism that generalises the “shallow inference” of the sequent calculus by permitting the application of inference rules like term rewriting rules. Deep inference makes it possible to access shorter proofs than sequent calculus; however, with the cost of increased nondeterminism, an obstacle in front of proof search applications. Deep inference is essential for designing system BV, an extension of multiplicative linear logic (MLL) with a self-dual non-commutative operator. MLL has shallow inference systems, whereas BV is impossible with a shallow-only system. As Tiu showed, any restriction on rule depth makes a system incomplete for BV. This paper shows that any restriction that rules out shallow rules makes the system incomplete, too. Our results indicate that for system BV, shallow and deep rules must coexist for completeness. We provide extensive empirical evidence that deep inference can still be faster than shallow inference when used strategically with a proof theoretical technique for reducing nondeterminism. We show that prioritising deeper rule instances reduces the cost of proof search by reducing the size of the managed contexts, consequently providing more immediate access to shorter proofs. Moreover, we identify a class of MLL formulae with deep inference proof search times that grow linearly in the number of atoms in contrast to an exponential growth pattern with shallow inference. We introduce a large and exhaustive benchmark for MLL, with and without mix, and a proof search framework to apply various search strategies, which should be of independent interest.

Matthias Lanzinger (TU Wien)
Stefano Sferrazza (University of Oxford)
Przemysław Andrzej Wałęga (University of Oxford)
Georg Gottlob (University of Calabria)
Fuzzy Datalog$^\exists$ over Arbitrary t-norms

ABSTRACT. One of the main challenges in the area of Neuro-symbolic AI is to perform logical reasoning in the presence of neural and symbolic datasets. This requires the combination of heterogeneous data sources such as knowledge graphs, neural model predictions, structured databases, crowd-sourced data, and many more. In this paper we introduce $t$-Datalog$^\exists$ as a formalism for such reasoning tasks, $t$-Datalog$^\exists$ generalises of Datalog with existential rules or Datalog$^\exists$ (also commonly referred to as tuple-generating dependencies) by allowing the use of arbitrary t-norms in place of classical conjunction in rule bodies. The resulting formalism combines the best of both worlds. It extends the power and flexibility of Datalog$^\exists$ to neuro-symbolic reasoning tasks while preserving many of the desirable properties of the classical case. In particular, we show that natural extensions of the chase to our setting produces \emph{fuzzy universal models}, and that the complexity of reasoning in important decidable fragments remains the same as in the classical setting.

Anela Lolic (TU Wien)
Matthias Baaz (Technische Universität Wien)
On Translations of Epsilon Proofs to LK

ABSTRACT. The epsilon calculus gives the impression to provide shorter proofs than other proof mechanisms. Consequently, Toshio Arai asked "What is the expense to translate a derivation with cuts in the sequent formulation of epsilon calculus to LK derivations with cuts?". We provide as partial answer to the question a proof that there is no function Psi such that a cut-free derivation in a sequent calculus variant of the epsilon calculus with size n can be elementarily translated to an LK derivation with size and cut degree Psi(n). The main property of the epsilon calculus used is its ability to overbind bound variables.

Anela Lolic (TU Wien)
Alexander Leitsch (Institute of Computer Languages (E185), TU Wien)
Herbrand's Theorem in Inductive Proofs

ABSTRACT. An inductive proof can be represented as a proof schema, i.e. as a parameterized sequence of proofs defined in a primitive recursive way. A corresponding cut-elimination method, called schematic CERES, can be used to analyze these proofs, and to extract their (schematic) Herbrand sequents, even though Herbrand's theorem in general does not hold for proofs with induction inferences. This work focuses on the most crucial part of the schematic cut-elimination method, which is to construct a refutation of a schematic formula that represents the cut-structure of the original proof schema. Moreover, we show that this new formalism allows the extraction of a structure from the refutation schema, called a Herbrand schema, which represents its Herbrand sequent.

Lachlan McGinness (Australian National University)
Peter Baumgartner (CSIRO)
Automated Theorem Provers Help Improve Large Language Model Reasoning

ABSTRACT. In this paper we demonstrate how logic programming systems and Automated first-order logic Theorem Provers (ATPs) can improve the accuracy of Large Language Models (LLMs) for logical reasoning tasks where the baseline performance is given by direct LLM solutions. We first evaluate LLM reasoning on steamroller problems using the PRONTOQA benchmark. We show how accuracy can be improved with a neuro-symbolic architecture where the LLM acts solely as a front-end for translating a given problem into a formal logic language and an automated reasoning engine is called for solving it. However, this approach critically hinges on the correctness of the LLM translation. To assess this translation correctness, we secondly define a framework of syntactic and semantic error categories. We implemented the framework and used it to identify errors that LLMs make in the benchmark domain. Based on these findings, we thirdly extended our method with capabilities for automatically correcting syntactic and semantic errors. For semantic error correction we integrate first-order logic ATPs, which is our main and novel contribution. We demonstrate that this approach reduces semantic errors significantly and further increases the accurracy of LLM logical reasoning.

Mudathir Mahgoub Yahia Mohamed (University of Iowa)
Andrew Reynolds (University of Iowa)
Cesare Tinelli (The University of Iowa)
Clark Barrett (Stanford University)
Verifying SQL queries using theories of tables and relations

ABSTRACT. We present a number of first- and second-order extensions to SMT theories specifically aimed at representing and analyzing SQL queries with join, projection, and selection operations. We support rea- soning about SQL queries with either bag or set semantics for database tables. We provide the former via an extension of a theory of finite bags and the latter via an extension of the theory of finite relations. Fur- thermore, we add the ability to reason about tables with null values by introducing a theory of nullable sorts based on an extension of the the- ory of algebraic datatypes. We implemented solvers for these theories in the SMT solver cvc5 and evaluated them on two sets of benchmarks derived from public sets of SQL equivalence problems. A comparative evaluation with the state of the art in automated SQL verification shows competitive performance in the benchmarks we support. While follow- ing bag semantics cvc5 proves less benchmarks compared to SPES and SQLSolver tools, it finds counterexamples for inequivalent queries that are claimed to be proven by other tools. When analyzing the same set of benchmarks with set semantics, our implementation of cvc5 shows compelling advantages compared to SPES.

Naïm Moussaoui Remil (Inria Paris | École Normale Supérieure)
Caterina Urban (Inria Paris | École Normale Supérieure)
Antoine Miné (Sorbonne Université, CNRS, LIP6)
Automatic Detection of Vulnerable Variables for CTL Properties of Programs

ABSTRACT. We present our tool FuncTion-V for the automatic identification of the minimal sets of program variables that an attacker can control to ensure an undesirable program property. FuncTion-V supports program properties expressed in Computation Tree Logic (CTL), and builds upon an abstract interpretation-based static analysis for CTL properties that we extend with an abstraction refinement process. We showcase our tool on benchmarks collected from the literature and SV-COMP 2023.

Jelle Piepenbrock (Radboud University)
Mikolas Janota (Czech Technical University in Prague)
Josef Urban (Czech Technical University in Prague)
Jan Jakubův (Czech Technical University in Prague)
First Experiments with Neural CVC5

ABSTRACT. The CVC5 solver is today one of the strongest systems for solving first order problems with theories but also without them. In this work we equip the enumeration-based instantiation method with a neural network that guides the choice of instantiated quantifiers and their ground instances. For that we develop a relatively fast graph neural network that repeatedly scores all available instantiation options with respect to the available formulas. The network runs directly on a CPU without the need for any special hardware. We train the neural guidance on a large set of proofs generated by the e-matching instantiation strategy and evaluate its performance on a set of previously unseen problems.

Sophie Rain (TU Wien)
Lea Salome Brugger (ETH Zürich)
Anja Petković Komel (TU Wien)
Laura Kovács (TU Wien)
Michael Rawson (TU Wien)
Scaling Game-Theoretic Security Reasoning

ABSTRACT. We present the CheckMate tool for the automated verification of game-theoretic security properties, with application to blockchain protocols. CheckMate applies automated reasoning techniques to determine whether a game-theoretic protocol model is game-theoretically secure, that is, Byzantine fault tolerant and incentive compatible. We describe CheckMate’s input format and its various components, modes, and output. CheckMate is evaluated on 14 benchmarks, including models of decentralized protocols, board games, and game-theoretic examples.

Daniel Ranalter (University of Innsbruck)
Chad Brown (Czech Technical University in Prague)
Cezary Kaliszyk (University of Innsbruck)
Experiments with Choice in Dependently-Typed Higher-Order Logic

ABSTRACT. Recently an extension to higher-order logic — called DHOL — was introduced, enrich- ing the language with dependent types, and creating a powerful extensional type theory. In this paper we propose two ways how choice can be added to DHOL. We extend the DHOL term structure by Hilbert’s indefinite choice operator ϵ, define a translation of the choice terms to HOL choice that extends the existing translation and show that the extension of the translation is sound and complete. We finally evaluate the extended translation on a set of dependent HOL problems that require choice.

Johann Rosain (ENS Lyon)
Richard Bonichon (O(1) Labs)
Julie Cailler (University of Regensburg)
David Delahaye (LIRMM)
Olivier Hermant (CRI)
A Generic Deskolemization Strategy

ABSTRACT. In this paper, we present a general strategy that enables the translation of tableau proofs using different Skolemization rules into machine-checkable proofs. It is part of a framework that enables (i) instantiation of the strategy into algorithms for different set of tableau rules (e.g., different logics) and (ii) easy soundness proof which relies on the local extensibility of user-defined rules. Furthermore, we propose an instantiation of this strategy for first-order tableaux that handles notably δ++ rules, which is, as far as the authors know, the first one in the literature. Additionally, this deskolemization strategy has been implemented in the Goéland automated theorem prover, enabling an export of its proofs in Coq and Lambdapi. Finally, we have evaluated the algorithm performances for δ+ and δ++ rules through the certification of proofs from some categories of the TPTP library.

Johannes Schoisswohl (TU Wien)
Laura Kovács (TU Wien)
Konstantin Korovin (The University of Manchester)
VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic

ABSTRACT. We introduce Virtual Integer-Real Arithmetic Substitution (VIRAS), a quantifier elimination procedure for deciding quantified linear mixed integer-real arithmetic problems. VIRAS combines the framework of virtual substitutions with conflict-driven proof search and linear integer arithmetic reasoning based on Cooper’s method. We demonstrate that VIRAS gives an exponential speedup over state-of-the-art methods in quantified arithmetic reasoning, proving problems that SMT-based techniques fail to solve.

Bernardo Subercaseaux (Carnegie Mellon University)
Sometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition

ABSTRACT. Adding blocked clauses to a CNF formula can substantially speed SAT-solving up, both in theory and practice. In theory, the addition of blocked clauses can exponentially reduce the length of the shortest refutation for a formula. In practice, it has been recently shown that the runtime of CDCL solvers decreases significantly on certain instance families when blocked clauses are added as a preprocessing step. This fact is in contrast, but not contradiction, with Blocked-Clause Elimination (BCE) being known as a sometimes effective preprocessing step for over a decade, and suggests that the practical role of blocked clauses in SAT-solving might be richer than expected. In this paper we propose a theoretical study of the complexity of Blocked-Clause Addition (BCA) as a preprocessing step for SAT-solving, and in particular, consider the problem of adding the maximum number of blocked clauses of a given arity k to an input formula F. While BCE is a confluent process, meaning that the order in which blocked clauses are eliminated is irrelevant, this is not the case for BCA: adding a blocked clause to a formula might unblock a different clause that was previously blocked, and this order-sensitivity turns out to be a crucial obstacle for carrying out BCA efficiently as a preprocessing step. Our main result is that computing the maximum number of k-ary blocked clauses that can be added to an input formula F is NP-hard for every k >= 2.

Joseph Tafese (University of Waterloo)
Arie Gurfinkel (University of Waterloo)
Efficient Simulation for Hardware Model Checking using Btor2MLIR

ABSTRACT. Simulation is an important aspect of model checking, serving as an invaluable pre-processing step that can quickly generate a set of reachable states. This is evident in model checking tools at the Hardware Model Checking Competitions, where Btor2 is used to represent verification problems. Recently, Btor2MLIR was introduced as a novel format for representing safety and correctness constraints for hardware circuits. It provides an executable semantics for circuits represented in Btor2 by providing an equivalent program in LLVM-IR. One challenge in simulating Btor2 circuits is the use of persistent (i.e., immutable) arrays to represent memorys. Persistent arrays work well for symbolic reasoning in SMT but they require copy-on-write semantics when being simulated natively. We provide an algorithm for converting persistent arrays to transient (i.e., mutable) arrays with efficient native execution. This opens the door for rapid prototyping, dynamic verification techniques and random testing using established tool chains such as LibFuzzer and KLEE.

Tanel Tammet (Tallinn University of Technology)
Waste Reduction: Experiments in Sharing Clauses between Runs of a Portfolio of Strategies (Experimental Paper)

ABSTRACT. Most high-end automated theorem provers for first order logic (FOL) split available time between short runs of a large portfolio of search strategies. These runs are typically independent and can be parallelized to exploit all the available processor cores. We explore several avenues of re-using clauses generated by earlier runs and present experimental results of their usefulness or lack thereof.

Guilherme Toledo (Bar Ilan University)
Yoni Zohar (Bar-Ilan University)
Combining Combination Properties: Minimal Models

ABSTRACT. This is part of an ongoing research project, with the aim of studying the connections between model-theoretic properties related to theory combination in Satisfiability Modulo Theories. In previous work, 7 properties were analyzed: convexity, stable infiniteness, smoothness, finite witnessibility, strong finite witnessibility, the finite model property, and stable finiteness.

The first two properties are needed for Nelson-Oppen combination, the third and fourth are related to polite combination, the third and fifth correspond to strong politeness, and the last two are related to the combination of shiny theories.

However, the remaining key property of shiny theories, namely, the ability to compute the cardinalities of minimal models, was not yet analyzed. In this paper we study this property.