Solving satisfiability problems using elliptic approximations – effective branching rules Original Research Article

An elliptic approximation of 3SAT problems is derived. It is used to derive branching rules for application in a Davis–Putnam–Logemann–Loveland branching & backtracking algorithm. Using the ellipsoid several well-known branching rules are rediscovered, but now they are obtained with a geometrical motivation. In fact, these rules can be considered to be approximations of the new rules we obtain, that make full use of the elliptic structure. These rules are more effective than the ‘old’ branching rules in terms of node counts. Extensive computational results are provided.