Convert algebraic formula to CNF Consider the following test:
$$\sum_{i=1}^n{a_ib_ic_i} \overset{?}{=} q,\tag1$$ 
where $a_i, b_i, c_i \in \{-1, 0, 1\}$ and $q \in \{0, 1\}.$ 
Is it possible to rewrite [1] to conjunctive normal form?
Any help (links/toy examples/hints on how to start) is much appreciated.
 A: As suggested by Courtois, Bard and Hulme (section 2.2), you could approach this problem in two steps:
Step 1:
Solve the equation modulo 2. Take boolean variables. The equation becomes an exclusive or and can be readily converted into a CNF using tools like bc2cnf.
Step 2:
For variables which were determined to be true/1 and thus unequal zero in step 1, find the sign. Again this is an exclusive or.

Alternative approach
If you require a solution in one step (and are prepared to deal with a far bigger CNF ...), you could model each variable as two boolean variables and translate your equation into a boolean expression as input for bc2cnf. 
Two variable encodings come to mind:
You could either encode the absolute value of the variable in one boolean and the sign in the second boolean:

As alternative, encode the variables as sums of -1 and +1:

Once you have encoded your triple-value integer variables in double-value boolean variables, you can take the logic for a full adder and a digital comparator to translate your equation into a logical circuit. The adder computes the sum and the comparator checks if the result stays between lower and upper bound.
