This paper introduces a highly competitive contingent planner, that uses the novel idea of encoding belief states as disjunctive normal form formulae (To et al. 2009), for the search for solutions in the belief state space. In (To et al. 2009), a complete transition function for computing successor belief states in the presence of incomplete information has been defined. This work extends the function to handle non-deterministic and sensing actions in the AND/OR forward search paradigm for contingent planning solutions. The function allows one, under reasonable assumptions, to compute successor belief states efficiently, i.e., in polynomial time. The paper also presents a novel variant of an AND/OR search algorithm, called PrAO (Pruning AND/OR search), which allows the planner to significantly prune the search space; furthermore, by the time a solution is found, the remaining search graph is also the solution tree for the contingent planing problem. The strength of these techniques is confirmed by the empirical results obtained from a large set of benchmarks available in the literature.