Sounds really cool, were you able to verify the correctness of the results?

SAT solvers run until they reach the "SAT" status, meaning "satisfied" or UNSAT. The harder the problem the longer you might be running the program - days, weeks even.

Ideally, what you want is a single SAT value among a remainder universe of UNSATs.

Sometimes the best you can achieve at any given point is a lower bound and an upper bound range, like "greater than 3 but less than 9."

Of course I simplified in my post but it started out with a pretty broad range of a lower and upper bound, then narrowed further, then narrowed further, then narrowed further, etc...until the specific final result achieved K=7=SAT while every K<7=UNSAT & every K>7=UNSAT. I think it ran for a full week alone on K between 6 and 7.