Perché non eseguono questi controlli sul numero di clausole in 3-Sat?

Question

Ho scritto un risolutore a 3 saggi per divertimento e confrontando le sue prestazioni con il solutore Pycosat. Il mio risolutore supera di gran lunga il Pycosat in due casi speciali, in cui risolvo facendo controlli semplici e ovvi, cosa che Pycosat non sembra fare (in base al tempo necessario per risolvere questi casi).

Presumevo che questi controlli sarebbero stati conosciuti e comunemente incorporati nei solutori. È questo il caso? Perché un risolutore non dovrebbe preoccuparsi di farlo?

I controlli si basano su quanto segue:

Permettere $ phi $ essere un CNF con $ n $ variabili e $ m $ Disgiunzioni, in cui ogni disgiunzione ha esattamente 3 variabili distinte e non ci sono due disgiunzioni hanno gli stessi letterali.

1) if $ m <8 $, poi $ phi $ è soddisfacente.

2) if $ m> 7* binom {n} {3} $, poi $ phi $ è insoddisfacente. ($ binom {n} {k} $ è il coefficiente binomiale.)

La prova è semplice ma noiosa. Posso fornirlo se necessario.