Attempts to disprove: https://cstheory.stackexchange.com/questions/54250/can-you-find-a-counterexample-disprove-my-p-np-solution
Article: https://www.academia.edu/118325445/P_NP_a_reduction_of_Boolean_Satisfiability_problem_to_Linear_Programming_and_Long_Arithmetic
Source code: https://github.com/srogatch/bsat-circulation/blob/lin-prog/CpuSolver.h
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).