A generate-and-test approach for computing "optimal" plans in SAT-based planning