Metalevel Algorithms for Variant Satisfiability

Variant satisfiability is a theory-generic algorithm to decide quantifier-free satisfiability in an initial algebra TS/E when the theory (Sigma, E) has the finite variant property and its constructors satisfy a compactness condition. This paper: (i) gives a precise definition of several meta-level sub-algorithms needed for variant satisfiability; (ii) proves them correct; and (iii) presents a reflective implementation in Maude 2.7 of variant satisfiability using these sub-algorithms.