Variant-based satisfiability in initial algebras

Although different satisfiability decision procedures can be combined by algorithms such as those of Nelson-Oppen or Shostak, current tools typically can only support a finite number of theories to use in such combinations. To make SMT solving more widely applicable one needs theory-generic satisfiability algorithms allowing a potentially infinite number of decidable theories to be user-definable, instead of needing to be built in by tool implementers. This work studies how folding variant narrowing, a generic unification algorithm that offers good extensibility in unification theory, can be extended to a generic variant-based satisfiability algorithm for the initial algebras of user-specified input theories when such theories satisfy Comon and Delaune's finite variant property (FVP) and some extra conditions. Several, increasingly larger infinite classes of theories whose initial algebras enjoy decidable variant-based satisfiability are identified and illustrated with examples. A method based on descent maps to bring other theories into these classes and to improve the generic algorithm's efficiency is also proposed.