Skip to content

Latest commit

 

History

History
13 lines (13 loc) · 647 Bytes

README.md

File metadata and controls

13 lines (13 loc) · 647 Bytes

SATsolver

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)

Compilation

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

How to use

Run executable, then provide formula as first line input.