Preliminary Results on Exploration-Driven Satisfiability Solving

Authors

  • Md Solimul Chowdhury The University of Alberta
  • Martin Müller The University of Alberta
  • Jia-Huai You The University of Alberta

DOI:

https://doi.org/10.1609/aaai.v32i1.12164

Keywords:

Satisfiability Solving, SAT, Exploration, Random Walk, Monte-Carlo Tree Search, Reinforcement Learning

Abstract

In this abstract, we present our study of exploring the SAT search space via random-sampling, with the goal of improving Conflict Directed Clause Learning (CDCL) SAT solvers. Our proposed CDCL SAT solving algorithm expSAT uses a novel branching heuristic expVSIDS. It combines the standard VSIDS scores with heuristic scores derived from exploration. Experiments with application benchmarks from recent SAT competitions demonstrate the potential of the expSAT approach for improving CDCL SAT solvers.

AAAI 2018 Proceedings Cover

Downloads

Published

2018-04-29

How to Cite

Chowdhury, M. S., Müller, M., & You, J.-H. (2018). Preliminary Results on Exploration-Driven Satisfiability Solving. Proceedings of the AAAI Conference on Artificial Intelligence, 32(1). https://doi.org/10.1609/aaai.v32i1.12164

Issue

Vol. 32 No. 1 (2018): Thirty-Second AAAI Conference on Artificial Intelligence

Section

Student Abstract Track