Třídy booleovských formulí s efektivně řešitelným SATem

Abstrakt

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.

Klíčová slova

• booleovské formule
• SAT
• splnitelnost