{- |
Description: Module for sat solving on 'PropositionalFormula's.
License: GNU LGPLv3
Maintainer: paul.bittner@uni-ulm.de

Module for sat solving on 'PropositionalFormula's.
Uses the picosat library.
-}
module SAT (
    sat,
    satAssignment,
    tautCounterExample,
    taut,
    contradicts,
    toIntCNF) where

import UUID
import Propositions
import Util

import Picosat
import Control.Monad.State
import Data.Bimap
import Data.List (find)
import Data.Maybe (isJust)

import System.IO.Unsafe (unsafePerformIO)

-- | Returns /true/ iff the given propositional formula is satisfiable.
sat :: (Show a, Ord a) => PropositionalFormula a -> Bool
sat :: PropositionalFormula a -> Bool
sat = Maybe (Assignment a) -> Bool
forall a. Maybe a -> Bool
isJust(Maybe (Assignment a) -> Bool)
-> (PropositionalFormula a -> Maybe (Assignment a))
-> PropositionalFormula a
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.PropositionalFormula a -> Maybe (Assignment a)
forall a.
(Show a, Ord a) =>
PropositionalFormula a -> Maybe (Assignment a)
satAssignment

-- | Returns a satisfying assignment @Just a@ for the given propositional formula
-- iff the formula is satisfiable.
-- Returns @Nothing@ otherwise.
satAssignment :: (Show a, Ord a) => PropositionalFormula a -> Maybe (Assignment a)
satAssignment :: PropositionalFormula a -> Maybe (Assignment a)
satAssignment p :: PropositionalFormula a
p = 
    let (cnf :: [[Int]]
cnf, m :: Bimap a Int
m) = PropositionalFormula a -> ([[Int]], Bimap a Int)
forall a. Ord a => PropositionalFormula a -> ([[Int]], Bimap a Int)
toIntCNF PropositionalFormula a
p in
        IO (Maybe (Assignment a)) -> Maybe (Assignment a)
forall a. IO a -> a
unsafePerformIO (IO (Maybe (Assignment a)) -> Maybe (Assignment a))
-> IO (Maybe (Assignment a)) -> Maybe (Assignment a)
forall a b. (a -> b) -> a -> b
$ do -- TODO: Remove this hack
            Solution
res <- [[Int]] -> IO Solution
solve [[Int]]
cnf
            case Solution
res of
                Solution s :: [Int]
s -> Maybe (Assignment a) -> IO (Maybe (Assignment a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Assignment a) -> IO (Maybe (Assignment a)))
-> Maybe (Assignment a) -> IO (Maybe (Assignment a))
forall a b. (a -> b) -> a -> b
$ Assignment a -> Maybe (Assignment a)
forall a. a -> Maybe a
Just
                    (\x :: a
x -> case (Int -> Bool) -> [Int] -> Maybe Int
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\i :: Int
i -> Int -> Int
forall a. Num a => a -> a
abs Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Bimap a Int
m Bimap a Int -> a -> Int
forall a b. (Ord a, Ord b) => Bimap a b -> a -> b
! a
x) [Int]
s of
                        Nothing -> [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error ([Char] -> Bool) -> [Char] -> Bool
forall a b. (a -> b) -> a -> b
$ (a -> [Char]
forall a. Show a => a -> [Char]
show a
x)[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++" is not a variable in this configuration!"
                        Just i :: Int
i -> Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0)
                Unsatisfiable -> Maybe (Assignment a) -> IO (Maybe (Assignment a))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Assignment a)
forall a. Maybe a
Nothing
                Unknown -> Maybe (Assignment a) -> IO (Maybe (Assignment a))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Assignment a)
forall a. Maybe a
Nothing

-- | Returns /true/ iff the given propositional formula is a tautology.
taut :: (Show a, Ord a) => PropositionalFormula a -> Bool
taut :: PropositionalFormula a -> Bool
taut = Bool -> Bool
not(Bool -> Bool)
-> (PropositionalFormula a -> Bool)
-> PropositionalFormula a
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.PropositionalFormula a -> Bool
forall a. (Show a, Ord a) => PropositionalFormula a -> Bool
sat(PropositionalFormula a -> Bool)
-> (PropositionalFormula a -> PropositionalFormula a)
-> PropositionalFormula a
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
PNot

{- |
Returns @Nothing@ iff the given formula is a tautology.
Otherwise, returns a counterexample (i.e., an assignment under which the given formula evaluates to /false/).
-}
tautCounterExample :: (Show a, Ord a) => PropositionalFormula a -> Maybe (Assignment a)
tautCounterExample :: PropositionalFormula a -> Maybe (Assignment a)
tautCounterExample = PropositionalFormula a -> Maybe (Assignment a)
forall a.
(Show a, Ord a) =>
PropositionalFormula a -> Maybe (Assignment a)
satAssignment(PropositionalFormula a -> Maybe (Assignment a))
-> (PropositionalFormula a -> PropositionalFormula a)
-> PropositionalFormula a
-> Maybe (Assignment a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
PNot

{- |
Returns /true/ iff the given formula is not satisfiable (i.e., there is no assignment making it true).
-}
contradicts :: (Show a, Ord a) => PropositionalFormula a -> Bool
contradicts :: PropositionalFormula a -> Bool
contradicts = Bool -> Bool
not(Bool -> Bool)
-> (PropositionalFormula a -> Bool)
-> PropositionalFormula a
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.PropositionalFormula a -> Bool
forall a. (Show a, Ord a) => PropositionalFormula a -> Bool
sat

{- |
Converts the given formula to a list of clauses (first argument).
Each clause is represented as a list of literals where literals are represented as integers.
Negative literals indicate negation of variables.
For example, the literal @-3@ translates to @PNot x@, where @x@ is the variable represented by @3@.
The mapping from integers to variables is returned as a bimap in the second argument.
-}
toIntCNF :: (Ord a) => PropositionalFormula a -> ([[Int]], Bimap a Int)
toIntCNF :: PropositionalFormula a -> ([[Int]], Bimap a Int)
toIntCNF p :: PropositionalFormula a
p = (([[Int]], Bimap a Int), Int) -> ([[Int]], Bimap a Int)
forall a b. (a, b) -> a
fst ((([[Int]], Bimap a Int), Int) -> ([[Int]], Bimap a Int))
-> (([[Int]], Bimap a Int), Int) -> ([[Int]], Bimap a Int)
forall a b. (a -> b) -> a -> b
$ (State Int ([[Int]], Bimap a Int)
 -> Int -> (([[Int]], Bimap a Int), Int))
-> Int
-> State Int ([[Int]], Bimap a Int)
-> (([[Int]], Bimap a Int), Int)
forall a b c. (a -> b -> c) -> b -> a -> c
flip State Int ([[Int]], Bimap a Int)
-> Int -> (([[Int]], Bimap a Int), Int)
forall s a. State s a -> s -> (a, s)
runState 1 (State Int ([[Int]], Bimap a Int) -> (([[Int]], Bimap a Int), Int))
-> State Int ([[Int]], Bimap a Int)
-> (([[Int]], Bimap a Int), Int)
forall a b. (a -> b) -> a -> b
$ do
    (m :: Bimap a Int
m, p' :: PropositionalFormula Int
p') <- Bimap a Int
-> PropositionalFormula a
-> State Int (Bimap a Int, PropositionalFormula Int)
forall a.
Ord a =>
Bimap a Int
-> PropositionalFormula a
-> State Int (Bimap a Int, PropositionalFormula Int)
intifyFormula Bimap a Int
forall a b. Bimap a b
empty (PropositionalFormula a
 -> State Int (Bimap a Int, PropositionalFormula Int))
-> PropositionalFormula a
-> State Int (Bimap a Int, PropositionalFormula Int)
forall a b. (a -> b) -> a -> b
$ PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
simplify PropositionalFormula a
p
    ([[Int]], Bimap a Int) -> State Int ([[Int]], Bimap a Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Int -> Int) -> (() -> Int) -> PropositionalFormula Int -> [[Int]]
forall a.
Show a =>
(a -> a) -> (() -> a) -> PropositionalFormula a -> [[a]]
clausifyCNF (\x :: Int
x -> -Int
x) (\_ -> [Char] -> Int
forall a. HasCallStack => [Char] -> a
error "Cannot construct false.") (PropositionalFormula Int -> [[Int]])
-> PropositionalFormula Int -> [[Int]]
forall a b. (a -> b) -> a -> b
$ PropositionalFormula Int -> PropositionalFormula Int
forall a. PropositionalFormula a -> PropositionalFormula a
lazyToCNF PropositionalFormula Int
p', Bimap a Int
m)

{- |
Replaces all values in a propositional formula with integers.
Returns the converted formulas as well as the mapping from values to integers.
The first argument is the initial mapping between values and integers (can be @empty@).
-}
intifyFormula :: (Ord a) => Bimap a Int -> PropositionalFormula a -> State UUID (Bimap a Int, PropositionalFormula Int)
intifyFormula :: Bimap a Int
-> PropositionalFormula a
-> State Int (Bimap a Int, PropositionalFormula Int)
intifyFormula m :: Bimap a Int
m PTrue = do
    (m' :: Bimap a Int
m', conflict :: [PropositionalFormula Int]
conflict) <- Bimap a Int -> State Int (Bimap a Int, [PropositionalFormula Int])
forall a.
Ord a =>
Bimap a Int -> State Int (Bimap a Int, [PropositionalFormula Int])
createConflictingLiterals Bimap a Int
m
    (Bimap a Int, PropositionalFormula Int)
-> State Int (Bimap a Int, PropositionalFormula Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bimap a Int
m', [PropositionalFormula Int] -> PropositionalFormula Int
forall a. [PropositionalFormula a] -> PropositionalFormula a
POr [PropositionalFormula Int]
conflict)
intifyFormula m :: Bimap a Int
m PFalse = do
    (m' :: Bimap a Int
m', conflict :: [PropositionalFormula Int]
conflict) <- Bimap a Int -> State Int (Bimap a Int, [PropositionalFormula Int])
forall a.
Ord a =>
Bimap a Int -> State Int (Bimap a Int, [PropositionalFormula Int])
createConflictingLiterals Bimap a Int
m
    (Bimap a Int, PropositionalFormula Int)
-> State Int (Bimap a Int, PropositionalFormula Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bimap a Int
m', [PropositionalFormula Int] -> PropositionalFormula Int
forall a. [PropositionalFormula a] -> PropositionalFormula a
PAnd [PropositionalFormula Int]
conflict)
intifyFormula m :: Bimap a Int
m (PVariable v :: a
v) =
    if a -> Bimap a Int -> Bool
forall a b. (Ord a, Ord b) => a -> Bimap a b -> Bool
member a
v Bimap a Int
m
    then (Bimap a Int, PropositionalFormula Int)
-> State Int (Bimap a Int, PropositionalFormula Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bimap a Int
m, Int -> PropositionalFormula Int
forall a. a -> PropositionalFormula a
PVariable (Bimap a Int
m Bimap a Int -> a -> Int
forall a b. (Ord a, Ord b) => Bimap a b -> a -> b
! a
v))
    else do
        State Int ()
next
        Int
uuidForV <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
        let intval :: Int
intval = Int -> Int
toInt Int
uuidForV in
            (Bimap a Int, PropositionalFormula Int)
-> State Int (Bimap a Int, PropositionalFormula Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Int -> Bimap a Int -> Bimap a Int
forall a b. (Ord a, Ord b) => a -> b -> Bimap a b -> Bimap a b
insert a
v Int
intval Bimap a Int
m, Int -> PropositionalFormula Int
forall a. a -> PropositionalFormula a
PVariable Int
intval)
intifyFormula m :: Bimap a Int
m (PNot p :: PropositionalFormula a
p) = do
    (m' :: Bimap a Int
m', p' :: PropositionalFormula Int
p') <- Bimap a Int
-> PropositionalFormula a
-> State Int (Bimap a Int, PropositionalFormula Int)
forall a.
Ord a =>
Bimap a Int
-> PropositionalFormula a
-> State Int (Bimap a Int, PropositionalFormula Int)
intifyFormula Bimap a Int
m PropositionalFormula a
p
    (Bimap a Int, PropositionalFormula Int)
-> State Int (Bimap a Int, PropositionalFormula Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bimap a Int
m', PropositionalFormula Int -> PropositionalFormula Int
forall a. PropositionalFormula a -> PropositionalFormula a
PNot PropositionalFormula Int
p')
intifyFormula m :: Bimap a Int
m (PAnd cs :: [PropositionalFormula a]
cs) = do
    (m' :: Bimap a Int
m', cs' :: [PropositionalFormula Int]
cs') <- Bimap a Int
-> [PropositionalFormula a]
-> State Int (Bimap a Int, [PropositionalFormula Int])
forall a.
Ord a =>
Bimap a Int
-> [PropositionalFormula a]
-> State Int (Bimap a Int, [PropositionalFormula Int])
intifyFormulas Bimap a Int
m [PropositionalFormula a]
cs
    (Bimap a Int, PropositionalFormula Int)
-> State Int (Bimap a Int, PropositionalFormula Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bimap a Int
m', [PropositionalFormula Int] -> PropositionalFormula Int
forall a. [PropositionalFormula a] -> PropositionalFormula a
PAnd [PropositionalFormula Int]
cs')
intifyFormula m :: Bimap a Int
m (POr cs :: [PropositionalFormula a]
cs) = do
    (m' :: Bimap a Int
m', cs' :: [PropositionalFormula Int]
cs') <- Bimap a Int
-> [PropositionalFormula a]
-> State Int (Bimap a Int, [PropositionalFormula Int])
forall a.
Ord a =>
Bimap a Int
-> [PropositionalFormula a]
-> State Int (Bimap a Int, [PropositionalFormula Int])
intifyFormulas Bimap a Int
m [PropositionalFormula a]
cs
    (Bimap a Int, PropositionalFormula Int)
-> State Int (Bimap a Int, PropositionalFormula Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bimap a Int
m', [PropositionalFormula Int] -> PropositionalFormula Int
forall a. [PropositionalFormula a] -> PropositionalFormula a
POr [PropositionalFormula Int]
cs')

{- |
Applies 'intifyFormula' to all given formulas
-}
intifyFormulas :: (Ord a) => Bimap a Int -> [PropositionalFormula a] -> State UUID (Bimap a Int, [PropositionalFormula Int])
-- (m, []) is the initial state of the fold. At the beginning, the map is unchanged and no formulas have been processed.
-- foldM will fill this list of formulas one step at a time while adapting the map if necessary.
intifyFormulas :: Bimap a Int
-> [PropositionalFormula a]
-> State Int (Bimap a Int, [PropositionalFormula Int])
intifyFormulas m :: Bimap a Int
m formulas :: [PropositionalFormula a]
formulas = ((Bimap a Int, [PropositionalFormula Int])
 -> PropositionalFormula a
 -> State Int (Bimap a Int, [PropositionalFormula Int]))
-> (Bimap a Int, [PropositionalFormula Int])
-> [PropositionalFormula a]
-> State Int (Bimap a Int, [PropositionalFormula Int])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Bimap a Int, [PropositionalFormula Int])
-> PropositionalFormula a
-> State Int (Bimap a Int, [PropositionalFormula Int])
forall a.
Ord a =>
(Bimap a Int, [PropositionalFormula Int])
-> PropositionalFormula a
-> State Int (Bimap a Int, [PropositionalFormula Int])
intifyFormulas_fold (Bimap a Int
m, []) ([PropositionalFormula a] -> [PropositionalFormula a]
forall a. [a] -> [a]
reverse [PropositionalFormula a]
formulas) -- reverse is just here for human readability: The output will have the same order as the input then.

{- |
The folding function for 'intifyFormulas'.
It takes the current progress of the fold @(mi, cis)@ and a formula to intify @c@:

* @mi@: The current mapping from values a to ints.
* @cis@: A list of already intified formulas
* @c@: A formula of values @a@ that has to be intified and merged into @(mi, cis)@.
-}
intifyFormulas_fold :: (Ord a) => (Bimap a Int, [PropositionalFormula Int]) -> PropositionalFormula a -> State UUID (Bimap a Int, [PropositionalFormula Int])
intifyFormulas_fold :: (Bimap a Int, [PropositionalFormula Int])
-> PropositionalFormula a
-> State Int (Bimap a Int, [PropositionalFormula Int])
intifyFormulas_fold (mi :: Bimap a Int
mi, cis :: [PropositionalFormula Int]
cis) c :: PropositionalFormula a
c = do
    (mi' :: Bimap a Int
mi', c' :: PropositionalFormula Int
c') <- Bimap a Int
-> PropositionalFormula a
-> State Int (Bimap a Int, PropositionalFormula Int)
forall a.
Ord a =>
Bimap a Int
-> PropositionalFormula a
-> State Int (Bimap a Int, PropositionalFormula Int)
intifyFormula Bimap a Int
mi PropositionalFormula a
c
    (Bimap a Int, [PropositionalFormula Int])
-> State Int (Bimap a Int, [PropositionalFormula Int])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bimap a Int
mi', [PropositionalFormula Int
c'][PropositionalFormula Int]
-> [PropositionalFormula Int] -> [PropositionalFormula Int]
forall a. [a] -> [a] -> [a]
++[PropositionalFormula Int]
cis)

{- |
Creates a list of the two literals 'x' and 'not x' where x is a new generated variable.
-}
createConflictingLiterals :: (Ord a) => Bimap a Int -> State UUID (Bimap a Int, [PropositionalFormula Int])
createConflictingLiterals :: Bimap a Int -> State Int (Bimap a Int, [PropositionalFormula Int])
createConflictingLiterals m :: Bimap a Int
m = do
    State Int ()
next
    Int
z <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
    let intval :: Int
intval = Int -> Int
toInt Int
z in
        (Bimap a Int, [PropositionalFormula Int])
-> State Int (Bimap a Int, [PropositionalFormula Int])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bimap a Int
m, [Int -> PropositionalFormula Int
forall a. a -> PropositionalFormula a
PVariable Int
intval, PropositionalFormula Int -> PropositionalFormula Int
forall a. PropositionalFormula a -> PropositionalFormula a
PNot (PropositionalFormula Int -> PropositionalFormula Int)
-> PropositionalFormula Int -> PropositionalFormula Int
forall a b. (a -> b) -> a -> b
$ Int -> PropositionalFormula Int
forall a. a -> PropositionalFormula a
PVariable Int
intval])