AVATAR: A SAT-based Architecture for First-Order Theorem-Provers
Marijn Heule
ACL2 Seminar, Feb. 17, 2015

A new SAT-based architecture for first-order resolution and
superposition theorem provers, called AVATAR (Advanced Vampire
Architecture for Theories and Resolution), was presented at
CAV'14. The original motivation of this architecture comes from a
problem well-studied in the past --- dealing with formulas consisting
of clauses containing propositional variables and other clauses that
can be split into components with disjoint sets of variables.  Such
clauses are common for problems coming from applications, for example
in verification and program analysis, where many ground literals occur
in the problems and even more are generated during the proof-search.

This problem was previously studied by adding various versions of
splitting. The addition of splitting resulted in considerable
improvements in performance of theorem provers. However, even with
various versions of splitting implemented, the performance of
superposition theorem provers is nowhere near SMT solvers on purely
ground problems or SAT solvers on propositional problems.

AVATAR is a new, revolutionary architecture for superposition theorem
provers, where a superposition theorem prover is tightly integrated
with a SAT solver. Its implementation in the theorem prover Vampire
resulted in drastic improvements over all previous implementation of
splitting. Over four hundred TPTP problems previously unsolvable by
any modern prover, including Vampire itself, have been proved, most of
them with short runtimes. Many problems solved with one of 481
variants of splitting previously implemented in Vampire can also be
solved with AVATAR.