The web page for the output predicate begins with a lot of comments. If you are interested, you can use these comments to determine the meaning of each variable in the predicate, and you can discard them if you are not interested. Some of the variables give the bits of the product. Those variables will appear in unit clauses that force them to take on the appropriate value so that they represent the number you input. Some of the variables give the bits of the first factor. Some of the variables give the bits of the second factor. The remaining variables give the values on the wires in the multiplication circuit that is simulated by the predicate. All of the details should be clear from reading the comments. Likewise the details of how the circuit is wired together should be clear.
To ensure that no factors are found for prime numbers, the circuit
requires, for n-bit inputs, that the first factor
have no more than (n-1) bits and that the second
factor has no more than n/2 (rounded up) bits.
The two basic types of multiplication circuits that are implemented are:
For the two basic types of multipliers, the circuit begins by forming all the products ai * bj where ai is a digit from the first number factor and bj is a digit from the second factor. These products are then added, but each multiplier circuit differs in the details of how they carry out the addition.
In the carry-save circuit, row i of the
circuit adds the product from row i
(ai * b*) with the sum and carry (shifted
one column) to obtain a new sum and a new carry. A special adder is
used to add the final sum and final carry. The products from the
first row must go through a linear number of adders to get to the
special adder.
In the Wallace-tree circuit, the rows (with appropriate shifts) are added in groups of three to produce sums and carries. The sums and carries (with appropriate shifts) are again added in groups of three, and this is repeated until there is just one sum and one carry. Then a special adder is used to add the final sum and the final carry. The products from any row need go through only a logarithmic number of adders before they get to the special adder.
The adder type specifies the special adder. The
n-bit adder uses the algorithm (adapted to binary
numbers) taught in grade school. It is simple, but carries must
propagate through a linear number of addition stages.
The fast adder is a log-time adder taken from
Foundations of Computer Science by Aho and Ullman. If you select
Fast for adder type and Wallace for multiplier type, then no
path in the circuit has length longer than a small constant times the number
of bits needed to specify the input integer. It is an interesting
experimental question as to whether such SAT problems are easier.
The predicate generation is written using a Haskell program (inspired by the Lava library). The idea is that one writes completely standard executable specifications for the circuits, and then exploits Haskell type classes to get a non-standard interpretation of the primitives which generates CNF clauses. For example, a half-adder is specified as follows:
halfAdd :: Circuit m => (Bit,Bit) -> m (Bit,Bit)
halfAdd (a,b) =
do carryOut <- and2 (a,b)
sum <- xor2 (a,b)
return (carryOut,sum)
In the standard interpretation, and2 is defined as the
usual operation on booleans:
and2 (Bool x, Bool y) = return (Bool (x && y))In the symbolic interpretation,
and2 instead generates
CNF clauses relating its input variables to its output variables:
and2 (b1, b2) =
do v <- newBitVar
let or1 = Or [b1, b2, notBit v]
or2 = Or [b1, notBit b2, notBit v]
or3 = Or [notBit b1, b2, notBit v]
or4 = Or [notBit b1, notBit b2, v]
addDesc [or1,or2,or3,or4]
return v
This approach to generating the predicates is appealing as it enables
us to use the full power of Haskell to write circuits naturally, test
the circuits extensively using the standard interpretation, and then
simply turn a switch on to use the symbolic interpretation.