Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning

Marco Sälzer, Eric Alsmann, Martin Lange

We analyse the complexity of the satisfiability problem, or similarly feasibility problem, (trSAT) for transformer encoders (TE), which naturally occurs in formal verification or i…