Solving 3SAT and MIS Problems with Analog Quantum Machines

This work considers the use of analog quantum machines to solve the boolean satisfiability problem 3SAT by taking Quadratic Unconstrained Binary Optimization models (QUBO) as input. With the aim of using real quantum computers instead of emulators to solve instances of the problem, we choose the D-Wave quantum machines, which have a static topology and limited connectivity. Therefore, the choice of the problem formulation must take these important constraints into account. For this reason, we propose to solve 3SAT instances through polynomial-time reduction to the Maximum Independent Set problem. This is because the resulting graph is less dense and requires lower connectivity than the one that would be produced by directly modeling 3SAT into a QUBO.