# Can you find a counterexample / disprove my P=NP solution?

I've posted the full article here. The source code is available here.

Basically, in the Linear Programming (LP) task, we solve a system of inequalities: one inequality per BSAT clause. In each inequality, put +x[i] if i-th boolean variable appears straight in this clause, and -x[i] if the variable appears negated. Each inequality has a lower bound to be satisfiable: 2-N[j], where N[j] is the number of variables in j-th inequality. We limit each variable to -1 <= x[i] <= +1.

We run multiple iterations of LP solving. In each iteration, we minimize the following function:

f(x[0],..,x[N-1]) = sum( i, -x[i] * (4^(-i)) )


Obviously, to get any sensible precision for optimizing such a function, we need long arithmetic - with precision of at least 2*N bits. After the function is minized, some variables become within -1+eps or 1-eps ranges. We consider such variables assigned False and True respectively. The other variables have abs(x[i]) < 1-eps and we consider them unassigned.

Next, we reorder the variables so that x[0] becomes the one with the smallest absolute value, x[1] becomes the next smallest, etc., and in the end of the new order of variables there are assigned variables (whose abs(x[i]) >= 1-eps).

We repeat the process from solving the LP task, with a warm start, temporarily assigning True to variables whose x[i]>-0 and False to variables whose x[i]<+0 (for those unfamiliar, machine arithmetic has signed zero - it distinguishes between +0 and -0).

The solution is tested for 20 variables and base 4 as above - it converges in 2-3 iterations. If we use base 2, it converges in 3-4 iterations. The solution also converges for 100 variables and base 1.1, but it takes hundreds of iterations because variable assignments interfere with each other. I just don't yet have an LP solver with multi-precision (i.e. beyond the machine's double data type, which has only 53-63 bits of precision).

Do you see any flaws or counterexamples to this algorithm?

From what I can tell, you have proposed a (heuristic) algorithm for solving the Satisfiability Problem. But you have not given an argument for the correctness of your algorithm or an analysis of the asymptotic runtime, so this does not prove $$P=NP$$.
Also, I want to make sure I understand your algorithm correctly. First, am I correct in assuming the statement is assumed to be in CNF? Next, I want to make sure I understand how you translate clauses to constraints. Consider the clause $$(x_1 \lor \neg x_2 \lor \neg x_3 \lor x_4 \lor x_5)$$. Am I correct that this would correspond to the constraint $$x_1 - x_2 - x_3 + x_4 + x_5 \geq -3$$? Finally, am I correct that, after each solve of the LP, you set some of the decision variable to $$1$$ or $$-1$$ (corresponding to "true" or "false"), and repeat this process until a satisfying assignment is found, or it can be determined that there is no satisfying assignment?
Assuming I am correct about the above, there are a few issues with your approach. First, the way you are translating clauses to constraints is incorrect. Looking at my example above, the constraint can be satisfied by setting all of the variables to 0. Indeed, for any clause of two or more literals the corresponding constraint is satisfied when all of the variables are 0. Second you claim, "After the function is minized, some variables become within -1+eps or 1-eps ranges." But this it is possible that no variables are near -1 or +1. As such, it is not clear how too bound the number of iterations needed by your algorithm. It is not even clear your algorithm is guaranteed to terminate. Finally, is it not possible that in the only satisfying assignments, that a particular variable $$x_k$$ is set to -1, but the LP assigns a value close to 1 to a variable, and thus you round it up to 1. It seems your algorithm would incorrectly determine that this instance is unsatisfiable.
• The objective function drives variable values to converge to 1 or -1, away from zeroes. If LP solver can't find a solution at some iteration, then the boolean formula is not satisfiable. Yes, I use CNF with DIMACS interface. Before each iteration, all variables receive initial values of +-1: e.g. I set them all to -1 (False) before the first iteration, and in the next iterations I set to False whatever's less than +0, and True for greater than -0. These values are just to warmup the LP solver - it can completely reassign the values. eps must be small enough to avoid wrong roundings. Commented Apr 30 at 18:51