|
Andrzej Zbrzezny
A Boolean Encoding of Arithmetic Operations
999
Abstract
In this paper we present algorithms for a~Boolean encoding of four basic
arithmetic operations on integer numbers: addition, subtraction, multiplication
and division. Integer numbers are encoded in two's complement system as vectors
of Boolean formulas and arithmetic operations are faithfully encoded as
operations on vectors of Boolean formulas. In addition, we also provide an
algorithm for a Boolean encoding of the operations of calculating integer
square root and an algorithm for a Boolean encoding of the operation of
exponentiation with nonnegative integer exponent.
Keywords: Boolean encoding, bounded model checking, digital circuit, SAT
solver, timed automaton, vector of Boolean formulas.
|
|
 |
 |
