There exists a wide range of constraint programming (CP) problems defined on Boolean functions depending on binary variables. One of the approaches to solving CP problems is using specific appropriate solvers, e.g., SAT solvers. An alternative is using the generic solvers for mixed-integer linear programming problems (MILP), but they require transforming expressions with Boolean functions to linear equations or inequalities. Here, we present two methods of such a transformation which applies to any Boolean function defined by explicit rules giving values of the Boolean function for all combinations of its Boolean variables. The first method represents the Boolean function as a linear equation in the original binary variables and, possibly, binary ancillaries, which become additional variables of the MILP problem being composed. The second method represents the Boolean function as a set of linear inequalities in the original binary variables and one additional continuous variable (representing the value of the function). The choice between the first or second method is a trade-off between the number of binary variables and number of linear constraints in the emerging MP problem. The advantage of the proposed approach is that both methods reduce important cryptanalysis problems, such as the preimaging of hash functions or breaking symmetric ciphers as the MILP problems, which are solved by the generic MILP solvers. Furthermore, the first method enables to reduce the binary linear equations to quadratic unconstrained binary optimization (QUBO), by the quantum annealer, e.g., D-Wave.

Previous publications presented an implementation of coarse-grained parallel Branch-and-Bound (B&B) method. It supports two strategies: decomposition of feasible domain into a set of sub-problems; “multisearch” (or concurrent) solving the same problem with different settings of the BNB-method. In both cases several B&B-solver’s processes exchange best values of goal function on feasible solutions they found. Earlier, it was found that this approach gives a noticeable speed-up of solving the original optimization problem. The method has been implemented as an Everest-application called DDBNB (Domain Decomposition B&B). It is based on Everest distributed computing platform, everest.distcomp.org, and open source solvers: CBC, projects.coin-or.org/Cbc; SCIP, scip.zib.de. Originally, DDBNB has been tested on discrete optimization problems (Traveling Salesman and Load Balancing). The paper presents application of DDBNB to global optimization problems with polynomial functions (solver SCIP supports solving of such class of problems). Well known problems concerning optimal placements of points on 3D-sphere are considered: Tammes and Thomson problems. The first problem is to maximize minimal distance between any two of N points. The second - minimize electrostatic Coulomb energy of unit charges put in N points. Both may be represented as mathematical programming problems with polynomial functions. Feasible domains of both problems are direct products of 3D-spheres and different decompositions of this domains by linear inequalities into hundreds of subproblems have been tested. Tests performed gave promising results and crucial acceleration for Tammes problems, N=7,8,9, and Thomson problem, N=5. One should note that Thomson problem got computer aided proof (substantially based on the problem’s specifics) less than a decade ago, when proposed approach is rather generic and does not go into details of the problem to be solved. Formulation of original problems and decomposition strategies have been implemented via Pyomo, pyomo.org. All sub-problems have been passed to solvers as AMPL-stubs, (also known as NL-files). Usage of Everest platform enables to involve in experiments HPC resources of NRC Kurchatov Institute.