I'm hoping a real expert comes by to give a better answer, but these are things I've thought about a bit. Here are some thoughts:
(1) You should separate notions of computability (is there an algorithm?) and complexity (will the algorithm terminate in my lifetime?) Hilbert's 10th problem is a question about computability. Questions about SAT, solving equations over finite fields, or basically any computation in algebraic geometry over an algebraically closed field, such as computing betti numbers and Frobenius eigenvalues1, are all computable; the question is how complex they are.
(2) Given an instance of SAT, impose not only the various binary equations you are thinking of, but also the equations $x_i^2=x_i$ for all $i$. Now all of the solutions over $\mathbb{F}^{alg}_2$ live in $\mathbb{F}_2$. So, expanding the size of your problem linearly, you can make there be no difference between working in the boolean field and in its algebraic closure.
This transformation suggests that sophisticated notions like cohomology and Frobenius action will not be useful for the general question of counting solutions to equations over $\mathbb{F}_2$. If your family of equations over $\mathbb{F}_2$ contains the relations $x_i^2 = x_i$ then the solutions are just finitely many points all defined over the ground field, so all cohomology is trivial other than $H^0$ and the Frob action is trivial. So, for at least some equations over $\mathbb{F}_2$, the geometry doesn't give you any tools other than going back to solving the SAT problem.
I would very much like to see someone define and study the notion of which problems are "ALGEBRAIC GEOMETRY-HARD". Ravi's work on Murphy's law (and the people who have followed him) have this flavor, but they don't actually talk about computational complexity.
(4) Your motivation may be in the opposite direction. That is to say, you may be hoping to start with a SAT problem and create equations over $\mathbb{F}_2$ for which the high power tools do help you. I can't prove this is impossible, but I'm skeptical.
That said, there is some work which points against my skepticism. Jesus De Loera and his collaborators (start here and, if you are interested, continue by reading all the papers on algebraic optimization here) have been taking standard hard instances of NP-complete graph theory problems, encoding them as algebraic geometry problems and beating pure graph theoretic algorithms. The results are entirely experimental, but the experimental data makes this method look surprisingly good.
Harm Derksen has tried a similar approach for Graph Isomorphism. He can prove that his methods at worst only polynomially worse than the classic Weisfeiler-Lehman algorithm and, for the Cai-Furer-Immerman graphs, his methods are exponentially better.
One interesting feature of these papers is that they discard Groebner basis methods in favor of brute force. For example, to test whether $g_1$, $g_2$, ..., $g_n$ generate the unit ideal, rather than using Groebner bases, De Loera et al simply guess an upper bound for the degree of polynomials $f_i$ obeying $\sum f_i g_i =1$ and solve this as a family of linear equations in the coefficients of the $f_i$.
(5) There is a general principle, whose precise statement I don't know, that the difficulty of computing with a projective variety $X$ is controlled by its Castelnuovo-Mumford regularity. Googling on "Castelnuovo Mumford regularity complexity" turns up lots of references where one could start digging, though I didn't find a statement simple enough to quote.
My understanding (but I am not an expert) is that varieties created by encoding combinatorial problems in algebraic geometry tend to have very high CM regularity.
1 Frobenius eigenvalues can be described as the eigenvalues of geometric Frob acting on a variety over $\mathbb{F}^{alg}_p$, so you can define them without talking about varieties over nonaglebraically closed fields, although you'll certainly miss some of the motivation.