There are a lot of different "focused" sequent calculi for lots of different logics, but my understanding is that many or most of them have the following flavor. First one divides the connectives into "left-asynchronous / positive" (e.g. $\vee$, $\oplus$, $\otimes$, $\exists$), whose left rules are invertible, and "right-asynchronous / negative" (e.g. $\wedge$, $\Rightarrow$, $\multimap$, $\forall$), whose right rules are invertible. Then the focused proof search (i.e. building a sequent calculus proof bottom-up) has two phases. First we apply all the asynchronous/invertible rules, in any order. Second, we focus on some formula and apply all of its synchronous rules, keeping focus on the formulas thereby generated and immediately applying any applicable asynchronous rules (or, equivalently, reverting to phase one in all generated subgoals), until we reach an atomic formula. At that point we can either finish the proof with an identity rule, or re-focus on a different formula.
At least some systems require the proof to finish as soon as the focus formula becomes atomic, which I believe means that if you chose the wrong formula to focus on in the first place you may have to backtrack. My question is rather about what happens if we allow the proof to re-focus on a different formula when it reaches an atomic one. In that case, is it possible to "choose the wrong formula" to focus on and have to backtrack? In other words, is it ever possible that there are synchronous formulas that must not be decomposed in a proof, or that must be decomposed in a particular order?
It's easy to come up with examples where you can get in trouble if you try to apply synchronous rules before asynchronous ones, e.g. $p\vee q \vdash q\vee p$. But the focused method requires all asynchronous rules to happen immediately, so this sort of problem doesn't arise.
Note also that there is another unrelated source of backtracking that this says nothing about, involved in individual synchronous rules. For instance, there are two $\& L$ rules that we have to choose between, and in a rule like $\otimes R$ we have to decide how to split the context between the two premises, and it's certainly always possible to make wrong choices there and have to backtrack. That's not what I'm asking about.
I've phrased this as a general question about all focused sequent calculi, but of course it's possible that the answer depends on the logic or on the details of the calculus. In that case I would be interested to know what properties of a logic or calculus lead to different behavior.