Special Olympics, part 3

gistfile1.txt

Задача и алгоритм: http://en.wikipedia.org/wiki/2-satisfiability#Limited_backtracking

Тестовые данные ниже. Первая строчка - число переменных, дальше проверки в формате "переменная - пробел - переменная". Если номер переменной отрицательный, то она должна быть False, если положительный - True.

Большой файл для примера: https://spark-public.s3.amazonaws.com/algo2/datasets/2sat1.txt у меня обрабатывается 6 минут, ответ "solved"

olympics3.hs

module Main where

import Data.Functor
import Data.Function
import Data.List (sortBy)
import Data.Maybe
import qualified Data.Vector.Unboxed as U

import Debug.Trace

type Clause = (Int, Int)
type Clauses = U.Vector Clause
type Var = (Bool, Bool)
type Vars = U.Vector Var

readClause :: String -> Clause
readClause s = let [v1, v2] = words s
                in (read v1, read v2)

getVar :: Vars -> Int -> Var
getVar vars i = vars `U.unsafeIndex` (abs i - 1)

checkVar :: Vars -> Int -> Bool
checkVar vars i
    | not isset = True
    | otherwise = value == (i > 0)
    where
    (isset, value) = getVar vars i

checkClause :: Vars -> Clause -> Bool
checkClause vars (i1, i2) = checkVar vars i1 || checkVar vars i2

good4
1 2
-1 3
3 4
-2 -4
    checkClauses :: Clauses -> Vars -> Bool
checkClauses cl vars = U.all (checkClause vars) cl

-- find unset var and set it to value. return new vars or nothing, if all vars set
setVar :: Bool -> Vars -> Maybe Vars
setVar v vars = case U.findIndex (\(isset, _) -> not isset) vars of
                    Nothing -> Nothing
                    Just i  -> Just $ vars U.// [(i, (True, v))]

-- create list of forces vars, may be empty
getUpdates :: Clauses -> Vars -> [(Int, Var)]
getUpdates cl vars = U.foldr upd [] cl
    where
--    fixvar a b c d _ | trace ("fv " ++ show a ++ " " ++ show b ++ " " ++ show c +
+ " " ++ show d) False = undefined
    fixvar i1 (True, v1) i2 (False, _) xs | (i1 > 0) /= v1 = (abs i2 - 1, (True, i2
 > 0)) : xs
    fixvar i1 (False, _) i2 (True, v2) xs | (i2 > 0) /= v2 = (abs i1 - 1, (True, i1 > 0)) : xs
    fixvar _ _ _ _ xs = xs

--    upd clause _ | not $ checkClause vars clause = error "clause failed"
    upd (i1, i2) = fixvar i1 (getVar vars i1) i2 (getVar vars i2)

-- force vars to required values. return new var list or nothing if contradiction
forceVars :: Clauses -> Vars -> Maybe Vars
forceVars cl vars
--    | trace ("force " ++ show vars) False = undefined
    | not $ checkClauses cl vars = Nothing
    | null updates = Just vars
    | otherwise = forceVars cl $ vars `U.unsafeUpd` updates
    where
    updates = getUpdates cl vars

solve :: Clauses -> Maybe Vars -> Vars -> Maybe Vars
solve cl backtrack vars 
--    | trace ("solve " ++ show vars ++ " " ++ show forced) False = undefined
    | isJust forced && isNothing nextvars = forced
    | isJust forced = trace (show unset) $ solve cl (Just vars) (fromJust nextvars)
    | isNothing backtrack = Nothing
    | otherwise = solve cl Nothing (fromJust btvars)
    where
    forced = forceVars cl vars
    nextvars = setVar True (fromJust forced)
    btvars = setVar False (fromJust backtrack)
    unset = U.foldr' (\(isset,_) c -> if not isset then c + 1 else c) (0 :: Int) $ fromJust nextvars

-- put most used vars in front of list, to be filled first
rewriteClauses :: Int -> Clauses -> (Int, Clauses)
rewriteClauses nvars clauses = (used, U.map fixclause clauses)
    where
    base = U.replicate nvars 0
    sums = U.accum (+) base $ U.foldr (\(v1, v2) xs -> (abs v1 - 1, 1):(abs v2 - 1, 1):xs) [] clauses
    used = U.length $ U.filter (/= 0) sums
    counts = sortBy (flip (compare `on` snd)) $ zip [1..] $ U.toList sums
    newvals = base U.// zipWith (\n (i, _) -> (i - 1, n)) [1..] counts
    fixval i = signum i * (newvals U.! (abs i - 1))
    fixclause (i1, i2) = (fixval i1, fixval i2)

main :: IO ()
main = do
    (hdr:body) <- lines <$> getContents
    let nvars = read hdr
    let clauses = U.fromList $ map readClause body
    let (used, newclauses) = rewriteClauses nvars clauses
    let vars = U.replicate used (False, False)
    let answer = solve newclauses Nothing vars
    print $ "using " ++ show used ++ " vars of " ++ show nvars
    print $ case answer of
                Nothing -> "unsolvable"
                Just avars -> do
                        let checkset = U.all fst avars
                        let testcl = checkClauses newclauses avars
                        if checkset && testcl then "solved"
                                              else "algorithm error:" ++ show checkset ++ " " ++ show testcl

solvable-1

4
1 2
-1 -2
3 -2
3 2

solvable-2

4
1 2
-1 3
3 4
-2 -4

unsolvable-1

5
1 1
-1 2
-1 3
-2 -3
4 5