ABSTRACT.  Instantiation-based reasoning aims to combine the expressivity of first-order logic with the efficiency of propositional and SMT reasoning. Most instantiation- based methods are complete for first-order logic and are especially efficient for the effectively propositional fragment (EPR). It turns out that many problems such as model checking, bit-vector reasoning, finite model finding and QBF solving can be succinctly encoded into the EPR fragment. In this talk I will discuss recent developments in instantiation-based reasoning, EPR based encodings and related challenges.

ABSTRACT. Quantified Boolean formulas (QBFs) generalize propositional formulas
by admitting quantifications over propositional variables. In this
talk, I will discuss the handling of quantifiers in different calculi
for QBFs. The considered calculi are different versions of
Q-resolution and sequent systems with different quantifier
rules. Since QBFs can be considered as a restriction of first-order
predicate logic where formulas are interpreted only over a two element
domain, I will also consider translations of QBFs to first-order
formulas together with first-order resolution. I will compare the
different calculi with respect to polynomial simulation and
exponentially separate the ones which instantiate the formula from the
ones where no instantiation is possible.

ABSTRACT. We report on techniques for translating bounded propositional reachability problems into Quantified Boolean Formulae (QBF). The techniques exploit the binary-tree structure of the QBF quantification to produce encodings logarithmic in the size of the instance and thus exponentially smaller than the corresponding SAT encoding with the same bound. We briefly describe our experimental results, and discuss the challenging structure that is implicit in these encodings.

ABSTRACT. Bit-precise reasoning is essential in many applications of Satisfiability Modulo Theories (SMT). Quantifier-free resp. quantified bit-vector formulas (QF_BV resp. BV) play an important role in hardware resp. software verification. In recent years, efficient approaches for solving such formulas have been developed. Most of the QF_BV solvers rely on bit-blasting, while BV solvers rely on quantifier instantiation. In [Kovasznai, Froehlich, & Biere, SMT 2012], we investigated the worst-case complexity of those logics and argued that bit-blasting resp. quantifier instantiation is exponential resp. double-exponential in general. We also introduced the criterion "bit-width boundedness" to bit-vector problems, as a property that seems to hold for most practical problems, and proved it to reduce the worst-case complexity by an exponential.
In this talk, we are going to give a survey on [Kovasznai, Froehlich, & Biere, CADE 2013], by proposing a polynomial translation from QF_BV to Effectively Propositional Logic (EPR) and by presenting our tool BV2EPR together with experimental data. Note that while our translation guarantees polynomiality for any QF_BV formula, it is too robust for bit-width bounded QF_BV problems and therefore cannot be considered very practical. In contrast, a translation from bit-width bounded BV problems to EPR might be of practical relevance. Therefore, in the rest of the talk, we will present ideas how to extend our translation further to BV formulas.

ABSTRACT. We consider the quantified constraint satisfaction problem (QCSP) which is to decide, given a structure and a first-order sentence (not assumed here to be in prenex form) built from conjunction and quantification, whether or not the sentence is true on the structure. We present a proof system for certifying the falsity of QCSP instances and develop its basic theory; for instance, we provide an algorithmic interpretation of its behavior. Our proof system places the established Q-resolution proof system in a broader context; we will discuss how, in a sense made precise, it generalizes Q-resolution and gives a clear proof of the soundness of Q-resolution.

As an application, we give an algebraic, Ehrenfeucht-Fraïssé-style characterization of the condition of not having bounded-width proofs (for a QCSP instance) and show that the resulting theory can be used to obtain tractability results for the QCSP.

This talk is based on the article available at http://arxiv.org/abs/1403.0222.

ABSTRACT. The past 15 years has seen tremendous improvement in the effectiveness of solvers for Quantified Boolean Formulas (QBF). This talk will discuss some of the main algorithmic approaches that have been employed in constructing such solvers. We will aim to identify certain features of these approaches that are effective and not so effective. Some of the theoretical questions that arise from our empirical experience with these solvers will be identified in an attempt to spur more synergy between theory and practice for solving QBF.

ABSTRACT. We deal with (general) equational constraints, that is, first-order formulas, with equality as its only predicate symbol, over a (finite or infinite) language $\Language$ of function symbols. As semantic domain, we consider the algebra of finite terms over L. Solving one of such constraints means to find all the solutions for (i.e. assignments to) its free variables. We present the Projective Quantifier Elimination (PQE) technique for solving equational constraints (in particular, deciding their satisfiability) that performs an algebraic-style transformation of expressions instead of handling first-order formulas. PQE is formulated on the basis of three algebraic operations on expressions: complement, intersection and projection. We aim to contribute not only a new style of quantifier elimination for constraint solving, but also a more efficient method for equational constraint solving. PQE avoids unnecessary applications of the costly Explosion Rule (ER) that are performed by traditional solving methods.

ABSTRACT. There is great interest in the use of symbolic reasoning for synthesising loop invariants, ranking functions, or whole program fragments and hardware circuits. Solvers for the quantifier-free fragment of bit-vector logic exist and often rely on SAT solvers for efficiency. However, many techniques require quantifiers in bit-vector formulas to avoid an exponential blow-up during construction and QBF solvers are often inefficient. I will present an approach based on a set of effective word-level simplifications that are traditionally employed in automated theorem proving, heuristic quantifier instantiation methods used in SMT solvers, and model finding techniques based on function templates. I will also go into why we got interested in this problem in the first place and where we would like to take it from here.

ABSTRACT. We take as starting point routines for quantifier reasoning in the SMT solver Z3 and we analyze these through the lens of quantfier projection: quantifiers are specialized or instantiated partially using information about possible feasible interpretations that is collected during search.

ABSTRACT. Modern SMT solvers primarily rely on heuristic methods such as E-matching for answering ``unsatisfiable" in the presence of quantified formulas. The success of these solvers is often hindered by an overabundance of instantiations produced by these heuristics, making it difficult for the solver to continue its operation. In this paper, we introduce new techniques that alleviate this shortcoming by first discovering instantiations that are in conflict with the current state of the solver. In these techniques, the solver only resorts to heuristic methods when such an instantiation cannot be found, thus decreasing its dependence upon E-matching. Our experimental results show our technique significantly reduces the number of instantiations required by the SMT solver for answering ``unsatisfiable" for several benchmark libraries, and consequently leads to improvements over state-of-the-art implementations.