01114011

a

01114011 van Maaren, Hans On the use of second order derivatives for the satisfiability problem. Du, Dingzhu (ed.) et al., Satisfiability problem: theory and applications. DIMACS workshop, Piscataway, NJ, USA, March 11-13, 1996. Providence, RI: AMS, American Mathematical Society. DIMACS, Ser. Discrete Math. Theor. Comput. Sci. 35, 677-687 (1997). 1997 Providence, RI: AMS, American Mathematical Society EN CNF formulae Summary: We study smooth convex and concave transforms of CNF formulae, introduced by van Maaren, Groote and Rozema. First- and second-order Taylor expansions of these transforms are used to design a LP-based branching algorithm, where the branching variable is determined by the smallest eigenvalue of the Hessian of the concave transform. Experiments with random 3-SAT formulae show that the resulting search trees are small.