K-SATO problema da satisfatibilidade booleana onde cada cláusula na fórmula lógica tem exatamente 'k' literais. É um problema central na teoria da complexidade computacional.
