Sequential logic can be minimised in terms of states used by repacking the state encoding. Two sequential designs are said to be a bi-simulations pair when they have the same external observable behaviour, but may be implemented differently internally. There is much research into algorithms that find a maximal bi-simulation of a single design, which is a partitioning of its state into blocks where there is no observable difference between being in one state or another in that block. Sequential models can be simplified by representing all states within a block as a single flip-flop encoding and removing or ignoring the unreachable states in the input design.
Once the flip-flop encoding is settled, we are faced with the combinatorial logic minimisation problem. Logic minimisation in itself is an extensive subject. The algorithms required to generate efficient circuits in the presence of timespecs are mature and proprietary, although several textbooks exist.
If we consider `straightforward' minimisation of total gate count, then there are several classes of algorithm available, depending on the run time available and how many outputs come from the logic block.
Logic minimisation can be solved with exhaustive search for small numbers of input variables (less then ten) or by Karnough maps by humans. A general principle of logic minimisation is the expansion of cubes to cover adjacent dont-cares, as done by humans with Karnough maps. A cube is a conjunction (ANDing) of one or more input variables or their negations. The more variables included in a cube the fewer input combinations it is true for, so cubes which expand as much as possible take fewest gates.
The Espresso algorithm [http://oak.ece.ul.ie/~colin/ce4518/espresso.html] from Berkely is widely used iterative algorithm for logic minimisation, based on repeated expansion and contraction of cubes and keeping the expansions which are broadest (minimal gates). It gives a good enough result in most cases.
For multiple outputs, the (PD) Putnam and Davis algorithm can be used, but it is rather simple. This expands all of the output expressions into sum-of-products terms and looks at the resulting terms, which are <em> implicants}. An implicant is a cube which, if true, means that the output must also be true. There are two simple rules for minimisation with implicants which the PD process uses. They are: two implicants which are different in only the negation of one variable (e.g. $ACD$ and $A\overline{C}D$) can be replaced with a single one without that variable (i.e. $AD$), and two implicants which are the same as each other except that one has an additional literal can be replaced with just the shorter one (e.g. $ABC$ and $AB$ can be replaced with just $AB$);
Unfortunately, there are no simple rules for many of the other identities of Boolean logic which allow minimisation, although one could use apply a finite table of known identities to get a bit further. An example problem (from the carry output of a full adder) is $AB + C(\overline{A}B + A\overline{B})$, which cannot be simplified with everyday rules to $AB + AC + CB$.
The PD algorithm works by looking at all of the implicants and selecting the ones to be used (implemented in gates) based on their usefulness. Clearly any implicant which is disjoint from all the others is needed. Implicants which are used by a high number of output expressions are then selected for implementation, since the output from the implicant gate will be used several times at the OR stage. Finally, implicants which are needed but have no special merit are chosen. At each stage, several options may be available, so the whole algorithm can be run iteratively with alternate decisions being forced, and the best result selected.
The Putnam and Davis algorithm tends to generate two-level logic trees, which are often not ideal, since the high fan-in gates needed have actually to be made from multiple smaller gates.\footnote{ Here the term 'two-level' denotes the depth of logic gates in a maximal chain rather than the number of voltage levels on a net. Sum-of-products form counts as two-level logic assuming inverted and un-inverted versions of all the literals are available.} Indeed, the initial expressions or HDL which the logic specification came from may contain a degree of useful structure which could best be preserved, but which instead is lost in the conversion to sum-of-products form.
Algorithms which iterate to improve on multi-level logic structures (i.e. as opposed to sum-of-products, two-level structures) are research areas. One algorithm, called Transduction, that a student of mine implemented from a paper had a run time of order $n^5$ and so was completely useless on real designs.