I think the best advice I could give you is to be aware that what you're hoping for -- an algorithm with performance bounds tight enough that you can use it in

I think the best advice I could give you is to be aware that what you're hoping for -- an algorithm with performance bounds tight enough that you can use it in a device driver -- probably doesn't exist. There is some chance, admittedly, that you will get lucky and find some structure in the problem that you can exploit to produce such an algorithm. But it's also entirely possible that there isn't any such structure, and the fact that you've resorted to brute force search to this point suggests there may not be. Even if there isn't, there is still hope for ways to search the space faster. This problem sounds like something that an SMT solver might work well on. I would give that a try.