El problema de satisfacibilidad (SAT) en lógica proposicional determina si hay una asignación de valores que haga que una fórmula proposicional dada sea verdadera. Recientemente, se han desarrollado solucionadores SAT rápidos, y la investigación de codificación SAT ha ganado atención. Esto permite que varios problemas del mundo real se transformen en SAT y se resuelvan, logrando una solución a los problemas originales. Proponemos un nuevo método de codificación, Codificación Fraccional, que se centra en las restricciones de "A lo más K" -un cuello de botella de complejidad computacional- y reduce la escala de las expresiones lógicas dividiendo las variables objetivo. Además, confirmamos que la Codificación Fraccional supera a los métodos existentes en términos del número de cláusulas generadas y variables auxiliares requeridas. Por lo tanto, permite la resolución eficiente de problemas del mundo real como la planificación y la verificación de hardware.