importData.List ( nub )importData.Maybe ( fromJust )dataFormula = Var String | And Formula Formula |

Or Formula Formula | Not Formula

getVarsDup (Var v) = [v]

getVarsDup (And f1 f2) = (getVarsDup f1) ++ (getVarsDup f2)

getVarsDup (Or f1 f2) = (getVarsDup f1) ++ (getVarsDup f2)

getVarsDup (Not f) = getVarsDup f

genValues n = genAux $ [replicate n True]

wheregenAux (v:vs) =ifnot $ or $ vthenv:vs

elsegenAux ((next v):v:vs)

next (True:ts) = (False:ts)

next (False:ts) = (True:(next ts))

solveFormula (Var v) env = fromJust $ lookup v env

solveFormula (And f1 f2) env = (solveFormula f1 env) &&

(solveFormula f2 env)

solveFormula (Or f1 f2) env = (solveFormula f1 env) ||

(solveFormula f2 env)

solveFormula (Not f) env = not $ solveFormula f env

allSolutions f = map (solveFormula f) (map (zip vars) vals)

wherevars = nub $ getVarsDup f

vals = genValues (length vars)

-- solve the SAT problem

sat f = or $ allSolutions f

-- pointfree!

sat2 = or . allSolutions

The idea is the same as creating a truth-table for the formula and then looking for a T in the possible values for it. Function

`genValues`

generates all possible values for the atomic propositions, and this is fed into `solveFormula`

. It would be very easy to alter the code to output the complete truth-table; I leave it as an exercise to the reader. Another standard exercise in logic textbooks is to prove that if a formula contains n atomic propositions, the truth-table will have 2^n lines. Thus, generating all combinations is easily seen to be exponential in time.But the fact that it is hard for the computer to solve doesn't mean that it's hard for someone to write a (naive) program to solve it. In practical applications, like circuit design, we may need to solve SAT for thousands of variables, and the naive algorithm would not work. For this we must use a more clever technique, like Binary Decision Diagrams. They're not that hard to code either; the book Expert F# includes an example of BDDs in F#.

## No comments:

Post a Comment