Rozwiązywanie sat z biblioteką SBK haskell: jak wygenerować predykat z analizowanego łańcucha?

Question

Chcę przetworzyć String, który przedstawia formułę zdaniową, a następnie znaleźć wszystkie modele formuły zdaniowej z solver SAT.

Teraz mogę przeanalizować formułę propositional z pakietem hatt; zobacz poniżej funkcję testParse.

Mogę również uruchomić wywołanie funkcji solwera SAT z biblioteką SBV; zobacz poniżej funkcję testParse.

Pytanie: jaki sposób, przy starcie, generują wartość typu Predicate jak myPredicate w bibliotece SBV który reprezentuje formułę zdaniową właśnie analizowany z łańcucha? Wiem tylko, jak ręcznie wpisać wyrażenie forSome_ $ \x y z -> ..., ale nie wiem, jak napisać funkcję konwertera z wartości Expr do wartości typu Predicate.

-- cabal install sbv hatt 
import Data.Logic.Propositional 
import Data.SBV 


-- Random test formula: 
-- (x or ~z) and (y or ~z) 

-- graphical depiction, see: https://www.wolframalpha.com/input/?i=%28x+or+~z%29+and+%28y+or+~z%29 

testParse = parseExpr "test source" "((X | ~Z) & (Y | ~Z))" 

myPredicate :: Predicate 
myPredicate = forSome_ $ \x y z -> ((x :: SBool) ||| (bnot z)) &&& (y ||| (bnot z)) 

testSat = do 
     x <- allSat $ myPredicate 
     putStrLn $ show x  


main = do 
     putStrLn $ show $ testParse 
     testSat 


    {- 
     Need a function that dynamically creates a Predicate 
(as I did with the function (like "\x y z -> ..") for an arbitrary expression of type "Expr" that is parsed from String. 
    -} 

informacje, które mogą być pomocne:

Oto link do BitVectors.Data: http://hackage.haskell.org/package/sbv-3.0/docs/src/Data-SBV-BitVectors-Data.html

Oto przykład kodu Examples.Puzzles.PowerSet forma:

import Data.SBV 

genPowerSet :: [SBool] -> SBool 
genPowerSet = bAll isBool 
    where isBool x = x .== true ||| x .== false 

powerSet :: [Word8] -> IO() 
powerSet xs = do putStrLn $ "Finding all subsets of " ++ show xs 
       res <- allSat $ genPowerSet `fmap` mkExistVars n 

Oto typ danych Expr (z biblioteki hatt):

data Expr = Variable  Var 
      | Negation  Expr 
      | Conjunction Expr Expr 
      | Disjunction Expr Expr 
      | Conditional Expr Expr 
      | Biconditional Expr Expr 
      deriving Eq 

Answer 1

Praca z SBV

Praca z SBV wymaga zgodne z typami i realizować Predicate tylko Symbolic SBool. Po tym kroku ważne jest, abyś zbadał i odkrył, że jest to monada - moneta!

Teraz, gdy wiesz, że masz monadę, to wszystko, co jest w plamie, które jest Symbolic powinno być trywialne, aby łączyć je w celu zbudowania dowolnego SAT, którego pragniesz. Dla twojego problemu potrzebujesz prostego interpretera na twoim AST, który buduje Predicate.

Kod przechodni

Kod jest wszystko wliczone w jednej formie ciągłej poniżej ale będę krok po kroku części zabawy. Punkt wejścia jest solveExpr która odbywa wyrażenia i daje wynik Sat:

solveExpr :: Expr -> IO AllSatResult 
solveExpr e0 = allSat prd 

Zastosowanie SBV na allSat do orzecznika jest jakby oczywiste. Aby zbudować ten predykat, musimy zadeklarować egzystencjalne SBool dla każdej zmiennej w naszym wyrażeniu. Na razie załóżmy, że mamy vs :: [String], gdzie każdy ciąg odpowiada jednemu z Var z wyrażenia.

prd :: Predicate 
    prd = do 
     syms <- mapM exists vs 
     let env = M.fromList (zip vs syms) 
     interpret env e0 

Zauważ, jak wkradają się tutaj podstawy języka programowania. Potrzebujemy teraz środowiska, które odwzorowuje nazwy zmiennych wyrażeń na symboliczne wartości logiczne używane przez SBV.

Następnie interpretujemy wyrażenie, aby wyprodukować naszą Predicate. Funkcja interpretacji używa środowiska i po prostu stosuje funkcję SBV, która pasuje do intencji każdego konstruktora z typu hatt'a Expr.

interpret :: Env -> Expr -> Predicate 
    interpret env expr = do 
    let interp = interpret env 
    case expr of 
    Variable v -> return (envLookup v env) 
    Negation e -> bnot `fmap` interp e 
    Conjunction e1 e2 -> 
    do r1 <- interp e1 
     r2 <- interp e2 
     return (r1 &&& r2) 
    Disjunction e1 e2 -> 
    do r1 <- interp e1 
     r2 <- interp e2 
     return (r1 ||| r2) 
    Conditional e1 e2 -> error "And so on" 
    Biconditional e1 e2 -> error "And so on" 

I to jest to! Reszta to tylko płyta kotła.

Pełny kod

import Data.Logic.Propositional hiding (interpret) 
import Data.SBV 
import Text.Parsec.Error (ParseError) 
import qualified Data.Map as M 
import qualified Data.Set as Set 
import Data.Foldable (foldMap) 
import Control.Monad ((<=<)) 

testParse :: Either ParseError Expr 
testParse = parseExpr "test source" "((X | ~Z) & (Y | ~Z))" 

type Env = M.Map String SBool 

envLookup :: Var -> Env -> SBool 
envLookup (Var v) e = maybe (error $ "Var not found: " ++ show v) id 
          (M.lookup [v] e) 

solveExpr :: Expr -> IO AllSatResult 
solveExpr e0 = allSat go 
where 
    vs :: [String] 
    vs = map (\(Var c) -> [c]) (variables e0) 

    go :: Predicate 
    go = do 
     syms <- mapM exists vs 
     let env = M.fromList (zip vs syms) 
     interpret env e0 
    interpret :: Env -> Expr -> Predicate 
    interpret env expr = do 
    let interp = interpret env 
    case expr of 
    Variable v -> return (envLookup v env) 
    Negation e -> bnot `fmap` interp e 
    Conjunction e1 e2 -> 
    do r1 <- interp e1 
     r2 <- interp e2 
     return (r1 &&& r2) 
    Disjunction e1 e2 -> 
    do r1 <- interp e1 
     r2 <- interp e2 
     return (r1 ||| r2) 
    Conditional e1 e2 -> error "And so on" 
    Biconditional e1 e2 -> error "And so on" 

main :: IO() 
main = do 
     let expr = testParse 
     putStrLn $ "Solving expr: " ++ show expr 
     either (error . show) (print <=< solveExpr) expr 

Answer 2

forSome_ jest członkiem klasy Provable, więc wydaje się, że to wystarczy, aby określić wystąpienie Provable Expr. Prawie wszystkie funkcje w SVB używają Provable, więc pozwoliłoby to na użycie wszystkich tych natywnie Expr. Najpierw przekształcamy Expr w funkcję, która wyszukuje wartości zmiennych w Vector. Można również użyć Data.Map.Map lub coś podobnego, ale środowisko nie ulega zmianie po utworzeniu i Vector daje stały czas wyszukiwania:

import Data.Logic.Propositional 
import Data.SBV.Bridge.CVC4 
import qualified Data.Vector as V 
import Control.Monad 

toFunc :: Boolean a => Expr -> V.Vector a -> a 
toFunc (Variable (Var x)) = \env -> env V.! (fromEnum x) 
toFunc (Negation x) = \env -> bnot (toFunc x env) 
toFunc (Conjunction a b) = \env -> toFunc a env &&& toFunc b env 
toFunc (Disjunction a b) = \env -> toFunc a env ||| toFunc b env 
toFunc (Conditional a b) = \env -> toFunc a env ==> toFunc b env 
toFunc (Biconditional a b) = \env -> toFunc a env <=> toFunc b env 

Provable zasadniczo definiuje dwie funkcje: forAll_, forAll, forSome_, forSome. Musimy wygenerować wszystkie możliwe mapy zmiennych do wartości i zastosować funkcję do map. Wybór jak dokładnie obsłużyć wyniki zostaną wykonane przez Symbolic monady:

forAllExp_ :: Expr -> Symbolic SBool 
forAllExp_ e = (m0 >>= f . V.accum (const id) (V.replicate (fromEnum maxV + 1) false) 
    where f = return . toFunc e 
     maxV = maximum $ map (\(Var x) -> x) (variables e) 
     m0 = mapM fresh (variables e) 

Gdzie fresh jest funkcją, która „ilościowo” danej zmiennej poprzez skojarzenie go z wszystkich możliwych wartości.

fresh :: Var -> Symbolic (Int, SBool) 
fresh (Var var) = forall >>= \a -> return (fromEnum var, a) 

Jeśli zdefiniujesz jedną z tych funkcji dla każdej z czterech funkcji, będziesz miał bardzo dużo bardzo powtarzalnych kodów. Więc można uogólnić powyższe następująco:

quantExp :: (String -> Symbolic SBool) -> Symbolic SBool -> [String] -> Expr -> Symbolic SBool 
quantExp q q_ s e = m0 >>= f . V.accum (const id) (V.replicate (fromEnum maxV + 1) false) 
    where f = return . toFunc e 
     maxV = maximum $ map (\(Var x) -> x) (variables e) 
     (v0, v1) = splitAt (length s) (variables e) 
     m0 = zipWithM fresh (map q s) v0 >>= \r0 -> mapM (fresh q_) v1 >>= \r1 -> return (r0++r1) 

fresh :: Symbolic SBool -> Var -> Symbolic (Int, SBool) 
fresh q (Var var) = q >>= \a -> return (fromEnum var, a) 

Jeśli jest niejasna dokładnie to, co się dzieje, instancja Provable może wystarczyć do wyjaśnienia:

instance Provable Expr where 
    forAll_ = quantExp forall forall_ [] 
    forAll = quantExp forall forall_ 
    forSome_ = quantExp exists exists_ [] 
    forSome = quantExp exists exists_ 

Wtedy twój przypadek testowy:

myPredicate :: Predicate 
myPredicate = forSome_ $ \x y z -> ((x :: SBool) ||| (bnot z)) &&& (y ||| (bnot z)) 

myPredicate' :: Predicate 
myPredicate' = forSome_ $ let Right a = parseExpr "test source" "((X | ~Z) & (Y | ~Z))" in a 

testSat = allSat myPredicate >>= print 
testSat' = allSat myPredicate >>= print