A Deep Dive into Conflict Generating Decisions
  Boolean Satisfiability (SAT) is a well-known NP-complete problem. Despite
this theoretical hardness, SAT solvers based on Conflict Driven Clause Learning
(CDCL) can solve large SAT instances from many important domains. CDCL learns
clauses from conflicts, a technique that allows a solver to prune its search
space. The selection heuristics in CDCL prioritize variables that are involved
in recent conflicts. While only a fraction of decisions generate any conflicts,
many generate multiple conflicts.
  In this paper, we study conflict-generating decisions in CDCL in detail. We
investigate the impact of single conflict (sc) decisions, which generate only
one conflict, and multi-conflict (mc) decisions which generate two or more. We
empirically characterize these two types of decisions based on the quality of
the learned clauses produced by each type of decision. We also show an
important connection between consecutive clauses learned within the same mc
decision, where one learned clause triggers the learning of the next one
forming a chain of clauses. This leads to the consideration of similarity
between conflicts, for which we formulate the notion of conflictsproximity as a
similarity measure. We show that conflicts in mc decisions are more closely
related than consecutive conflicts generated from sc decisions. Finally, we
develop Common Reason Variable Reduction (CRVR) as a new decision strategy that
reduces the selection priority of some variables from the learned clauses of mc
decisions. Our empirical evaluation of CRVR implemented in three leading
solvers demonstrates performance gains in benchmarks from the main track of SAT
Competition-2020.
