add DPLL.hs as main solver and export Formule module

    also add some examples in cnf/
    main fct reads a formula in dimacs format and prints if it is SAT
remove