Abstract
Boolean Satisfiability (SAT) is a fundamental problem in computer science, with profound implications in Computational Complexity, Logic, and Artificial Intelligence. Given a set of clauses over boolean variables, the SAT solving task is to determine variable assignments which satisfy that set of clauses or report unsatisfiability, in case no such assignments exist. In general, SAT solving is intractable. Despite the theoretical hardness, many large real-world problems from domains, such as hardware design verification, software debugging, planning, and encryption are routinely solved by using SAT solvers. At present, the most dominant SAT solvers are based on Conflict Driven Clause Learning (CDCL). The efficiency CDCL SAT solving depends crucially on finding conflicts at a fast rate. State-of- the-art CDCL branching heuristics such as VSIDS and LRB conform to this goal. In this talk, I will present our study (AAAI 2020) of the VSIDS and LRB branching heuristics and a novel exploration guided CDCL extension named expSAT, which is designed based on the insights obtained from our study.. Our study shows that both of these heuristics typically generate conflicts in short bursts, followed by what we call a conflict depression (CD) phase, in which the search fails to generate any conflicts for a number of consecutive decisions. This lack of conflict indicates that the variables which are currently ranked highest by the branching heuristic fail to generate conflicts. Based on this analysis of conflict depression, we propose expSAT, which randomly samples variable selection sequences amid a CD phase, in order to learn an updated heuristic from the generated conflicts. The goal is to escape from conflict depressions expeditiously. The branching heuristic deployed in expSAT combines these updates with the standard activity scores of VSIDS and LRB. An extensive empirical evaluation with five state-of-the-art CDCL SAT solvers demonstrates good-to-strong performance gains with the expSAT approach for benchmark instances from SAT Competitions 2017 and 2018, and impressive gains over a fixed set of hard bitcoin mining instances.
Guiding CDCL SAT Search via Random Exploration amid Conflict Depression.Md Solimul Chowdhury, Martin Müller, Jia-Huai You: AAAI 2020: 1428-1435