Dynamic analysis of constraint-variable dependencies to guide SAT diagnosis

An important aspect of the Boolean satisfiability problem is to derive an ordering of variables such that branching on that order results in a faster, more efficient search. Contemporary techniques employ either variable-activity or clause-connectivity based heuristics, but not both, to guide the search. This paper advocates for simultaneous analysis of variable-activity and clause-connectivity to derive an order for SAT search. Preliminary results demonstrate that the variable order derived by our approach can significantly expedite the search. As the search proceeds, clause database is updated due to added conflict clauses. Therefore, the variable activity and connectivity information changes dynamically. Our technique analyzes this information and recomputes the variable order whenever the search is restarted. Preliminary experiments show that such a dynamic analysis of constraint-variable relationships significantly improves the performance of the SAT solvers. Our technique is very fast and this analysis time is a negligible (in milliseconds) even for instances that contain a large number of variables and constraints. This paper presents preliminary experiments, analyzes the results and comments upon future research directions.