Below we propose a way to solve Boolean Satisfiability problem by means of linear programming (Interior Point Method, which is polynomial) and long arithmetic: the Interior Point Method would need to operate O(V) bit real numbers, where V is the number of variables in the Boolean formula.
Consider a Boolean formula in CNF form of C clauses and V variables. To convert it to a real-numbered linear programming task, for each clause we write a linear inequality as follows:
c[i] = (x[0] – m[0]) plus (x[1] – m[1]) plus (m[2] – x[2]) plus (m[3] – x[3]) > m[3] plus m[2] – m[1] – m[0]
In the formula above, c[i] represents the sum of variable values for i-th clause, x[j] is in the exclusive range 2^j to 2^(j plus 1), and m[j] is the middle of that range, i.e. m[j] = 2^j plus 2^(j-1) . If j-th variable in i-the clause appears without a negation, in the LP task we add (x[j] – m[j]) term, but for negated variables in the original Boolean formula, in the LP task we add (m[j] – x[j]) term.
Then all we need to do is to solve the system of linear inequalities given the lower limits on clause sums c[i], and the both-sides bounds on variable substitutes x[j] . We can do it in polynomial time with Interior Point Method that uses long arithmetic instead of native floating-point.
If after solving the linear programming task x[j] > m[j], then the corresponding variable takes a value of True; x[j] < m[j] => False; x[j] == m[j] => doesn’t matter (the variable can take True or False, given the determined values for the other variables).
Algorithmic complexity: the path-following interior point method by James Renegar ( https://en.wikipedia.org/wiki/Interior-point_method ) runs in O(V^3 * L) time, where V is the number of variables and L is the bitlength of the real numbers it operates on. Because our algorithm for Boolean Satisfiability operates on O(V) bits long real numbers, the complexity of our algorithm is O(V^4) .