SAT-based planning in complex domains: Concurrency, constraints and nondeterminism