Having an efficient algorithm for SAT (or any NP complete problem) immediately gives you an efficient algorithm for ALL problems in NP, including ECDLP.
NP-hard does not mean NP, it means a problem that is ATLEAST as hard as NP. NP-hard problems that are in NP are known as NP-Complete.
Finally ECDLP itself is not a decision problem, so even if the decision problem for ECDLP is in NP and P = NP, that does not mean that ECDLP itself has a polynomial time solution.
NP, NP-Complete, NP-Hard etc... only refer to decision problems, not to general purpose computations.
{ (Curve_spec, P, x) : x is a prefix of the discrete log of point P on the specified elliptic curve }
With that said, even if the decision problem for ECDLP is in NP and P = NP, that does not mean that a solution to ECDLP is in P.
If you can solve that problem in P-time then you can also solve the functional version (find an x for which F(x) = 1) in P-time simply by setting each bit to a value for which the decision problem is satisfiable, one by one.
No, it's not. All instances of DLP, including ECDLP, are just asking for an x such that b^x = a, as Wikpedia will tell you [1]. They only differ in the choice of group, but exponentiation within the group is assumed to be an efficient operation.
> With that said, even if the decision problem for ECDLP is in NP, that does not mean that a solution to ECDLP is in P.
It trivially does. You simply start with an empty prefix x and extend it 1 bit at a time by repeatedly asking if (Curve_spec, P, x0) is in the language. If so you continue with x0, if not you continue with x1.