Variazione di 3-sat max

Question

Supponiamo che ci venga dato un 3CNF e vogliamo sapere se le clausole K di questo 3CNF possono essere soddisfatte (k essendo un numero naturale)?

Sto cercando di pensare a un algoritmo efficiente per risolvere questo problema. Questa è una specie di variazione del massimo 3-Sat, ma con un k fisso. Se abbiamo clausole m, controllando ingenuamente otterrebbe confronti $ binom {m} {k} $, ma questo sembra fattoriale (se ci approssimiamo con la formula di Sterling, esponenziale) complessità.

Quale potrebbe essere un modo efficiente per verificarlo? Devo mancare qualcosa. Grazie.