From: Thorsten Kiefer on
Hi,
I wrote an applet, with wich you can solve a SaT instance by hand.
It is based on multiplication, and maybe you can find a sequence of
multiplications, where the maximum number of minterms becomes minimal.

http://tokis-edv-service.de/index.php/beispiele/solving-sat-by-hand

Best Regards
Thorsten