ABSTRACT. TBA

ABSTRACT. Existing techniques for Craig interpolation for the quantifier-free fragment of the theory of arrays are inefficient for computing sequence and tree interpolants: the solver needs to run for every partitioning (A, B) of the interpolation problem to avoid creating AB-mixed terms. We present a new approach using Proof Tree Preserving Interpolation and an array solver based on Weak Equivalence on Arrays. We give an interpolation algorithm for the lemmas produced by the array solver. The computed interpolants have worst-case exponential size for extensionality lemmas and worst-case quadratic size otherwise. We show that these bounds are strict in the sense that there are lemmas with no smaller interpolants. We implemented the algorithm and show that the produced interpolants are useful to prove memory safety for C programs.

ABSTRACT. Solving optimization problems with SAT has a long tradition, particularly in the form of MaxSAT, which maximizes the weight of satisfied clauses in a propositional formula. The extension to maximum satisfiability modulo theories (MaxSMT) is less mature but allows problems to be formulated in a higher-level language closer to actual applications. In this paper we describe a new approach for solving MaxSMT based on lifting one of the currently most successful approaches for MaxSAT, the implicit hitting set approach, from the propositional level to SMT. We also provide a unifying view of how optimization, propositional reasoning, and theory reasoning can be combined in a MaxSMT solver. This leads to a generic framework that can be instantiated in different ways, subsuming existing work and supporting new approaches. Experiments with two instantiations clearly show the benefit of our generic framework.

ABSTRACT. The clausal logical consequences of a formula are called its implicates. The generation of these implicates has several applications, such as the identification of missing hypotheses in a logical specification. We present a procedure that generates the implicates of a quantifier-free formula modulo a theory. No assumption is made on the considered theory, other than the existence of a decision procedure. The algorithm has been implemented (using the solvers Minisat, CVC4 and z3) and experimental results show evidence of the practical relevance of the proposed approach.

ABSTRACT. Recent work on the practical aspects on the modal logic S5 satisfiability problem showed that using a SAT-based approach outperforms other existing approaches. In this work, we go one step further and study the related minimal S5 satisfiability problem (MinS5-SAT), the problem of finding an S5 model, a Kripke structure, with the smallest number of worlds.

Finding a small S5 model is crucial as soon as the model should be presented to a user, displayed on a screen for instance. SAT-based approaches tend to produce S5-models with a large number of worlds, thus the need to minimize them.

That optimization problem can obviously be solved as a pseudo-Boolean optimization problem. We show in this paper that it is also equivalent to the extraction of a maximal satisfiable set (MSS). It can thus be solved using a standard pseudo-Boolean or MaxSAT solver, or an MSS-extractor.

We show that a new incremental, SAT-based approach can be proposed by taking into account the equivalence relation between the possible worlds on S5 models. That specialized approach presented the best performance on our experiments conducted on a wide range of benchmarks from the modal logic community and a wide range of pseudo-Boolean and MaxSAT solvers.

Our results demonstrate once again that domain knowledge is key to building efficient SAT-based tools.

ABSTRACT. In this paper, we describe a method for solving some open problems in design theory based on SAT solvers. Modern SAT solvers are efficient and can produce unsatisfiability proofs. However, the state-of-the-art SAT solvers cannot solve so-called large set of idempotent quasigroups. Two idempotent quasigroups over the same set of elements are said to be disjoint if at any position other than the main diagonal, the two elements from the two idempotent quasigroups at the same position cannot be the same. A collection of $n-2$ idempotent quasigroups of size n is called a large set if all idempotent quasigroups are mutually disjoint, denoted by LIQ(n). The existence of LIQ(n) satisfying certain identities has been a challenge for modern SAT solvers even if n = 9. We will use a finite model generator to help the SAT solver avoiding symmetric search spaces, and take both advantages of first order logic and the SAT techniques. Furthermore, we use an incremental search strategy to find a maximum number of disjoint idempotent quasigroups, thus decide the non-existence of large sets. The experimental results show that our method is highly efficient. The use of symmetry breaking is crucial to allow us to solve some instances in reasonable time.

ABSTRACT. Constrained counting is important in domains ranging from artificial intelligence to software analysis. There are already a few approaches for counting models over various types of constraints. Recently, hashing-based approaches achieve success but still rely on solution enumeration. In this paper, a new probabilistic approximate model counter is proposed, which is also a hashing-based universal framework, but with only satisfiability queries. A dynamic stopping criteria, for the new algorithm, is presented, which has not been studied yet in previous works of hashing-based approaches. Although the new algorithm lacks theoretical guarantee, it works well in practice. Empirical evaluation over benchmarks on propositional logic formulas and SMT(BV) formulas shows that the approach is promising.

ABSTRACT. We introduce a sound and complete coinductive proof calculus for reachability properties in transitions systems generated by logically constrained term rewriting rules over an order-sorted signature modulo builtins.

A key feature of the proof calculus is a circularity proof rule, which allows to obtain finite representations of the infinite coinductive proof trees. The paper also includes a brief description of a prototype implementation, which validates our approach on a number of examples.

ABSTRACT. In this paper, we describe a high-performance reasoning tool, called FAME, for semantic forgetting in expressive description logics. Forgetting is a non-standard reasoning service that seeks to create restricted views of ontologies by eliminating concept and role names from ontologies in a way such that all logical consequences up to the remaining signature are preserved. FAME is a Java-based implementation of an Ackermann-based method for forgetting concept and role names from ontologies expressible in the description logic ALCOIH, i.e., the basic ALC extended with nominals, inverse roles, and role inclusions. FAME can be used as a standalone tool or a Java library for forgetting or related tasks. Results of an evaluation of FAME on a corpus of 396 biomedical ontologies have shown that: (i) in more than 90% of the test cases FAME was successful (i.e., eliminated all specified concept and role names) and (ii) in more than 70% of these cases the elimination was done within a single second.

ABSTRACT. Existential rules are a syntactic variant of first-order Horn logic that has gained prominence in several communities. Such rules are used to express ontologies in knowledge representation, dependencies in databases, and recursive queries in data analytics. In this system description, we present our recent extension of the rule reasoning and query engine VLog with support for existential rules. Our column-oriented implementation of the restricted chase procedure aims at constructing a universal model for a Horn logic theory. While query answering in this logic is undecidable, and universal models might be infinite, our implementation can find a finite model in many cases. We conduct an evaluation over several real-world theories with millions of facts and thousands of rules, and we show that VLog can compete with the state of the art. Other notable features of our system include support for a variety of input sources and databases, query answering capabilities, cross-platform support, and excellent memory efficiency. The latter makes it possible to compute models with hundreds of millions of relational tuples on a laptop.