What kind of Diophantine equations are these? Assume that the $a$'s in the following equations must be limited to a binary values of $\{0,1\}$ and the $c$'s are integer constants: 
\begin{align}
                      2a_{34}a_{23}a_{24}  &= c_1\\
                 a_{23} + a_{24} + a_{34}  &= c_2\\
                     2 a_{34}a_{13}a_{14}  &= c_3\\
                 a_{13} + a_{14} + a_{34}  &= c_4\\
                     2 a_{24}a_{12}a_{14}  &= c_5\\
                 a_{12} + a_{14} + a_{24}  &= c_6
\end{align}
I recognize that these are highly restricted form of Diophantine equations, but I've been unable to find what they are called (once I know their names I can lookup proofs on any properties they have). If they don't have a specific name, how could one show that a] a solution exists, b] it is unique c] if not unique, how many solutions there are?
My CS background forces to acknowledge that I could enumerate through all $2^6$ possibilities, but I don't think I'd understand what is going if I did that. Also, I'd like to know how this would scale when there are more then 6 free variables.
 A: I don't think that this kind of restriction occurs in diophantine equations to begin with, so I doubt they carry a special name.
There are a lot of very simple observations that you can make, though: since each $a$ can only take the value $0$ or $1$, then the only possible values of $c_1$, $c_3$, and $c_5$ are $0$ or $2$; and $c_2$, $c_4$, and $c_6$ just tell you how many of the $a$s are equal to $1$ and how many are equal to $0$, so the only possible values are $0$, $1$, $2$, or $3$. In particular, $c_1 = 2$ if and only if $c_2=3$; and similarly with $c_3$ and $c_4$, and with $c_5$ and $c_6$. Your variables are divided into three non-disjoint subsets: $\{a_{23}, a_{24}, a_{34}\}$, $\{a_{13}, a_{14}, a_{34}\}$, and $\{a_{12}, a_{14}, a_{24}\}$; any two of the sets have exactly one element in common, and the triple intersection is trivial. Since you will know how many in each set are equal to $1$ and how many are equal to $0$, it will be easy to determine any solutions using these facts.
You can also delete the $2$s from the first, third, and fifth equation (suitably modifying $c_1$, $c_3$, and $c_5$ if necessary), and reduce $c_2$, $c_4$, and $c_6$ modulo $2$ so that you have a system of equations over $\mathbb{F}_2$, the field with two elements; solve it over that field and then check which (if any) of the solutions still works over $\mathbb{Z}$ (which is just a matter of whether $c_2$, $c_4$, and $c_6$ were originally $2$ instead of $0$, or $3$ instead of $1$). 
A: I think this could easily be translated into a boolean problem. We will interpret $x=0$ with $x$ is false and $x=1$ with $x$ is true. Now Consider quoations of the form 
$a+b+c=z$
where $z$ is an integer and $a, b, c \in \{0,1\}$. 
Now z gives you the amount of variables that you can set to "true". So we can observe because of the interval of $a,b,c$ that $z \in [0,3]$ it will give you basically 4 cases. 
If $z=0$ you get the equoation $a = 0 \land b = 0 \land c = 0$, as all variables are $0$ and therefore "false". 
If $z=1$, exactly one variable is "true", so you have multiple cases here, you get the equoations 
$(a = 1 \land b = 0 \land c = 0) \lor (a = 0 \land b = 1 \land c = 0) \lor (a = 0 \land b = 0 \land c = 1)$
If $z=2$ you get
$(a = 1 \land b = 1 \land c = 0) \lor (a = 1 \land b = 0 \land c = 1) \lor (a = 0 \land b = 1 \land 
  c = 1)$
If $z=3$ you get
$a = 1 \land b = 1 \land c = 1$
The $2abc=y$ equations are quite simple, you will either have $y = 0$ or $y = 1$. If you get $y = 0$ the equivalent logical equation is
$a = 0 \lor b = 0 \lor c = 0$
As at least one of the variables is 0 in that case.
Else if $y = 1$ you have
$a = 1 \land b = 1 \land c = 1$ as all variables are "true" in this case.
Now you are left with a boolean "SAT"-Problem ( http://en.wikipedia.org/wiki/Boolean_satisfiability_problem ) where many algorithms exist that are clever and will work for a huge number of quoations although the problem is NP-complete. 
