E2E4: Treba ty SMT solvery. Tak do 2007 (plus minus autobus) to nebylo moc prakticke, protoze exponencialni slozitost. No pak se prislo na to, ze nektere prakticke podmnoziny tyho problemu lze resit v polynomialnim case.
Alespon to je moje chapani veci, nejsem matematik, jen BFP (bezny franta programator),
DARK_ONE me mozna opravi / doplni. Kazdopadne to do dokaze Z3 je docela pusobive. A zaroven je (Z3 konkretne) dobre technicky udelane, je to .so s dobre navrzenym C API, je desne jednoduche to zacit pouzivat ve svem programu.
A to co se nad tim stavi je nemene "mind-blowing" - "symbolic execution" programu, "superoptimization", ...