I understand what using a SAT-solver implies, but I haven't noticed apt failing often in practical terms. The heuristics used seem to work fine for me.