I already said, I don't have an efficient algorithm. Once I will have, in my estimation, at best, it will be O(n^3) (n is number of variables), which still means a lot - to factor 16-bit integer, my (linear) 2XSAT reduction requires about 4000 variables, so the number of variables for a cryptographically-strong problem will be in millions. You need to have a very efficient parallel algorithm to deal with that, and that's very low on the list of priorities - first I need to understand how to actually make the algorithm efficient (so far I think I proved there is a polynomial bound - around O(n^8) or so, but I know for sure it's very inefficient, because I am doing it very naively).

There are other ways to improve the method, which (if indeed P=NP) are incredibly interesting - you can directly compose presolved general instances and specialize on them. Kinda like if you need to compute many solutions to linear equations, you only need to factor the matrix once.