Our main purpose is to enhance the efficiency of local search algorithms (issued from Walksat family) for the satisfiability problem (SAT) by including the structure of the treated instances in their resolution. The structure is described by the dependencies between the variables of the problem, interpreted as additional constraints hidden in the original formulation of the SAT instance. Checking these dependencies may allow a speeding up of the search and increasing the robustness of the incomplete methods. The extracted dependencies are implications and equivalencies between variables. The effective implementation of this purpose is achieved by an hybrid approach between a local search algorithm and an efficient DPL procedure.
展开▼
