Reasoning and experimenting within Zadeh's fuzzy propositional logic

We present several decision algorithms within the fuzzy propositional logic based on Zadeh's implication operator p -> q = max{1-p, q}, deciding both the fuzzy SAT problem as well as the best truth value bound problem, i.e. compute the best truth value bounds of a proposition with respect to a theory. Further, we evaluate all the algorithms by adapting and extending the well know methods for evaluating SAT decision algorithms. We show that both problems present the typical easy-hard-easy pattern.