Charles Explorer logo
🇨🇿

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

Publikace na Matematicko-fyzikální fakulta |
2010

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.