Fifth assignment for IB016, semester spring 2019.

Effective Transformation of a Logical Formula to Conjunctive Normal Form

In this homework you work will be to implement an effective tranformation of a propositional logic formula to Conjunctive Normal Form (CNF). You probably know from the basic logic course that for every propositional formula there is an equivalent formula in CNF. The problem with the basic transformation is that there can be an exponential blowup, i.e. the size of the resulting formula can be exponential compared to the size of the original formula. This is very impractical for example for SAT solvers (which are algorithms which aim at checking if a formula is satisfiable and try to be efficient for large classes of propositional formulas): these solvers usually require input formula to be in CNF and their runtime can be up to exponential in the size of the input formula. Therefore a SAT solver with naive conversion to CNF would have double exponential blowup.

There is another approach to conversion to CNF: we can create a formula in CNF which is satisfiable if and only if original formula was satisfiable (i.e. is equisatisfiable) and which has only a linear overhead. The trick is to use auxiliary variables in the transformation to represent subformulas of the original formula. This transformation is called Tseytin transformation and is described for example on Wikipedia: https://en.wikipedia.org/wiki/Tseytin_transformation. We do not require that you use Tseytin transformation in particular, however, your transformation must guarantee that the size of the resulting formula is linear with respect to the size of the original formula.

Your goal will be to implement functions eval and getVariables for boolean formulas represented by a tree data type, as well as those represented by CNF (which is basically a list of lists of literals). Furthermore, you will be required to implement toCNF which converts a tree-represented formula to CNF. Finally there is a small helper function eval' which you should also implement. Your implementation should use monad transformers, see later. There are some tests prepared for you, feel free to write your own tests on top of these.

Monad Transformers

In implementing the required functionality you are strongly advised to use monad transformers.

• eval: this function operates within MonadReader and MonadError and therefore you must use their functionality in the implementation.
• getVariables in the version for FormulaTree: think about a good use of MonadWriter / Writer in this function. You are strongly advised to use it (and it will be required to get full points).
• toCNF: think about which monads/monad transformers will be useful for this task. There are several aspects of the conversion to CNF which map well to different monads/transformers shown in the class. You will still get some points if you don't use any of them, but your work will probably be harder then if you choose your monads well.

Tips & Tricks

• Think before implementing. Especially about monads and transformers shown on the 10th & 11th lecture.
• Have a look at the mtl package.
• Use ghcid (or an IDE with similar functionality) for type checking & testing: ghcid -c 'ghci -Wall' -T testAll HW05.hs -- this will re-compile your solution every time you change it, and show you either compilation errors/warnings or test results. Ghcid can be installed either from your distribution's package if you have it, or from cabal.
• Use typed holes when you don't know the type of an subexpression which you need to write.
• Don't forget to use hlint & check compilation on aisa/ghc 8.6.

Notes on Used Language Extensions

There are several language extensions enabled in this homework. If you want to enable some more, please ask in discussion forum.

• FlexibleContexts -- this allows usage of concrete types (with kind *) as parts of the context (e.g. in MonadReader Valuation m Valuation cannot be used without this extension).
• InstanceSigs -- allows you to specify explicitly a type of a function in an instance definition.

• ScopedTypeVariables -- this, together with ExplicitForAll which it implies, allows you to use type variables from the functions' type in its nested functions, e.g.:

  foo :: forall m a. Monad m => (a -> m a) -> m [a]
  foo = ...
    where
      bar :: a -> m a
      bar = ...
  

  Here m and a in definition of bar represent the same type as in foo (while normally, this would define a polymorphic bar and therefore m would not need to be a monad).

• TemplateHaskell is used for generation of testAll function.
• GeneralizedNewtypeDeriving allows us to lift any instance available on some type to newtypes over this type (see e.g. CNF, Clause).

Modules and packages

You can use any module from packages base, containers, and mtl (which includes transformers). If you wish so, you can also use Unicode syntax from unicode-prelude.