Решение SAT с библиотекой haskell SBV: как создать предикат из проанализированной строки?
Я хочу разобрать String это изображает формулу высказывания, а затем найти все модели формулы высказывания с помощью решателя SAT.
Теперь я могу разобрать пропозициональную формулу с пакетом hatt; увидеть testParse функция ниже.
Я также могу запустить SAT Solver с библиотекой SBV; увидеть testParse функция ниже.
Вопрос: Как во время выполнения генерировать значение типа Predicate лайк myPredicate в библиотеке SBV, которая представляет пропозициональную формулу, которую я только что проанализировал из строки? Я только знаю, как вручную ввести forSome_ $ \x y z -> ... выражение, но не как написать функцию преобразователя из Expr значение к значению типа 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.
-}
Информация, которая может быть полезна:
Вот ссылка на BitVectors.Data: http://hackage.haskell.org/package/sbv-3.0/docs/src/Data-SBV-BitVectors-Data.html
Вот пример кода формы examples.Puzzles.PowerSet:
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
Вот тип данных Expr (из библиотеки hatt):
data Expr = Variable Var
| Negation Expr
| Conjunction Expr Expr
| Disjunction Expr Expr
| Conditional Expr Expr
| Biconditional Expr Expr
deriving Eq
2 ответа
Работа с SBV
Работа с SBV требует, чтобы вы следовали за типами и понимали Predicate это просто Symbolic SBool, После этого шага важно, чтобы вы исследовали и обнаружили Symbolic это монада - да, монада!
Теперь, когда вы знаете, что у вас есть монада, тогда что-нибудь в пикше Symbolic должно быть тривиально объединить, чтобы построить любой SAT, который вы желаете. Для вашей проблемы вам просто нужен простой интерпретатор вашего AST, который создает Predicate,
Code Walk-Through
Код все включено в одну непрерывную форму ниже, но я буду проходить через забавные части. Точка входа solveExpr который принимает выражения и выдает результат SAT:
solveExpr :: Expr -> IO AllSatResult
solveExpr e0 = allSat prd
Применение SBV's allSat с предикатом вроде как очевидно. Чтобы построить этот предикат, мы должны объявить экзистенциальный SBool для каждой переменной в нашем выражении. Пока давайте предположим, что у нас есть vs :: [String] где каждая строка соответствует одному из Var из выражения.
prd :: Predicate
prd = do
syms <- mapM exists vs
let env = M.fromList (zip vs syms)
interpret env e0
Обратите внимание на то, как здесь проникают основы языка программирования. Теперь нам нужна среда, которая отображает имена переменных выражений в символические логические значения, используемые SBV.
Далее мы интерпретируем выражение, чтобы произвести наш Predicate, Функция интерпретации использует среду и просто применяет функцию SBV, которая соответствует цели каждого конструктора из хеттов. 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"
И это все! Остальное - просто котельная плита.
Полный код
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
forSome_ является членом Provable класс, так что, кажется, было бы достаточно, чтобы определить экземпляр Provable Expr, Почти все функции в SVB использование Provable так что это позволит вам использовать все эти изначально Expr, Сначала мы конвертируем Expr к функции, которая ищет значения переменных в Vector, Вы также можете использовать Data.Map.Map или что-то в этом роде, но среда не меняется после создания и Vector дает постоянный поиск по времени:
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 по существу определяет две функции: forAll_, forAll, forSome_, forSome, Мы должны сгенерировать все возможные карты переменных для значений и применить функцию к картам. Выбор способа обработки результатов будет сделан Symbolic монада:
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)
куда fresh является функцией, которая "количественно" определяет данную переменную, связывая ее со всеми возможными значениями.
fresh :: Var -> Symbolic (Int, SBool)
fresh (Var var) = forall >>= \a -> return (fromEnum var, a)
Если вы определите одну из этих функций для каждой из четырех функций, у вас будет довольно много повторяющегося кода. Таким образом, вы можете обобщить вышесказанное следующим образом:
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)
Если это точно сбивает с толку то, что происходит, Provable Экземпляр может быть достаточно, чтобы объяснить:
instance Provable Expr where
forAll_ = quantExp forall forall_ []
forAll = quantExp forall forall_
forSome_ = quantExp exists exists_ []
forSome = quantExp exists exists_
Тогда ваш тестовый пример:
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