Variant Satisfiability of Parameterized Strings

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationRewriting Logic and Its Applications - 13th International Workshop, WRLA 2020, Revised Selected Papers
EditorsSantiago Escobar, Narciso Martí-Oliet
Number of pages18
ISBN (Print)9783030635947
StatePublished - 2020
Event13th International Workshop on Rewriting Logic and Its Applications, WRLA 2020 - Virtual, Online
Duration: Oct 20 2020Oct 22 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12328 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference13th International Workshop on Rewriting Logic and Its Applications, WRLA 2020
CityVirtual, Online

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Variant Satisfiability of Parameterized Strings'. Together they form a unique fingerprint.

Cite this