Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Resource-Constrained Heuristic for Max-SAT

Brian Matejek, Daniel Elenius, Cale Gentry, David Stoker, Adam Cobb

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.

Resource-Constrained Heuristic for Max-SAT

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.

Paper Structure

This paper contains 25 sections, 3 equations, 2 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Background and Notation
  3. Methodology
  4. Decomposer
  5. Random Selector.
  6. Energy Selector.
  7. Softmax Selector.
  8. Graph Selector.
  9. Clause Pruning
  10. Inner-Optimizer
  11. SAT Solvers.
  12. QUBO Optimizers.
  13. Composer
  14. Early Stopping
  15. Experimental Setup
  16. ...and 10 more sections

Figures (2)

  • Figure 1: We construct a weighted bipartite graph from any k-SAT instance. Each of the $N$ variables and $L$ clauses receives a single node in the graph. We add an edge between nodes $x_i$ and $c_j$ if clause $c_j$ contains variable $x_i$.
  • Figure 2: The energy and softmax selectors outperform the graph and random ones (top). Each of the inner-optimizers perform similarly well in their optimal configurations (middle). Our Max-SAT energies typically decrease as we reduce the constraints on the inner-optimizer (bottom).