Title: Theory / Unimportant / CS / Algo / Decision Procedures - Kroening Strichman V2 / 3 Quantified formulas;
Tags: fromAlgorithm hasNotNewEffectReturnsMeaning

Page: 60
Implementation: If there is some \(i\) such that \(y_{i,1}\) is reachable from \(y_{i,2}\) in the graph generated by \((x_{i,1},x_{i,2})\) rejects.
Otherwise accepts.
Section: 1
Chapter: 3
Effect: Deciding whether this formula is satisfiable
Variables: \(\bigwedge_{i\in E} x_{i,1}=x_{i,2}\land\bigwedge_{i\in I}y_{i,1}\ne y_{i,2}\)
Time complexity: \(|I|\times|\{x_{i,j}\}|\)