SAT and Arithmetic Geometry This is an agglomeration of several questions, linked by a single observation: SAT is equivalent to determining the existence of roots for a system of polynomial equations over $\mathbb{F}_2$ (note though that the system is represented in non-trivial manner). The reason it is OK to consider more than one equation is because the conjunction of the conditions $f_i(x_1 ... x_n) = 0$ is equivalent to the single condition $\prod_i (f_i(x_1 ... x_n) + 1) + 1 = 0$.


*

*This reminds of the solution of Hilbert's 10th problem, namely that it is undecidable whether a system of polynomial equations over $\mathbb{Z}$ has roots. Is there a formal relation? Can we use the undecidability over $\mathbb{Z}$ to provide clues why the problem is hard over $\mathbb{F}_2$ (that is, $P \ne NP$)? What is known about decidability and complexity for other rings? In particular, what is known about complexity over $\mathbb{F}_p$ for p prime > 2?

*The system of polynomial equations defines an algebraic scheme. Is it possible to find algebro-geometric conditions on this scheme, s.t. something can be told about the complexity of SAT restricted to such schemes?

*The solutions of our system of polynomial equations are the fixed points of the Frobenius endomorphism on the corresponding variety over $\bar{\mathbb{F}}_2$. There is a variant of Lefschetz's fixed-point theorem which relates the existence of such points to $l$-adic cohomology. Can this be used to provide some insight on P vs. NP?
 A: As for the first question, solvability of a system of polynomial equations is NP-complete over every finite field, and NP-hard for every integral domain. The reduction was already mentioned in David Speyers’s answer: add $x_i^2-x_i$ to your system for every variable $x_i$.
The exact complexity of solvability over infinite domains is not so easy to answer. To begin with, it may significantly depend on the representation of the polynomial and its coefficients.


*

*Solvability over $\mathbb Z$ is undecidable ($\Sigma^0_1$-complete). This is the MRDP theorem. The decidability of solvability over $\mathbb Q$ is an open problem.

*Solvability of polynomials with rational coefficients over $\mathbb R$ or $\mathbb C$ is in PSPACE, and it is not known whether one can do better. Assuming the generalized Riemann hypothesis, solvability of rational polynomials over $\mathbb C$ is in AM, and therefore in the second level of the polynomial hierarchy. Note that AM = NP under some plausible assumptions from circuit complexity.

*Solvability over the algebraic closure of a finite field is also decidable, though I do not know offhand what are the complexity bounds (but it should be again something in the vicinity of EXP or PSPACE). The keyword is “effective Nullstellensatz”.
A: I'm going to address just one aspect of your question, which has been restated in some of the answers and comments, about whether there is any formal connection between undecidability and computational complexity.
This is certainly a very tempting idea, and you could argue that one of the main reasons to conjecture that the polynomial hierarchy does not collapse (this is a standard generalization of the conjecture that P≠NP) is that the infinitary analogue of the polynomial hierarchy, namely the arithmetical hierarchy, is known not to collapse.  Of course we know, for example from the Baker–Gill–Solovay theorem, that we can't naively carry over all intuitions from computability theory over to complexity theory, but the analogy remains in the back of the minds of many people working in this subject.
Perhaps closer to your question are two papers by Michael Freedman, Limit, logic, and computation and K-SAT on groups and undecidability.  The latter paper in particular notes that 2-SAT is polytime solvable and 3-SAT is NP-complete, and constructs infinitary analogues of these two problems that are respectively decidable and undecidable.  Your observation about the analogy between the MRDP theorem and the hardness of solving systems of equations over $\mathbb{F}_2$ could be thought of as being in the same vein.  Unfortunately, while intriguing, so far these analogies don't seem to have yielded any significant insights into the P≠NP problem.
A: More unexpected to me is the reduction from SAT to linear system over
$\mathbb{N}_0$ (including $0$).
Monotone one in three SAT
 is NP-complete and is a conjunction of clauses, each clause is three boolean
 variables $(x,y,z)$. To satisfy a clause exactly one variable must be true.
The reduction to linear system over $\mathbb{N}_0$ is for each clause add the
 linear equation $x + y + z = 1$.
Solving the resulting system over $\mathbb{Z}$ is easy, but over $\mathbb{N}_0$ is
 NP-complete.
A: David mentioned in his answer results where Groebner bases are not used. However, Groebner bases for polynomial systems aren't the best available tools theoretically, either. E.g. the best theoretical results for complexity of solving 0-dimensional systems follow a route of symbolically deforming the system into one for which the Groebner basis is trivial to find, and then using Stickelberger Lemma to find roots of the deformed system, and finally taking the limit. Details of this are described e.g. in this book.
Groebner bases (in characteristic 0) are also usually beaten by the machinery of semidefinite programming relaxations. Perhaps not coincidentally, a lot of recent work in computational complexity (in particular, approximation algorithms) uses semidefinite programming relaxations, too.
There is also a line of research where the complexity is investigated w.r.t. arithmetic  operations in $\mathbb{C}$ (or $\mathbb{R}$) having unit cost. 
A: 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.
A: Which field you work over is not important for encoding SAT, because as pointed out by David Speyer, you can put in the equation $x^2=x$ to make $x$ take on only the values $0,1$.  You can encode $x\wedge y$ by $xy$ and $x\vee y$ by $x+y-xy$.  So determining if a system has a solution is at least NP-hard.  My understanding from surveying the computer science literature some time back is that over $\mathbb C$, it is known that determining if a system has a solution is in PSPACE unconditionally and is in a complexity class called AM, which is just above NP, if one assumes the generalized Riemann Hypothesis.  See Pascal Koiran,  Hilbert's Nullstellensatz is in the polynomial hierarchy.  J. Complexity 12 (1996), no. 4, 273–286.  I don't know if the results have been improved since.  This was the most recent I had found.
A: I wanted to add one point that has not been raised yet regarding the second point in the question (are there algebro-geometric conditions on the scheme defined by the starting equations such that something can be said about the difficulty of SAT on such instances). Namely:
A wide range of complexity of SAT instances appear already among those that are unsatisfiable. In this case, the scheme is empty, so it has no geometry to speak of.
When this is the case, it can be shown even without adding in equations of the form $x_i^2=x_i$, the scheme is still empty (essentially, because the equations you started with came from the translation of a Boolean formula into polynomials - this is by now standard in the proof complexity literature; you can see a proof e.g. in Pitassi '96 Theorem 1 or in our joint paper Lemma 4.2, and surely other places as well).
I have a couple thoughts on how to deal with this, which I think also may be interesting for the OQ, but have not been able to get them to go anywhere yet (and would welcome anyone who wants to discuss it!).

*

*If you started with many Boolean clauses (/polynomials), it can still be interesting to ask about the geometry of the schemes corresponding to the satisfiable subsets of the clauses.

*Rather than thinking of the system of equations $f_1(x_1, \dotsc, x_n), \dotsc, f_m(\vec{x})$ and the scheme they define (which, as I said, may be empty, thus lacking any meaningful geometry to speak of), one can think of the equations as defining a polynomial map $\mathbb{F}^n \to \mathbb{F}^m$, sending a point $\vec{x}$ to the point $\vec{f}(\vec{x})$. This map is always nontrivial, and the equations are satisfiable iff $0$ is in its image. The image of this map, of course, always has some geometry to it, and I think it is potentially quite interesting to think about whether some geometric properties of this image tell you something about the complexity of the corresponding SAT instance. Here is one geometric fact that Toni Pitassi and I proved (Proposition B.6 here): when the $f_i$ come from the standard algebraic translation of a Boolean cnf formula, 0 is in the image iff 0 is in the Zariski closure of the image. That is, in this case, the image of this map cannot come infinitesimally close to 0 without actually containing 0, or in terms of the equations, the $f_i$ cannot be "infinitesimally close" to being satisfiable without actually being satisfiable. (The proof is somewhat specific to the point 0, that is, the image is not in general closed.)

