cMinor - 1 month ago 31

Java Question

Is there any algorithm to reduce sat problem.

*Satisfiability is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE. Equally important is to determine whether no such assignments exist, which would imply that the function expressed by the formula is identically FALSE for all possible variable assignments. In this latter case, we would say that the function is unsatisfiable; otherwise it is satisfiable. To emphasize the binary nature of this problem, it is frequently referred to as Boolean or propositional satisfiability. The shorthand "SAT" is also commonly used to denote it, with the implicit understanding that the function and its variables are all binary-valued.*

I have used genetic algorithms to solve this, but it would be easier if is reduced first?.

Answer

Take a look at Reduced Order Binary Decision Diagrams (ROBDD). It provides a way of compressing boolean expressions to a reduced canonical form. There's plenty of software around for performing the BDD reduction, the wikipedia link above for ROBDD contains a nice list of external links to other relevant packages at the bottom of the article.