Wyniki wyszukiwania - BazTech

1

From arithmetic expressions to propositional formulae

Stępień L., Stępień M. R.

Scientific Issues of Jan Długosz University in Częstochowa. Mathematics

|

2016

|

Vol. 21

135--143

EN

In papers [3], [4], [5] Authors presented a new method of solving some kinds of computational tasks in the area of linear algebra by applying SAT-solver as the highly optimized algorithms for solving the problem of propositional satisfiability. On input SAT-solver (cf. [1], [2]) takes a propositional formula in the clause form. In this paper we show in detail how any arithmetical expression can be translated into propositional formula in the CNF form skipping out its traditional form. For this, we define the notion of consistency of arithmetic and boolean valuations.

2

The Solution of SAT Problems Using Ternary Vectors and Parallel Processing

Posthoff C., Steinbach B.

International Journal of Electronics and Telecommunications

|

2011

|

Vol. 57, No. 3

233-249

EN

This paper will show a new approach to the solution of SAT-problems. It has been based on the isomorphism between the Boolean algebras of finite sets and the Boolean algebras of logic functions depending on a finite number of binary variables. Ternary vectors are the main data structure representing sets of Boolean vectors. The respective set operations (mainly the complement and the intersection) can be executed in a bit-parallel way (64 bits at present), but additionally also on different processors working in parallel. Even a hierarchy of processors, a small set of processor cores of a single CPU, and the huge number of cores of the GPU has been taken into consideration. There is no need for any search algorithms. The approach always finds all solutions of the problem without consideration of special cases (such us no solution, one solution, all solutions). It also allows to include problem-relevant knowledge into the problem-solving process at an early point of time. Very often it is possible to use ternary vectors directly for the modeling of a problem. Some examples are used to illustrate the efficiency of this approach (Sudoku, Queen's problems on the chessboard, node bases in graphs, graph-coloring problems, Hamiltonian and Eulerian paths etc.).

3

Zastosowanie technik algebraicznych w kryptoanalizie różnicowej na przykadzie szyfru blokowego DES

Gąsecki A., Misztal M.

Biuletyn Wojskowej Akademii Technicznej

|

2011

|

Vol. 60, nr 3

379-390

PL

Artykuł omawia nowy sposób ataku na szyfr blokowy DES. Zaprezentowany pomysł polega na połączeniu dwóch znanych metod kryptoanalizy, tj. kryptoanalizy różnicowej oraz ataku algebraicznego. W artykule scharakteryzowano budowę algorytmu, elementy wykorzystanych ataków oraz sposób ich połączenia. Przedstawione zostały także otrzymane wyniki oraz omówiono efekty w porównaniu z zaprezentowanymi metodami kryptoanalizy stosowanymi oddzielnie.

EN

Article describes a new method of cryptanalysis of block cipher DES. Presented idea combines two, already known techniques, namely differential crypt-analysis and algebraic attacks. The article covers a description of the block cipher DES, used elements of attacks and the way of their combination. Then, comes the presentation of the results and comparison with already known techniques of cryptanalysis, but used separately.

4

A Boolean Encoding of Arithmetic Operations

Zbrzezny A.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

|

2007

|

Nr 999

1-35

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.

5

Comparing BDD and SAT based techniques for model checking Chaum's Dining Cryptographers Protocol

Kacprzak M., Lomuscio A., Niewiadomski A., Penczek W., Raimondi F., Szreter M.

Fundamenta Informaticae

|

2006

|

Vol. 72, nr 1-3

215-234

EN

We analyse different versions of the Dining Cryptographers protocol by means of automatic verification via model checking. Specifically we model the protocol in terms of a network of communicating automata and verify that the protocol meets the anonymity requirements specified. Two different model checking techniques (ordered binary decision diagrams and SAT-based bounded model checking) are evaluated and compared to verify the protocols.