Boolean Satisfiability (SAT) is an NP-complete problem, indicating its inherent computational hardness. However, Conflict Driven Clause Learning (CDCL) SAT solvers efficiently tackle large instances in diverse domains. Swift conflict identification is crucial for effective problem-solving, as conflicts lead to the learning of search space pruning clauses, pinpointing the root causes of conflicts and preventing their recurrence. CDCL decision heuristics prioritize variables that participated in recent conflicts, anticipating rapid conflict generation and expediting additional clause learning. In practice, only a fraction of decisions lead to conflicts, yet some decisions may yield multiple conflicts. In this paper, we delve into a detailed study of conflict generating decisions in CDCL, distinguishing between single conflict (sc) decisions, generating only one conflict, and multi-conflict (mc) decisions, producing two or more conflicts. Our empirical analysis characterizes each decision type based on the quality of the learned clauses they produce. Furthermore, our theoretical analysis reveals a crucial distinction: consecutive clauses learned within the same mc decision form a chain of clauses, absent in learned clauses from sc decisions. This leads to the hypothesis that the reasons for conflicts in mc decisions are more closely related than the reasons for conflicts in sc decisions, empirically confirmed with our introduced notion of reason proximity. Finally, we propose score reduction (sr) as a novel decision strategy, reducing the selection priority of certain variables from learned clauses in mc decisions. With four sets of benchmarks, culminating in over 1200 benchmarks, empirical evaluation of sr implemented on top of the SAT competition 2023 winner solver reveals the merit of this new strategy.

Abstract We present , a powerful local search SAT solver that effectively solves hard combinatorial problems. Its unique approach of transferring clause weights in local minima enhances its efficiency in solving problem instances. Since it is implemented on top of , benefits from practical techniques such as restart strategies and thread parallelization. Our implementation includes a parallel version that shares data structures across threads, leading to a significant reduction in memory usage. Our experiments demonstrate that outperforms similar solvers on a vast set of SAT competition benchmarks. Notably, with the parallel configuration of , we improve lower bounds for several van der Waerden numbers.

The efficiency of Conflict Driven Clause Learning (CDCL) SAT solving depends crucially on finding conflicts at a fast rate. State-of-the-art CDCL branching heuristics such as VSIDS, CHB and LRB conform to this goal. We take a closer look at the way in which conflicts are generated over the course of a CDCL SAT search. Our study of the VSIDS branching heuristic shows that conflicts are typically generated in short bursts, followed by what we call a conflict depression phase in which the search fails to generate any conflicts in a span of decisions. The lack of conflict indicates that the variables that are currently ranked highest by the branching heuristic fail to generate conflicts. Based on this analysis, we propose an exploration strategy, called expSAT, which randomly samples variable selection sequences 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 VSIDS activity scores. An extensive empirical evaluation with four state-of-the-art CDCL SAT solvers demonstrates good-to-strong performance gains with the expSAT approach.

We present a tight integration of SAT with CP, called SAT(gc), which embeds global constraints into SAT. A prototype is implemented by integrating the state of the art SAT solver ZCHAFF and the generic constraint solver GECODE. Experiments are carried out for benchmarks from puzzle domains and planning domains to reveal insights in compact representation, solving effectiveness, and novel usability of the new framework.