Boolean Functions

Context and Motivation

Although not always visible to the naked eye, Boolean Functions can be found and/or used about everywhere in computer science, but also in other fields such as physics, biology, chemistry, and so on. Two different exemplifications of the need for the efficient representation and manipulation of Boolean Functions are given below.

Hardware Synthesis and Verification

Nowadays, most critical systems rely on digital circuits, including safety-critical systems (from the ABS of a car to anti-collision systems in aircraft and control systems in power plants), mission-critical systems (navigational system for rockets or planetary rovers, supercomputer operation…) and security-critical systems (such as data centers or communication satellites). Moreover, important questions also arise about the minimization of cost and energy consumption while still ensuring optimal performance.

In order to efficiently optimize digital circuits, we usually rely on complex programs. However, these programs are rarely proven themselves, thus, they may introduce errors and produce a circuit which does not meet its specification. An obvious solution would be to prove optimizing programs; however, two major issues arise: first, these programs are complex, so that proving them would be very expensive; second, they might be proprietary, so that one cannot check that the proof is correct.

A simpler alternative is to design a program that is able to check that two circuits are equivalent. As a result, one could compare the expected behavior of the system with the actual behavior of the digital circuit supposed to implement it. Then, the only piece of software left to be proven is the “equivalence checker” itself.

Parametric Graph/Automaton Manipulation

Although a graph is, generally speaking, nothing but a collection of objects called vertices linked together by arcs .¹

There exist many types of graphs (directed or undirected, acyclical, labeled, with multi-edges, and so on), each one with its own flavors and specificities.

Many graph algorithms exist, from the most widely known ones to the most obscure ones, that can either extract useful properties (depth, width, reachability, bridges, Strongly Connected Components…) or solve problems modeled with graphs (traveling salesman problem, maximum flow, coloring problems…).

However, when one gets interested in applying them to graphs with billions of vertices (and even more arcs), he/she faces the issue that modern computers can hardly deal with such graphs using classical explicit representations. One way of dealing with such instances is to use implicit representations. Such issues arose in model checking, and the use of Binary Decision Diagrams allowed to drastically increase performances and handle instances that used to be inaccessible to computation.

We encountered similar issues when dealing with the structural analysis of parametric (or multimode) systems of equations (e.g., IsamDAE). This particular application required to deal with parametrized structured weighted graphs, that were efficiently dealt with by encoding the existence conditions of their vertices and arcs as Boolean Functions of the parameter variables, or mode variables. As for the weights of the arcs, that are natural numbers parametrized by the mode variables, their binary representations could also be encoded using Boolean Functions.

Symbolic Manipulation

The work on the BoReAl project revolves around the efficient symbolic representation (and manipulation) of complex objects that would be otherwise too big to be represented explicitly. Such task is performed by dynamically exploiting various levels of structure within the problems we intend to solve. Here is a list of our main projects.

Lambda Decision Diagram

Lambda Decision Diagrams (λDD) is a generic framework extending the notion of Binary Decision Diagrams by labeling the arcs with functional transforms. More concise and meaningful representations of the underlying Boolean Functions can then be built and manipulated.

Reduced Block Triangular Form

Reduced Block Triangular Form (RBTF) refers to two aspects of our works:

• an intermediary representation for conjunctive forms, that is, systems of equations that can be expressed as the intersection of several constraints;
• its algorithmic counterpart, allowing to efficiently turn a given equation system into this intermediary representation while preserving the initial structure.

RBTF has been independently implemented into the Snowflake package as a Generic Symbolic Dynamic Programming framework.

Snowflake is an implementation of the RBTF (Reduced Block Triangular Form) algorithm in OCaml as a functor. We provide several instantiations of this functor using Arlen Cox’ MLBDD package, allowing to compute SAT or ARGMAX (using parametric natural numbers).

1. If arcs are undirected, we prefer the terms of nodes and edges instead of vertices and arcs, respectively. ↩

Participants

Khalil Ghorbal, Joan Thibault (PhD).