A Boolean Encoding of Arithmetic Operations

• Autorzy: Zbrzezny A.

Warianty tytułu

PL

Kodowanie Boolowskie operacji arytmetycznych

• Języki publikacji: EN

Abstrakty

EN

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.

PL

W pracy przedstawiamy algorytmy realizujące Boolowskie kodowanie czterech podstawowych operacji arytmetycznych: dodawania, odejmowania, mnożenia i dzielenia. Liczby całkowite są kodowane w systemie uzupełnieniowym do 2 jako wektory formuł Boolowskich a operacje arytmetyczne są zakodowane jako operacje na wektorach formuł Boolowskich. Dodatkowo przedstawiamy algorytmy realizujące Boolowskie kodowanie dla operacji obliczania całkowitego pierwiastka kwadratowego oraz dla operacji potęgowania.

Słowa kluczowe

EN

Boolean encoding; bounded model checking; digital circuit; SAT solver; timed automaton; vector of Boolean formulas

PL

kodowanie Boolowskie; ograniczona weryfikacja modelowa; układ cyfrowy; SAT tester; automat czasowy; wektor formuł Boolowskich

• Wydawca: Instytut Podstaw Informatyki PAN
• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2007
• Tom: Nr 999
• Strony: 1--35
• Opis fizyczny: Bibliogr. 7 poz.

Twórcy

autor

Zbrzezny A.

• Instytut Matematyki i Informatyki Akademia im. Jana Długosza w Częstochowie al. Armii Krajowej 13/15 42-200 Częstochowa Polska,

Bibliografia

• [1] A. Aiken, S. Bugrara, I. Dillig, T. Dillig, B. Hackett, and P. Hawkins. The saturn program analysis system. Computer science technical report, Stanford University, 2006.
• [2] P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Półrola, M. Szreter, B. Woźna, and A. Zbrzezny. Verics: A tool for verifying Timed Automata and Estelle specifications. In Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), volume 2619 of LNCS, pages 278-283. Springer-Verlag, 2003.
• [3] D. Goldberg. Computer Architecture: A Quantitative Approach, chapter Computer Arithmetic. In , Hennessy and Patterson [4], third edition, 2003. ISBN 1-55860-596-7.
• [4] J. L. Hennessy and D. A. Patterson. Computer Architecture: A Quantitative Approach. Morgan-Kaufman, third edition, 2003. ISBN 1-55860-596-7.
• [5] A. Janowska and P. Janowski. Slicing of timed automata with discrete data. In L. Czaja, editor, Proc. ofthe Int. Workshop on Concurrency, Specification and Programming (CS&P'05), volume l, pages 211-222. Warsaw University, 2005.
• [6] Y. Xie and A. Aiken. Saturn: A sat-based tool for bug detection. In Proceedings o f the 15th International Conference on Computer Aided Verification (CAV 2005), LNCS 3576, pages 139-143. Springer-Verlag, Berlin, 2005. ISBN 978-3-540-27231-1.
• [7] A. Zbrzezny and A. Półrola. Sat-based reachability checking for timed automata with discrete data. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'06), volume 206(1) of Informatik-Berichte, pages 207-218. Humboldt University, 2006.