how to encode circuits in 0 1 integer programs, a sketch

0-1 program for circuits.txt

how to use integer programming to encode circuits:

Given a circuit C with n boolean inputs, and assume without loss of
generality  that every logic operation is unary or binary. Label each
binary or unary expression c_1 .... c_m. Let r_0 be the distinguished
clause that is the result of this boolean circuit (because an n bit
output  is just a product of circuits that have 1 bit outputs.).   

For a given c_i, it is of the form c_i = one of 
      1) = not a, which we can define via the constraint  c_i - a= 0
      2) = a xor b, define via   not a -b + not b - a+ c_i = 1 because   
      	   not a -b + not b - a = 0 always
	   and so this one needs to generate new clause variables  for the nots.

	  *and* & *or*  can then be encoded in a straightforward fashion with these.