propositional solver