Machine learning by satisfiability solving

Define B = {0, 1} and a Boolean function f_p: B^N B where p is a Boolean parameter vector in Bⁿ. Consider that f_p(x) can be represented as a Boolean expression whose variables are the entries of vectors p and x. Assume that c is the cost of computing f_p(x) measured in some way, for example, the number of operator evaluations based on some complete set of Boolean operators. Then, given y in B and x in B^N, the cost to solve the equation f_p(x) = y for satisfying y has cost c2ⁿ, using the most naive brute force search.

For 3SAT solving, a much better worst case bound is known, namely O(1.307ⁿ), see here, for a related discussion see here. For the inexactly-defined class of industrial problems," performance in practice is often much better; for a discussion see here.

Now consider a set of Boolean feature vectors x_i and labels y_i. for i in {1, ..., d}. One can now solve f_p(x_i) = y_i for all i. Since the number of unknown variables to be solved for is unchanged, the naive bound on computational cost is cd2ⁿ, scaling linearly in the number of data values d. Note this is tractable if the phenomenon in question can be modeled by a small number of logical parameters n.

In practice, one generally does not solve a machine learning problem exactly but approximately, minimizing a loss function. One can use the AtLeast operator in a SAT solver like Z3 to require that f_p(x_i) = y_i be satisfied for at least K values of i, for some K. One can then find the maximal such K by performing bisection on K, requiring log₂(d) such SAT solves. On exact solvers for this problem see also here.

The AtLeast operator can be implemented by either binary adder / totalizer encoding (Bailleux and Boufkhad 2003), sequential counter encoding (Sinz 2005), or Batcher sorting network approach (Abio et al. 2013). Unfortunately, all these methods require adding significant numbers of auxiliary variables, adversely affecting the naive complexity bound. However, one can hope that performance is much better than this bound for industrial problems, as is often the case in practice. Furthermore, randomized approximation algorithms known to run in polynomial time can provably find assignments that satisfy a guaranteed fraction (e.g., 3/4 or more) of the maximum number of satisfiable Boolean constraints (see for example here, here, here and here). This might serve as a proxy for exactly solving for the optimizer.

If the problem instead has Boolean expressions with embedded linear inequality predicates on integer variables of bounded range, one could apply SMT solver methods directly using the ideas described above, or convert the problem to a SAT problem and apply the above methods directly.

The idea of using SAT solvers for machine learning in the way described here goes back to (Kamath et al. 1992). The method is described with an example in Donald Knuth's TAOCP fascicle on Satisfiability, section on Learning a Boolean function.

The post Machine learning by satisfiability solving first appeared on John D. Cook.