Changed arguments order to match other functions

This commit is contained in:
Dimitri Lozeve 2016-08-03 20:33:25 +01:00
parent e36db42ec7
commit c683e624bc
No known key found for this signature in database
GPG key ID: 12B390E6BD7CF219

8
Sat.hs
View file

@ -195,13 +195,13 @@ resolveAll f = case findMatchingPair f of
-- applies resolveAll and the unit propagation and pure literals -- applies resolveAll and the unit propagation and pure literals
-- rules, until it reaches the empty formula (therefore SAT) or an -- rules, until it reaches the empty formula (therefore SAT) or an
-- empty clause (therefore UNSAT). -- empty clause (therefore UNSAT).
resolutionSolve :: Assignment -> CNF -> Result resolutionSolve :: (CNF, Assignment) -> Result
resolutionSolve asst [] = SAT asst resolutionSolve ([], asst) = SAT asst
resolutionSolve asst f resolutionSolve (f, asst)
| [] `elem` f = UNSAT | [] `elem` f = UNSAT
| otherwise = | otherwise =
let (f', asst') = (pureLitRule . unitPropagate) (f, asst) in let (f', asst') = (pureLitRule . unitPropagate) (f, asst) in
resolutionSolve asst' (resolveAll f') resolutionSolve (resolveAll f', asst')