Is there an equivalent concept of a "variety" for SAT? Couldn't find anything via google - I was wondering what work is out there looking at SAT problems from the perspective akin to an algebraic variety, e.g. a set of variables $X_1=$true, $X_2=$false, .., $X_k=$true, etc define a set of propositions which are all satisfed by that particular set of values in much the same way that a variety defines a set of polynomials that all happen to vanish at the same points.
Thanks.
 A: First, let me address the dual question (which is easier): visualizing a SAT instance as a variety. 
There is a natural way of representing any instance of SAT as a variety in $(\mathbb{Z}/2\mathbb{Z})^n$ (where $n$ is the number of variables). This is because we can interpret the two-element Boolean algebra $(2, \vee, \wedge, \neg)$ in the two-element ring $(\mathbb{Z}/2\mathbb{Z}, +, \times)$:


*

*"$a\wedge b$" is shorthand for "$a\times b$".

*"$a\vee b$" is shorthand for "$a+b+ab$".

*"$\neg a$" is shorthand for "$1-a$" (that is, the element of the ring $\mathbb{Z}/2\mathbb{Z}$ which when added to $a$ equals $1$). Note that $1-a=1+a$ in this context.
So, for instance, to the SAT-instance $$(a\vee b)\wedge (\neg a)$$ we associate the polynomial $$(a+b+ab)(1-a)=a+b+ab+a+ab+ab=b+ab.$$ Finding a solution to the SAT-instance corresponds to finding a point where this polynomial equals 1 (not zero), that is, to finding a zero for the polynomial $$1+b+ab.$$ It's easily checked that the only zero of this polynomial is $b=1$, $a=0$, which agrees with the SAT-instance.
See https://en.wikipedia.org/wiki/Boolean_ring.

OK, now onto the question you ask. 
The problem is that in order to even begin to think of something as a variety, we have to think of that thing as a subset of $R^n$ for some ring $R$ and some number $n$. The problem is, the set of SAT instances does not form a ring in any obvious way (let alone the set of ordered pairs from a ring).
This can be fixed: equivalence classes of SAT instances can be thought of as a ring. Specifically, identify $\varphi$ and $\psi$ if their solution sets are the same. The result is a Boolean algebra, which can be turned into a Boolean ring (see above). Now to each valuation of the $k$-many propositional variables (we fix $k$ ahead of time), we can associate a subset of this ring, and this subset is indeed a variety. But this is kind of ugly; in particular, the equivalence class construction requires us to solve SAT!
Based on this, I would tentatively say that there is no "natural" and computationally efficient way to view the set of SAT instances which are solved by a fixed valuation as a variety.
A: For one variety over one finite field, the algebraic geometry translation of a SAT problem is not all that useful.  Switching between the two descriptions is computationally trivial. Algebraic geometry doesn't help with finding solutions so much as describing relations between solutions. SAT problems do not lead to structured varieties like elliptic curves or algebraic surfaces where algebraic geometry comes into its own.
The advantage of geometry is when there are many varieties, or many fields and rings in which to solve the equations, or both. 
This is roughly the idea of Aaronson and Wigderson's paper on Algebraization as a barrier to $P \neq NP$ proofs.  General arguments about computation with bits, thought of as facts about polynomials or varieties where we look for solutions mod $2$, also would work over finite fields with more than $2$ elements, or more general rings than that. In those more general settings they can arrange oracles for which $P = NP$, so things are not that easy.
Geometric Complexity Theory proposed by Mulmuley is an application of algebraic geometry to complexity and an approach to the $P=NP$ problem, but the geometry does not come from mapping SAT problems to algebraic equations mod $2$.  The idea is to look for algebraic problems in invariant theory and group representation theory that are close enough analogues of $P=NP$ that solving the algebra problems would have implications for computational complexity theory.  Algebraic geometry appears in GCT because it is a tool for the algebra problems that appear.
