Přehled známých tříd booleovských formulí, pro které je znám polynomiální algoritmus pro testování problému splnitelnosti (SAT). Shrnujeme základní vlstnosti těchto tříd a jejich vzájemné vztahy vzhledem k inkluzi.
Zváštní pozornost věnujime třídě SLUR. Tuto třídu zobecňujeme do hierarchie tříd a dokazujeme její vlastnosti.