Dynamic Polarity Adjustment in a Parallel SAT Solver

In this paper, a new heuristic for polarity selection is proposed. This heuristic is defined for parallel SAT solvers. The selected polarity is an important component of modern SAT solvers, in particular in portfolio ones. Indeed, these solvers are often based on the cooperation/competition principle. In this case, the polarity can be used to guide the solver in the search space. A criterion based on the intention notion is proposed in order to evaluate whether two solvers are to study the same search space or not. Once this criterion defined, a dynamical heuristic polarity is proposed for tuning the different solvers. Experimental results show that our approach is efficient and provides significant improvements on a range of industrial instances.