Resource-Constrained Heuristic for Max-SAT

TL;DR

This paper introduces a resource-constrained heuristic for Max-SAT that decomposes problems into smaller parts, leveraging traditional solvers or specialized hardware, and employs novel variable selection and size prediction methods.

Contribution

It presents a new decomposition approach for Max-SAT that integrates variable selection, QUBO transformation, and size prediction, outperforming existing solutions.

Findings

Outperforms existing QUBO decomposer solutions on benchmark instances.

Introduces a novel graph-based variable selection method.

Develops a model to predict subproblem sizes for QUBO solvers.

Abstract

We propose a resource-constrained heuristic for instances of Max-SAT that iteratively decomposes a larger problem into smaller subcomponents that can be solved by optimized solvers and hardware. The unconstrained outer loop maintains the state space of a given problem and selects a subset of the SAT variables for optimization independent of previous calls. The resource-constrained inner loop maximizes the number of satisfiable clauses in the "sub-SAT" problem. Our outer loop is agnostic to the mechanisms of the inner loop, allowing for the use of traditional solvers for the optimization step. However, we can also transform the selected "sub-SAT" problem into a quadratic unconstrained binary optimization (QUBO) one and use specialized hardware for optimization. In contrast to existing solutions that convert a SAT instance into a QUBO one before decomposition, we choose a subset of the SAT variables before QUBO optimization. We analyze a set of variable selection methods, including a novel graph-based method that exploits the structure of a given SAT instance. The number of QUBO variables needed to encode a (sub-)SAT problem varies, so we additionally learn a model that predicts the size of sub-SAT problems that will fit a fixed-size QUBO solver. We empirically demonstrate our results on a set of randomly generated Max-SAT instances as well as real world examples from the Max-SAT evaluation benchmarks and outperform existing QUBO decomposer solutions.