Exploiting Macro-actions and Predicting Plan Length in Planning as Satisfiability