Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Logic functions and equations : binary models for computer science (2nd ed.)
Posthoff C., Steinbach B., Springer International Publishing, New York, NY, 2019. 508 pp. Type: Book (978-3-030024-19-2)
Date Reviewed: Aug 6 2019

Logic functions, commonly known as Boolean functions, arise in many areas of computer science and information technology. On a fundamental technological level, every digital circuit can be modeled as a Boolean function. Design, optimization, and circuit synthesis can be reduced to corresponding problems on Boolean functions. On an abstract level, the semantics of every formula in propositional logic is a Boolean function.

Since many problems in the formal analysis and verification of computer programs, as well as in discrete mathematics, combinatorics, and optimization, are often solved by their reduction to the satisfiability of propositional formulas (SAT) problem, a large variety of applications rely at their core on techniques for the efficient representation and manipulation of Boolean functions.

This book represents a completely revised new edition of the authors’ previous book on logic functions [1]. Based on 40 years of research, the text discusses both the fundamental theory and a number of practical applications of the theory. A particular focus is placed on the approach of representing (the solution sets of) Boolean functions as lists of ternary vectors (vectors whose entries are the values “true,” “false,” “any”); the software system XBOOLE, developed by the authors, uses this representation to solve a variety of problems related to logic functions. However, unlike the previous edition, which was very much based on XBOOLE, this new text presents the material in a mostly system-independent way.

Part 1 presents the theoretical foundations. Chapter 1 gives (with a nice historical outline) an introduction to Boolean algebra. Chapter 2 introduces the concept of logic functions and the various possibilities of their representation and manipulation, including the ternary vector list approach favored by the authors. Chapter 3 discusses logic equations and their solution (based on ternary vectors as the main data structure); this presents an interesting alternative view on the satisfiability problem of propositional logic. Chapter 4 presents Boolean differential calculus, a core research topic of the authors, which investigates how changing the values of Boolean variables affects the solutions of logic functions. Chapter 5 discusses classes of logic functions (such as the lattices determined by partially defined functions) and the symbolic solution of functional equations and Boolean differential equations.

Part 2 presents a number of applications of the theory. Chapter 6 gives a short overview on propositional logic and binary arithmetic, the two main historical sources of Boolean functions, with applications to coding theory and cryptography. Chapter 7 discusses a variety of problems that can be reduced to SAT and demonstrates their solution via ternary vector lists and XBOOLE. Chapter 8 briefly presents the authors’ own research on a particular graph coloring problem. In contrast to this special topic, chapter 9 gives an extensive overview on modeling combinatorial circuits by logic functions, their analysis, their synthesis, and the derivation of error models for their testing. Chapter 10 extends this discussion to sequential circuits implementing finite state machines.

Via these two parts, the book presents an essentially self-contained account of the theory and applications of Boolean functions. However, due to its focus on the particular model of ternary vector lists, it does not give a comprehensive survey of the state of the field. The presented approach is today less prominent than binary decision diagrams (BDDS), which are also briefly discussed in the book. Likewise, the problem of SAT is mainly solved today by algorithms that are based on other data structures and apply conflict-driven clause learning or stochastic local search. Furthermore, the book does not address the important application of model checking, that is, the verification of finite state systems, which became effective via efficient BDD encodings of Boolean functions. Furthermore, the modern approach of bounded model checking relies on the encoding of finite execution traces as propositional formulas and the application of SAT.

All in all, the focus of the text is more on algebra than logic (whose presentation is comparatively short and has some minor quirks, for example, bounded existential quantification is expressed using logical conjunction, not implication, as claimed in the book). Thus, to get a truly complete picture of the field, the reader is advised to also consult a textbook on propositional logic and modern SAT solving.

The presented book nevertheless represents a unique and very recommendable exposition on the theory of Boolean functions and its numerous applications. The text is very well written in such a style that readers with varying backgrounds will benefit from the presented results, both theoretically and practically. Its particular approach will also give readers already familiar with propositional logic and SAT new and interesting insights.

Reviewer:  Wolfgang Schreiner Review #: CR146643 (1910-0356)
1) Posthoff, C.; Steinbach, B. Logic functions and equations: binary models for computer science. Springer, New York, NY, 2004.
Bookmark and Share
  Featured Reviewer  
 
General (F.3.0 )
 
 
General (B.6.0 )
 
Would you recommend this review?
yes
no
Other reviews under "General": Date
Mathematics in programming
Tunnicliffe W., Prentice-Hall, Inc., Upper Saddle River, NJ, 1991. Type: Book (9780135634042)
Aug 1 1992
Introduction to the theory of programming languages
Meyer B., Prentice-Hall, Inc., Upper Saddle River, NJ, 1990. Type: Book (9780134985107)
Jun 1 1991
Formal methods--mathematics, theory, recipes or what?
Cooke J. The Computer Journal 35(5): 419-423, 1992. Type: Article
Nov 1 1993
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy