Stochastic Local Search over Minterms on Structured SAT Instances

Authors

  • Wenxiang Chen Colorado State University
  • Darrell Whitley Colorado State University
  • Adele Howe Colorado State University
  • Brian Goldman Colorado State University

DOI:

https://doi.org/10.1609/socs.v7i1.18403

Keywords:

satisfiability, stochastic local search, structured problems, representation, minterm

Abstract

We observed that Conjunctive Normal Form (CNF) encodings of structured SAT instances often have a set of consecutive clauses defined over a small number of Boolean variables. To exploit the pattern, we propose a transformation of CNF to an alternative representation, Conjunctive Minterm Canonical Form (CMCF). The transformation is a two-step process: CNF clauses are first partitioned into disjoint subsets such that each subset contains CNF clauses with shared Boolean variables. CNF clauses in each subset are then replaced by Minterm Canonical Form (i.e., partial solutions), which is found by enumeration. We show empirically that a simple Stochastic Local Search (SLS) solver based on CMCF can consistently achieve a higher success rate using fewer evaluations than the SLS solver WalkSAT on two representative classes of structured SAT problems.

Downloads

Published

2021-09-01