Haskell app that verifies satisfiability of given formula. Formula can be made up of single character named variables, and "implies", "or", "not", "and" operators. For example:
(not p) and (p or not q)
All operators are assumed to be right associative, meaning p and q implies r
is equivalent to p and (q implies r)
Run ghc Sat.hs
in the project directory.
Data.List.Split module is required, to download it, run cabal install --lib --package-env . split
in the project directory
Run executable, then provide formula as first line input.