HSE, Discrete Mathematics for Algorithm and Software Design
Given a Boolean formula in 2-CNF, use the resolution method to determine whether it is satisfiable. Clauses of the 2-CNF can be of one of the two forms: α \/ β or α -> β, where α and β are literals (p or ~p, where p is a variable). The CNF is presented in the usual notation, for example: (p -> q) /\ (~r \/ s) /\ (~q -> p)