Tuesday, March 23, 2010

SAT Fitness Function

Given a solution to a satisfiability problem, we can easily check whether or not it evaluates to true by evaluating the boolean expression with the values for the variables from the solution. But how do we determine how close a partial solution was to evaluating to true? I've read of a method called SAW, but I haven't found the original paper yet, so I don't know exactly how it can be used to come up with fitness, but I will probably end up using it for my capstone as it seems to be used in other research on evolutionary computing and SAT problems.
The other way to do this is of course to evolve weights for each clause through co-evolution. I imagine that a regular GA evolving weights that emphasis those clauses that are satisfied by the fewest individuals would be a reasonable way to determine fitness. There have been some nice results in the literature of co-evolution increasing the efficiency of GAs (measured by the quality of the solutions, not the amount of time taken to run the algorithm.
The main problem with this is that there seems to be a simpler method out there (SAW) and it may be difficult to set up the experiment correctly with my framework. I will probably at least try to do it just for fun, as it will be a good test of the framework to see how well it supports a different way of doing this from the regular individual in, fitness out sort of evaluation.

No comments:

Post a Comment