For those who want more information, the full source code for the predicate generation is collected in this Haskell file. The source code for the simplifier is in this WEB file.
The program produces one or two web pages as output depending on whether you select Simplify output or not.
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
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
(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
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
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
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,
and2is defined as the usual operation on booleans:
and2 (Bool x, Bool y) = return (Bool (x && y))In the symbolic interpretation,
and2instead 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 vThis 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.
The initial output has many trivial features, including unit clauses. The simplifier applies rules to simplify the predicate without changing the set of solutions. The simplifier has fixed size limits, so it may not work for large problems. (It can handle a maximum of 15,000 variables and 63,000 clauses.)
The simplifier repeatedly applies the following rules to the CNF predicate: