There's something seriously messed up with these algorithms. Take as input: a -> a According to 'dpll: better' this is unsatisfiable. (It isn't; it's a ta

There's something seriously messed up with these algorithms. Take as input: a -> a According to 'dpll: better' this is unsatisfiable. (It isn't; it's a tautology.) The algorithm 'dpll: naive' does not succeed either. The rest of the algorithms fail to observe it as a tautology and instead look for a specific input which makes it correct (generally 'a'). That's not necessarily a bad thing but it was somewhat unexpected (as when it gives you the solution you're probably tempted to think it's "the" solution and not just "a" solution) -- the easiest workaround is to look for the unsatisfiability of ~(a -> a). Using this here is a counterexample to 'dpll: better' showing just how bad it is: ~((a -> b) -> (((a -> b) -> c) -> c)) "Clause set is true if we assign values to variables as: a b c". (This is the negation of another tautology, saying that if we have access to a value of type x and a function from x -> y then we have access to a value of type y. The only complication is that x is a function from a -> b and y is labeled c.) A famous tautology which is not available to type theory is Pierce's law, ((p -> q) -> p) -> p 'dpll: better' also says that this is unsatisfiable, but also that its negation is unsatisfiable.