Skip to main content
main-content

Über dieses Buch

This book describes recent findings in the domain of Boolean logic and Boolean algebra, covering application domains in circuit and system design, but also basic research in mathematics and theoretical computer science. Content includes invited chapters and a selection of the best papers presented at the 13th annual International Workshop on Boolean Problems.

Provides a single-source reference to the state-of-the-art research in the field of logic synthesis and Boolean techniques;Includes a selection of the best papers presented at the 13th annual International Workshop on Boolean Problems;Covers Boolean algebras, Boolean logic, Boolean modeling, Combinatorial Search, Boolean and bitwise arithmetic, Software and tools for the solution of Boolean problems, Applications of Boolean logic and algebras, Applications to real-world problems, Boolean constraint solving, and Extensions of Boolean logic.

Inhaltsverzeichnis

Frontmatter

Chapter 1. Self-explaining Digital Systems: Technical View, Implementation Aspects, and Completeness

Abstract
Today’s systems are increasingly complex, often adaptable, and even autonomous. This makes designing, connecting, diagnosing, and using such systems difficult. Often this difficulty is due to a lack in understanding why a system acts as it does, i.e., why the system executes certain actions.
We propose to extend systems such that they can explain their actions to users and designers. We formalize this as self-explanation. For digital systems we discuss an approach for implementing and verifying our notion of self-explanation. A self-explaining robot controller serves as proof-of-concept.
Görschwin Fey, Rolf Drechsler

Chapter 2. Secure Implementation of Lattice-Based Encryption Schemes

Abstract
With the call for new cryptographic standards that resist powerful quantum computers, lattice-based cryptography has gained significant popularity. To become viable replacements for contemporary cryptography, lattice-based encryption and key-exchange schemes based on the hardness of the ring-LWE problem still need to address the issues with today’s adversary models in real-world security applications. In this chapter we discuss the Boolean techniques and conversion challenges for the protection of ring-LWE encryption against active attacks (i.e., adaptive chosen-ciphertext attacks) and equipped with countermeasures against side-channel analysis. Our solution is based on a post-quantum variant of the Fujisaki–Okamoto (FO) transform combined with provably secure, first-order masking. We show that CCA2-secured ring-LWE-based encryption can be achieved with reasonable performance on constrained devices but also stresses that the required transformation and handling of decryption errors implies an additional performance overhead that has not been considered so far.
Tobias Oder, Tobias Schneider, Tim Güneysu

Chapter 3. Derivative Operations for Classes of Boolean Functions

Abstract
Derivative operations of the Boolean differential calculus are very useful for many applications, like the test of digital circuits, the synthesis using the bi-decomposition of Boolean functions, the specification of Boolean functions with regard to certain properties, etc. Basically, a derivative operation can be executed for a single Boolean function. Here we extend the known theory such that each of the ten derivative operations can be applied to classes \(\mathcal {C}_N\) of Boolean functions without the need to compute the derivative operation for each Boolean function of the class separately.
Bernd Steinbach, Christian Posthoff

Chapter 4. Towards the Structure of a Class of Permutation Matrices Associated with Bent Functions

Abstract
Bent functions, that are useful in cryptographic applications, can be characterized in different ways. A recently formulated characterization is in terms of the Gibbs dyadic derivative. This characterization can be interpreted through permutation matrices associated with bent functions by this differential operator. We point out that these permutation matrices express some characteristic block structure and discuss a possible determination of it as a set of rules that should be satisfied by the corresponding submatrices. We believe that a further study of this structure can bring interesting results providing a deeper insight into features of bent functions.
Radomir S. Stanković, Milena Stanković, Jaakko T. Astola, Claudio Moraga

Chapter 5. Improving SAT Solving Using Monte Carlo Tree Search-Based Clause Learning

Abstract
Most modern state-of-the-art Boolean Satisfiability (SAT) solvers are based on the Davis–Putnam–Logemann–Loveland algorithm and exploit techniques like unit propagation and Conflict-Driven Clause Learning (CDCL). Even though this approach proved to be successful in practice, the success of the Monte Carlo Tree Search (MCTS) algorithm in other domains led to research in using it to solve SAT problems. A recent approach extended the attempt to solve SAT using an MCTS-based algorithm by adding CDCL. We further analyzed the behavior of that approach by using visualizations of the produced search trees and based on the analysis introduced multiple heuristics improving different aspects of the quality of the learned clauses. While the resulting solver can be used to solve SAT on its own, the real strength lies in the learned clauses. By using the MCTS solver as a preprocessor, the learned clauses can be used to improve the performance of existing SAT solvers.
Oliver Keszocze, Kenneth Schmitz, Jens Schloeter, Rolf Drechsler

Chapter 6. Synthesis of Majority Expressions Through Primitive Function Manipulation

Abstract
Due to technology advancements and circuits miniaturization, the study of logic systems that can be applied to nanotechnology has been progressing steadily. Among the creation of nanoelectronic circuits the reversible and majority logic stand out. This paper proposes the MPC (Majority Primitives Combination) algorithm, used for majority logic synthesis. The algorithm receives a truth table as input and returns a majority function that covers the same set of minterms. The formulation of a valid output function is made with the combination of previously optimized functions. As cost criteria the algorithm searches for a function with the least number of levels, followed by the least number of gates, inverters, and gate inputs. In this paper it’s also presented a comparison between the MPC and the exact_mig, currently considered the best algorithm for majority synthesis. The exact_mig encodes the exact synthesis of majority functions using the number of levels and gates as cost criteria. The MPC considers two additional cost criteria, the number of inverters and the number of gate inputs, with the goal to further improve exact_mig results. Therefore, the MPC aims to synthesize functions with the same amount of levels and gates, but with less inverters and gate inputs. Tests have shown that both algorithms return optimal solutions for all functions with 3 input variables. For functions with 4 inputs, the MPC is able to further improve 66% functions and achieves equal results for 11%. For functions with 5 input variables, out of a sample of 1000 randomly generated functions, the MPC further improved 48% functions and achieved equal results for 11%.
Evandro C. Ferraz, Jeferson de Lima Muniz, Alexandre C. R. da Silva, Gerhard W. Dueck

Chapter 7. Literal Selection in Switching Lattice Design

Abstract
Switching lattices are two-dimensional arrays of four-terminal switches proposed in a seminal paper by Akers in 1972 to implement Boolean functions. Recently, with the advent of a variety of emerging nanoscale technologies based on regular arrays of switches, synthesis methods targeting lattices of multi-terminal switches have found a renewed interest. In this paper we discuss two different combinatorial problems related to the assignment of input literals to switches in a lattice when multiple choices are possible at some switch. We propose and develop efficient heuristic algorithms for both problems and discuss the implication of the different solutions on the layout of switching lattices. Experimental results on a set of known benchmarks confirm the effectiveness of the proposed heuristics.
Anna Bernasconi, Fabrizio Luccio, Linda Pagli, Davide Rucci

Chapter 8. Exact Synthesis of ESOP Forms

Abstract
We present an exact synthesis approach for computing Exclusive-or Sum-of-Products (ESOP) forms with a minimum number of product terms using Boolean satisfiability. Our approach finds one or more ESOP forms for a given Boolean function. The approach can deal with incompletely specified Boolean functions defined over many Boolean variables and is particularly fast if the Boolean function can be expressed with only a few product terms. We describe the formalization of the ESOP synthesis problem with a fixed number of terms as a decision problem and present search procedures for determining ESOP forms of minimum size. We further discuss how the search procedures can be relaxed to find ESOP forms of small sizes in reasonable time. We experimentally evaluate the performance of the SAT-based synthesis procedures on completely and incompletely specified Boolean functions.
Heinz Riener, Rüdiger Ehlers, Bruno de O. Schmitt, Giovanni De Micheli

Chapter 9. An Algorithm for Linear, Affine and Spectral Classification of Boolean Functions

Abstract
The spectral representation and classification of Boolean functions have been previously studied and found to be useful in logic design and testing. Spectral techniques also have potential application for reversible and quantum circuits. This paper considers the partitioning of Boolean functions into linear, affine and spectral equivalence classes. A single efficient recursive classification algorithm is presented. It can be used to determine all equivalence classes for small n, and to determine if two functions fall in the same equivalence class for larger n. For two functions in the same equivalence class, the algorithm identifies a sequence of translations to map one to the other.
D. Michael Miller, Mathias Soeken

Chapter 10. New Results on Reversible Boolean Functions Having Component Functions with Specified Properties

Abstract
In the traditional logic synthesis different classifications of non-reversible Boolean functions have found many applications. Recently, some attempts to deal with classifications of reversible functions have been published. In this paper, solutions of two problems which have not been addressed yet are presented. The solutions were found by extrapolation of cycle structures for 3-and 4-variable reversible functions obtained in the course of enumerative computations.
Paweł Kerntopf, Krzysztof Podlaski, Claudio Moraga, Radomir Stanković

Chapter 11. Efficient Hardware Operations for the Residue Number System by Boolean Minimization

Abstract
Residue number systems (RNS) represent numbers by their remainders modulo a set of relatively prime numbers. This paper proposes an efficient hardware implementation of modular multiplication and of the modulo function (X(mod P)), based on Boolean minimization. We report experiments showing a performance advantage up to 30 times for our approach vs. the results obtained by state-of-the-art industrial tools.
Danila Gorodecky, Tiziano Villa

Backmatter

Weitere Informationen