- 5 Jul 2014: Fixed a bug for inputs less than 5.
- 23 Nov 2007: Fixed a bug that caused the generator to occasionally output clauses with boolean constants instead of variables.
- 1 Jan 2006: The old CGI servers has been replaced by a new one running a different OS. The code for the simplification has not been recompiled for the new system yet and hence the simplification of the output does not work now.
- 10 Feb 2005: Fixed a bug in the simplifier that caused it to sometimes drop some clauses.

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
requires, for ** n**-bit inputs, that the first factor
have no more than

`(n-1)`

`n/2`

The two basic types of multiplication circuits that are implemented are:

- the carry-save multiplier, and
- the Wallace-tree multiplier (IEEE Trans. on Electronic Comp., 1964).

For the two basic types of multipliers, the circuit begins by
forming all the products **a _{i} * b_{j}** where

In the carry-save circuit, row ** i** of the
circuit adds the product from row

`i`

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

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 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:

- Remove subsumed clauses. (If the literals in clause A are a subset of those in clause B, then remove clause B.)
- Do resolutions where at least one parent is subsumed. (If clause
A is
**x l**and clause B is_{1}... l_{n}**-x l**then replace clause B with_{1}... l_{n}y_{1}... y_{n}**l**._{1}... l_{n}y_{1}... y_{n} - Substitute for equalities. (If clause A is
**l**and clause B is_{1}-l_{2}**-l**, then replace all occurrences of_{1}l_{2}**l**with_{2}**l**except in clauses A and B.)_{1}

- ATPG template class library (Library for Combitional/Sequential logic simulation, and fault simulation functionality (semi-PROOFS)).

sabry@cs.indiana.edu