We are very excited to join forces with MLCommons and OctoML.ai! Contact Grigori Fursin for more details!

Improving SAT Solvers via Blocked Clause Decomposition

lib:1ad86ba4fc88c58c (v1.0.0)

Authors: Jingchao Chen
ArXiv: 1604.00536
Document:  PDF  DOI 
Abstract URL: http://arxiv.org/abs/1604.00536v1


The decision variable selection policy used by the most competitive CDCL (Conflict-Driven Clause Learning) SAT solvers is either VSIDS (Variable State Independent Decaying Sum) or its variants such as exponential version EVSIDS. The common characteristic of VSIDS and its variants is to make use of statistical information in the solving process, but ignore structure information of the problem. For this reason, this paper modifies the decision variable selection policy, and presents a SAT solving technique based on BCD (Blocked Clause Decomposition). Its basic idea is that a part of decision variables are selected by VSIDS heuristic, while another part of decision variables are selected by blocked sets that are obtained by BCD. Compared with the existing BCD-based technique, our technique is simple, and need not to reencode CNF formulas. SAT solvers for certified UNSAT track can apply also our BCD-based technique. Our experiments on application benchmarks demonstrate that the new variables selection policy based on BCD can increase the performance of SAT solvers such as abcdSAT. The solver with BCD solved an instance from the SAT Race 2015 that was not solved by any solver so far. This shows that in some cases, the heuristic based on structure information is more efficient than that based on statistical information.

Relevant initiatives  

Related knowledge about this paper Reproduced results (crowd-benchmarking and competitions) Artifact and reproducibility checklists Common formats for research projects and shared artifacts Reproducibility initiatives

Comments  

Please log in to add your comments!
If you notice any inapropriate content that should not be here, please report us as soon as possible and we will try to remove it within 48 hours!