W solverach SAT często można znaleźć metody płaszczyzny cięcia, zmienną propagację, odgałęzienie i wiązanie, uczenie się klauzul, inteligentne cofanie, a nawet ręcznie tkaną ludzką heurystykę. Jednak przez dziesięciolecia najlepsze solwery SAT polegały w dużej mierze na technikach sprawdzania rozdzielczości i używają kombinacji innych rzeczy po prostu do pomocy i do bezpośredniego wyszukiwania w stylu rozdzielczości. Oczywiście podejrzewa się, że ŻADNY algorytm nie zdoła rozstrzygnąć kwestii satysfakcji w czasie wielomianowym, przynajmniej w niektórych przypadkach.
W 1985 r. Haken udowodnił w swojej pracy „Nietrwałość rozdzielczości”, że zasada gołębia zakodowana w CNF nie dopuszcza dowodów wielomianowej rozdzielczości. Chociaż dowodzi to czegoś o niemożliwości zastosowania algorytmów opartych na rozdzielczości, daje również kryteria, według których można oceniać najnowocześniejsze solwery - i w rzeczywistości jednym z wielu rozważań, które należy wziąć pod uwagę przy projektowaniu dzisiejszego solvera SAT, jest to, jak prawdopodobnie będzie on działał w znanych „trudnych” przypadkach.
Posiadanie listy klas formuł boolowskich, które potwierdzają wykładniczo dowody rozdzielczości, jest użyteczne w tym sensie, że daje „twarde” formuły do testowania nowych solverów SAT. Jakie prace wykonano przy kompilowaniu takich klas razem? Czy ktoś ma odniesienie zawierające taką listę i odpowiednie dowody? Podaj jedną klasę logicznej formuły dla każdej odpowiedzi.