Two “knowingly incomplete,” yet useful, variant-based satisfiability procedures for QF formulas in the instantiations of two, increasingly more expressive, parameterized data types of strings are proposed. The first has four selector functions decomposing a list concatenation into its parts. The second adds a list membership predicate. The meaning of “parametric” here is much more general than is the case for decision procedures for strings in current SMT solvers, which are parametric on a finite alphabet. The parameterized data types presented here are parametric on a (typically infinite) algebraic data type of string elements. The main result is that if an algebraic data type has a variant satisfiability algorithm, then the data type of strings over such elements has a “knowingly incomplete,” yet practical, variant satisfiability algorithm, with no need for a Nelson-Oppen combination algorithm relating satisfiability in strings and in the given data type.