On the Use of CSP Semantic Information in SAT Models
Claudia Vasconcellos-Gaete, Vincent Barichard, Frédéric Lardeux · Research in Computing Science · 2019
Constraint Satisfaction Problems (CSP) and PropositionalSatisfiability Problems (SAT) are two paradigms intended to deal with constraint-based problems.In CSP modeling, it results natural to differentiate between decision and auxiliary variables.In SAT, instances do not contain any information about the nature of variables; solvers use the Variable Selection heuristic to determine the next decision to make.This article studies the effect of transfer semantic information from a CSP model to its corresponding SAT instance, in order to guide the branching only to variables directly related to the CSP model.The results obtained suggest that this modification can speed up the resolution for some instances.