Parallel algorithms for solving SAT-problems in application to optimization problems with Boolean constraints

A parallel technology that can be used to solve various problems of discrete optimization is proposed. This technology is based on a number of efficient procedures of reducing combinatorial optimization problems to SAT problems. A process of solving an optimization problem is implemented as an iterative scheme such that a SAT problem is solved at each step using various techniques of parallelization. In order to take into account the information accumulated during previous iterations, a special technique called “Incremental SAT” is used. This technique is usually applied to solve the verification problems for discrete systems. The technology proposed was tested using various combinatorial problems, in particular, the quadratic assignment problem.