4.8.4 Exploiting Propositional Structure in Local Search

Stochastic local search is simpler for CSPs that are in the form of propositional satisfiability problems, with Boolean variables and constraints that are clauses. Each local search step can be made more efficient for three main reasons:

  • Because only one alternative value exists for each assignment to a variable, the algorithm does not have to search through the alternative values.
  • Changing any value in an unsatisfied clause makes the clause satisfied. As a result, it is easy to satisfy a clause, but this may make other clauses unsatisfied.
  • If a variable is changed to be true, only those clauses where it appears negatively can be made unsatisfied and similarly for variables becoming false. This enables fast indexing of clauses.

It is possible to convert any finite CSP into a propositional satisfiable problem. A variable Y with domain {v1,...,vk} can be converted into k Boolean variables {Y1,...,Yk}, where Yi is true when Y has value vi and is false otherwise. Each Yi is called an indicator variable. There is a clause for each false tuple in each constraint, which specifies which assignments to the Yi are not allowed by the constraint. There are also constraints that specify that Yi and Yj cannot both be true when i≠j. There is also a constraint that one of the variables Yi must have value true. Converting a CSP into a propositional satisfiability problem has three potential advantages:

  • Each local step can be simpler and therefore implemented more efficiently.
  • The search space is expanded. In particular, before a solution has been found, more than one Yi could be true (which corresponds to Y having multiple values) or all of the Yi variables could be false (which corresponds to Y having no values). This can mean that some assignments that were local minima in the original problem may not be local minima in the new representation.
  • Satisfiability has been studied much more extensively than most other types of CSPs and more efficient solvers are currently known because more of the space of potential algorithms has been explored by researchers.

Whether the conversion makes search performance better for a particular example is, again, an empirical question.