Implication graph

Implication graph

Synchronous Sequential Circuits

Published in Sajjan G. Shiva, Introduction to Logic Design, 2018

To summarize the implication graph construction process, we start with an arbitrary state pair and include a new node into the implication graph, depending on the transitions of the first pair under each input combination. We continue with this process with the new nodes until no new nodes are generated. Transitions to single states are not shown on the implication graph. Note that the implication graph provides essentially the same information as an implication chart, but in a graphical form.

A novel structure-exploiting encoding for SAT-based diagnosis

View Article

Journal Information

Published in Journal of Experimental & Theoretical Artificial Intelligence, 2022

Sajjad Ahmed Siddiqi

The solver also has to keep track of the reasons for assignments to build an implication graph (Zhang et al., 2001) to be used for learning conflicts so that the conflicts are not repeated (described later). In an implication graph nodes represent assignments to variables. There is a directed edge from a node to if the assignment at node was in part directly responsible for the assignment at node . Thus implication graph depicts the Boolean propagation process. For example, following the above Boolean propagation for an AND gate, if an input of the AND gate was assigned a value of due to the AND gate itself being then the direct cause of assignment to the said input are the assignment of to the AND gate together with the assignments of to all the rest of the gate’s inputs. Note that a decision node and a node representing an assignment at decision level have no incoming edge.

Explore chapters and articles related to this topic

Synchronous Sequential Circuits

A novel structure-exploiting encoding for SAT-based diagnosis