English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Word equations are a crucial element in the theoretical foundation ofconstraint solving over strings. A word equation relates two words over stringvariables and constants. Its solution amounts to a function mapping variablesto constant strings that equate the left and right hand sides of the equation.While the problem of solving word equations is decidable, the decidability ofthe problem of solving a word equation with a length constraint (i.e., aconstraint relating the lengths of words in the word equation) has remained along-standing open problem. We focus on the subclass of quadratic wordequations, i.e., in which each variable occurs at most twice. We first showthat the length abstractions of solutions to quadratic word equations are ingeneral not Presburger-definable. We then describe a class of counter systemswith Presburger transition relations which capture the length abstraction of aquadratic word equation with regular constraints. We provide an encoding of theeffect of a simple loop of the counter systems in the existential theory ofPresburger Arithmetic with divisibility (PAD). Since PAD is decidable (NP-hardand is in NEXP), we obtain a decision procedure for quadratic words equationswith length constraints for which the associated counter system is flat (i.e.,all nodes belong to at most one cycle). In particular, we show a decidabilityresult (in fact, also an NP algorithm with a PAD oracle) for a recentlyproposed NP-complete fragment of word equations called regular-oriented wordequations, when augmented with length constraints. We extend this decidabilityresult (in fact, with a complexity upper bound of PSPACE with a PAD oracle) inthe presence of regular constraints.

Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility