arXiv subjects
Publications and source records attributed to Mnacho Echenim.
This paper investigates under which conditions instantiation-based proof procedures can be combined in a nested way, in order to mechanically construct new instantiation procedures for richer theories. Interesting applications in the field of verification are emphasized, particularly for handling extensions of the theory of arrays.
Symmetries occur naturally in CSP or SAT problems and are not very difficult to discover, but using them to prune the search space tends to be very challenging. Indeed, this usually requires finding specific elements in a group of symmetries that can be huge, and the problem of their very existence is NP-hard. We formulate such an existence problem as a constraint problem on one variable (the symmetry to be used) ranging over a group, and try to find restrictions that may be solved in polynomial time. By considering a simple form of constraints (restricted by a cardinality k) and the class of groups that have the structure of Fp-vector spaces, we propose a partial algorithm based on linear algebra. This polynomial algorithm always applies when k=p=2, but may fail otherwise as we prove the problem to be NP-hard for all other values of k and p. Experiments show that this approach though restricted should allow for an efficient use of at least some groups of symmetries. We conclude with a few directions to be explored to efficiently solve this problem on the general case.
Many decision procedures for SMT problems rely more or less implicitly on an instantiation of the axioms of the theories under consideration, and differ by making use of the additional properties of each theory, in order to increase efficiency. We present a new technique for devising complete instantiation schemes on SMT problems over a combination of linear arithmetic with another theory T. The method consists in first instantiating the arithmetic part of the formula, and then getting rid of the remaining variables in the problem by using an instantiation strategy which is complete for T. We provide examples evidencing that not only is this technique generic (in the sense that it applies to a wide range of theories) but it is also efficient, even compared to state-of-the-art instantiation schemes for specific theories.