LogicMin Module
This module implements algorithms for logic minimization
Functions and values
Function or value | Description |
Computes a KV diagram for a given list of atoms. The KV diagram is given as two arrays (col,row) where col and row denote the column and row vectors, respectively, i.e., col[i] and row[j] denote the assignments to the variables in entry (i,j) of the KV diagram, and their union is therefore the assignment to be evaluated there.
|
|
|
|
Convert a cube (idx,(pos,neg)) as used in the Quine table to a string. The index set idx is written as a set of integers {i1,...,iN} and the cube (pos,neg) itself is written as a bitvector with * whenever there is a don't care.
|
|
|
The following function computes minimal DNFs for a given formula phi with a care set care, where the ordering of atoms atomL is respected. The function applies first the Quine method QuineTable to compute all cubes (implicants) of care->phi, and extracts then the prime cubes with function QuineTablePrimeImplicants where each prime cube is associated with a new boolean variable PI[i]. After this, it generates a formula coverPhi in CNF over the variables PI[i] such that coverPhi has a disjunct for each model of care&phi and that contains all PI[i] that cover that model. The formula coverPhi is then converted to DNF (in sets of sets representation) so that minimal DNFs for phi wrt. care can be derived. The function finally returns a tuple (qt,primeCubes,coverPhi,dnfCover,minDNFs) with:
|
Compute the Quine table: The function expects a formula phi and its variable order order atomL. It computes the Quine table that contains all implicants of phi as a list of list of lists [I0;...;In] where each Ik is the list of list of implicants of order k, i.e., where k variables are don't cares, hence, I0 are all full models of phi. Each Ik=[Lk0;...;Lkj] is partitioned into levels Lki according to the number of atoms made true (zero in Lk0 up to j in Lkj]. Each Lki is finally a list of cubes, where a cube (idx,(pos,neg)) is given by the sets of atoms (pos,neg) made true and false by the cube, respectively. The index idx is a set of integers that uniquely represents the cube; it is the union of binary numbers that an be derived when all don't cares are replaced by either true and false (following the order atomL). |
|
Get the prime implicants of a formula phi from its Quine table: We check whether the index set of a cube is contained in one of the other cube's index set of the next level. If so, it is not a prime implicant, since it has been used to construct that higher cube. The function returns a list of tuples (piv,(idx,(pos,neg))) where piv is a boolean variable generated for the prime implicant (idx,(pos,neg)). |