Generating Weighted MAX-2-SAT Instances with Tunable Frustration on an RBM

Many optimization problems can be cast into the maximum satisfiability (MAX-SAT) form, and many solvers have been developed for tackling such problems. To evaluate a MAX-SAT solver, it is convenient to generate hard MAX-SAT instances with known solutions. Here, we propose a method of generating weighted MAX-2-SAT instances inspired by the frustrated-loop algorithm used by the quantum annealing community to generate Ising instances on a cubic lattice with nearest-neighbor couplings. We extend the algorithm for instances of general bipartite couplings, with the associated optimization problem being the minimization of the restricted Boltzmann machine (RBM) energy over the nodal values, which is useful for an effective pre-training of the RBM. The difficulty of the generated instances can be tuned through a central parameter known as the frustration index. It is observed through simulation that the frustration index drives a double phase transition in the hardness scaling behavior of the generated instances with respect to the size of the system [1]. Work supported in part by CMRR and DARPA.

[1] Y. R. Pei, H. Manukian, and M. Di Ventra, "Generating Weighted MAX-2-SAT Instances of Tunable Difficulty with Frustrated Loops". arXiv:1905.05334.