%!PS-Adobe-2.0 %%Creator: dvips(k) 5.86 Copyright 1999 Radical Eye Software %%Title: dddmp-2.0.dvi %%Pages: 10 %%PageOrder: Ascend %%BoundingBox: 0 0 596 842 %%DocumentFonts: Times-Bold Times-Roman Courier Times-Italic Helvetica %%DocumentPaperSizes: a4 %%EndComments %DVIPSWebPage: (www.radicaleye.com) %DVIPSCommandLine: dvips -t a4 -f dddmp-2.0 %DVIPSParameters: dpi=600, compressed %DVIPSSource: TeX output 2002.12.11:0557 %%BeginProcSet: texc.pro %! /TeXDict 300 dict def TeXDict begin/N{def}def/B{bind def}N/S{exch}N/X{S N}B/A{dup}B/TR{translate}N/isls false N/vsize 11 72 mul N/hsize 8.5 72 mul N/landplus90{false}def/@rigin{isls{[0 landplus90{1 -1}{-1 1}ifelse 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale isls{ landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div hsize mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul TR[ matrix currentmatrix{A A round sub abs 0.00001 lt{round}if}forall round exch round exch]setmatrix}N/@landscape{/isls true N}B/@manualfeed{ statusdict/manualfeed true put}B/@copies{/#copies X}B/FMat[1 0 0 -1 0 0] N/FBB[0 0 0 0]N/nn 0 N/IEn 0 N/ctr 0 N/df-tail{/nn 8 dict N nn begin /FontType 3 N/FontMatrix fntrx N/FontBBox FBB N string/base X array /BitMaps X/BuildChar{CharBuilder}N/Encoding IEn N end A{/foo setfont}2 array copy cvx N load 0 nn put/ctr 0 N[}B/sf 0 N/df{/sf 1 N/fntrx FMat N df-tail}B/dfs{div/sf X/fntrx[sf 0 0 sf neg 0 0]N df-tail}B/E{pop nn A definefont setfont}B/Cw{Cd A length 5 sub get}B/Ch{Cd A length 4 sub get }B/Cx{128 Cd A length 3 sub get sub}B/Cy{Cd A length 2 sub get 127 sub} B/Cdx{Cd A length 1 sub get}B/Ci{Cd A type/stringtype ne{ctr get/ctr ctr 1 add N}if}B/id 0 N/rw 0 N/rc 0 N/gp 0 N/cp 0 N/G 0 N/CharBuilder{save 3 1 roll S A/base get 2 index get S/BitMaps get S get/Cd X pop/ctr 0 N Cdx 0 Cx Cy Ch sub Cx Cw add Cy setcachedevice Cw Ch true[1 0 0 -1 -.1 Cx sub Cy .1 sub]/id Ci N/rw Cw 7 add 8 idiv string N/rc 0 N/gp 0 N/cp 0 N{ rc 0 ne{rc 1 sub/rc X rw}{G}ifelse}imagemask restore}B/G{{id gp get/gp gp 1 add N A 18 mod S 18 idiv pl S get exec}loop}B/adv{cp add/cp X}B /chg{rw cp id gp 4 index getinterval putinterval A gp add/gp X adv}B/nd{ /cp 0 N rw exit}B/lsh{rw cp 2 copy get A 0 eq{pop 1}{A 255 eq{pop 254}{ A A add 255 and S 1 and or}ifelse}ifelse put 1 adv}B/rsh{rw cp 2 copy get A 0 eq{pop 128}{A 255 eq{pop 127}{A 2 idiv S 128 and or}ifelse} ifelse put 1 adv}B/clr{rw cp 2 index string putinterval adv}B/set{rw cp fillstr 0 4 index getinterval putinterval adv}B/fillstr 18 string 0 1 17 {2 copy 255 put pop}for N/pl[{adv 1 chg}{adv 1 chg nd}{1 add chg}{1 add chg nd}{adv lsh}{adv lsh nd}{adv rsh}{adv rsh nd}{1 add adv}{/rc X nd}{ 1 add set}{1 add clr}{adv 2 chg}{adv 2 chg nd}{pop nd}]A{bind pop} forall N/D{/cc X A type/stringtype ne{]}if nn/base get cc ctr put nn /BitMaps get S ctr S sf 1 ne{A A length 1 sub A 2 index S get sf div put }if put/ctr ctr 1 add N}B/I{cc 1 add D}B/bop{userdict/bop-hook known{ bop-hook}if/SI save N @rigin 0 0 moveto/V matrix currentmatrix A 1 get A mul exch 0 get A mul add .99 lt{/QV}{/RV}ifelse load def pop pop}N/eop{ SI restore userdict/eop-hook known{eop-hook}if showpage}N/@start{ userdict/start-hook known{start-hook}if pop/VResolution X/Resolution X 1000 div/DVImag X/IEn 256 array N 2 string 0 1 255{IEn S A 360 add 36 4 index cvrs cvn put}for pop 65781.76 div/vsize X 65781.76 div/hsize X}N /p{show}N/RMat[1 0 0 -1 0 0]N/BDot 260 string N/Rx 0 N/Ry 0 N/V{}B/RV/v{ /Ry X/Rx X V}B statusdict begin/product where{pop false[(Display)(NeXT) (LaserWriter 16/600)]{A length product length le{A length product exch 0 exch getinterval eq{pop true exit}if}{pop}ifelse}forall}{false}ifelse end{{gsave TR -.1 .1 TR 1 1 scale Rx Ry false RMat{BDot}imagemask grestore}}{{gsave TR -.1 .1 TR Rx Ry scale 1 1 false RMat{BDot} imagemask grestore}}ifelse B/QV{gsave newpath transform round exch round exch itransform moveto Rx 0 rlineto 0 Ry neg rlineto Rx neg 0 rlineto fill grestore}B/a{moveto}B/delta 0 N/tail{A/delta X 0 rmoveto}B/M{S p delta add tail}B/b{S p tail}B/c{-4 M}B/d{-3 M}B/e{-2 M}B/f{-1 M}B/g{0 M} B/h{1 M}B/i{2 M}B/j{3 M}B/k{4 M}B/w{0 rmoveto}B/l{p -4 w}B/m{p -3 w}B/n{ p -2 w}B/o{p -1 w}B/q{p 1 w}B/r{p 2 w}B/s{p 3 w}B/t{p 4 w}B/x{0 S rmoveto}B/y{3 2 roll p a}B/bos{/SS save N}B/eos{SS restore}B end %%EndProcSet %%BeginProcSet: 8r.enc % @@psencodingfile@{ % author = "S. Rahtz, P. MacKay, Alan Jeffrey, B. Horn, K. Berry", % version = "0.6", % date = "22 June 1996", % filename = "8r.enc", % email = "kb@@mail.tug.org", % address = "135 Center Hill Rd. // Plymouth, MA 02360", % codetable = "ISO/ASCII", % checksum = "119 662 4424", % docstring = "Encoding for TrueType or Type 1 fonts to be used with TeX." % @} % % Idea is to have all the characters normally included in Type 1 fonts % available for typesetting. This is effectively the characters in Adobe % Standard Encoding + ISO Latin 1 + extra characters from Lucida. % % Character code assignments were made as follows: % % (1) the Windows ANSI characters are almost all in their Windows ANSI % positions, because some Windows users cannot easily reencode the % fonts, and it makes no difference on other systems. The only Windows % ANSI characters not available are those that make no sense for % typesetting -- rubout (127 decimal), nobreakspace (160), softhyphen % (173). quotesingle and grave are moved just because it's such an % irritation not having them in TeX positions. % % (2) Remaining characters are assigned arbitrarily to the lower part % of the range, avoiding 0, 10 and 13 in case we meet dumb software. % % (3) Y&Y Lucida Bright includes some extra text characters; in the % hopes that other PostScript fonts, perhaps created for public % consumption, will include them, they are included starting at 0x12. % % (4) Remaining positions left undefined are for use in (hopefully) % upward-compatible revisions, if someday more characters are generally % available. % % (5) hyphen appears twice for compatibility with both ASCII and Windows. % /TeXBase1Encoding [ % 0x00 (encoded characters from Adobe Standard not in Windows 3.1) /.notdef /dotaccent /fi /fl /fraction /hungarumlaut /Lslash /lslash /ogonek /ring /.notdef /breve /minus /.notdef % These are the only two remaining unencoded characters, so may as % well include them. /Zcaron /zcaron % 0x10 /caron /dotlessi % (unusual TeX characters available in, e.g., Lucida Bright) /dotlessj /ff /ffi /ffl /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef /.notdef % very contentious; it's so painful not having quoteleft and quoteright % at 96 and 145 that we move the things normally found there down to here. /grave /quotesingle % 0x20 (ASCII begins) /space /exclam /quotedbl /numbersign /dollar /percent /ampersand /quoteright /parenleft /parenright /asterisk /plus /comma /hyphen /period /slash % 0x30 /zero /one /two /three /four /five /six /seven /eight /nine /colon /semicolon /less /equal /greater /question % 0x40 /at /A /B /C /D /E /F /G /H /I /J /K /L /M /N /O % 0x50 /P /Q /R /S /T /U /V /W /X /Y /Z /bracketleft /backslash /bracketright /asciicircum /underscore % 0x60 /quoteleft /a /b /c /d /e /f /g /h /i /j /k /l /m /n /o % 0x70 /p /q /r /s /t /u /v /w /x /y /z /braceleft /bar /braceright /asciitilde /.notdef % rubout; ASCII ends % 0x80 /.notdef /.notdef /quotesinglbase /florin /quotedblbase /ellipsis /dagger /daggerdbl /circumflex /perthousand /Scaron /guilsinglleft /OE /.notdef /.notdef /.notdef % 0x90 /.notdef /.notdef /.notdef /quotedblleft /quotedblright /bullet /endash /emdash /tilde /trademark /scaron /guilsinglright /oe /.notdef /.notdef /Ydieresis % 0xA0 /.notdef % nobreakspace /exclamdown /cent /sterling /currency /yen /brokenbar /section /dieresis /copyright /ordfeminine /guillemotleft /logicalnot /hyphen % Y&Y (also at 45); Windows' softhyphen /registered /macron % 0xD0 /degree /plusminus /twosuperior /threesuperior /acute /mu /paragraph /periodcentered /cedilla /onesuperior /ordmasculine /guillemotright /onequarter /onehalf /threequarters /questiondown % 0xC0 /Agrave /Aacute /Acircumflex /Atilde /Adieresis /Aring /AE /Ccedilla /Egrave /Eacute /Ecircumflex /Edieresis /Igrave /Iacute /Icircumflex /Idieresis % 0xD0 /Eth /Ntilde /Ograve /Oacute /Ocircumflex /Otilde /Odieresis /multiply /Oslash /Ugrave /Uacute /Ucircumflex /Udieresis /Yacute /Thorn /germandbls % 0xE0 /agrave /aacute /acircumflex /atilde /adieresis /aring /ae /ccedilla /egrave /eacute /ecircumflex /edieresis /igrave /iacute /icircumflex /idieresis % 0xF0 /eth /ntilde /ograve /oacute /ocircumflex /otilde /odieresis /divide /oslash /ugrave /uacute /ucircumflex /udieresis /yacute /thorn /ydieresis ] def %%EndProcSet %%BeginProcSet: texps.pro %! TeXDict begin/rf{findfont dup length 1 add dict begin{1 index/FID ne 2 index/UniqueID ne and{def}{pop pop}ifelse}forall[1 index 0 6 -1 roll exec 0 exch 5 -1 roll VResolution Resolution div mul neg 0 0]/Metrics exch def dict begin Encoding{exch dup type/integertype ne{pop pop 1 sub dup 0 le{pop}{[}ifelse}{FontMatrix 0 get div Metrics 0 get div def} ifelse}forall Metrics/Metrics currentdict end def[2 index currentdict end definefont 3 -1 roll makefont/setfont cvx]cvx def}def/ObliqueSlant{ dup sin S cos div neg}B/SlantFont{4 index mul add}def/ExtendFont{3 -1 roll mul exch}def/ReEncodeFont{CharStrings rcheck{/Encoding false def dup[exch{dup CharStrings exch known not{pop/.notdef/Encoding true def} if}forall Encoding{]exch pop}{cleartomark}ifelse}if/Encoding exch def} def end %%EndProcSet %%BeginProcSet: special.pro %! TeXDict begin/SDict 200 dict N SDict begin/@SpecialDefaults{/hs 612 N /vs 792 N/ho 0 N/vo 0 N/hsc 1 N/vsc 1 N/ang 0 N/CLIP 0 N/rwiSeen false N /rhiSeen false N/letter{}N/note{}N/a4{}N/legal{}N}B/@scaleunit 100 N /@hscale{@scaleunit div/hsc X}B/@vscale{@scaleunit div/vsc X}B/@hsize{ /hs X/CLIP 1 N}B/@vsize{/vs X/CLIP 1 N}B/@clip{/CLIP 2 N}B/@hoffset{/ho X}B/@voffset{/vo X}B/@angle{/ang X}B/@rwi{10 div/rwi X/rwiSeen true N}B /@rhi{10 div/rhi X/rhiSeen true N}B/@llx{/llx X}B/@lly{/lly X}B/@urx{ /urx X}B/@ury{/ury X}B/magscale true def end/@MacSetUp{userdict/md known {userdict/md get type/dicttype eq{userdict begin md length 10 add md maxlength ge{/md md dup length 20 add dict copy def}if end md begin /letter{}N/note{}N/legal{}N/od{txpose 1 0 mtx defaultmatrix dtransform S atan/pa X newpath clippath mark{transform{itransform moveto}}{transform{ itransform lineto}}{6 -2 roll transform 6 -2 roll transform 6 -2 roll transform{itransform 6 2 roll itransform 6 2 roll itransform 6 2 roll curveto}}{{closepath}}pathforall newpath counttomark array astore/gc xdf pop ct 39 0 put 10 fz 0 fs 2 F/|______Courier fnt invertflag{PaintBlack} if}N/txpose{pxs pys scale ppr aload pop por{noflips{pop S neg S TR pop 1 -1 scale}if xflip yflip and{pop S neg S TR 180 rotate 1 -1 scale ppr 3 get ppr 1 get neg sub neg ppr 2 get ppr 0 get neg sub neg TR}if xflip yflip not and{pop S neg S TR pop 180 rotate ppr 3 get ppr 1 get neg sub neg 0 TR}if yflip xflip not and{ppr 1 get neg ppr 0 get neg TR}if}{ noflips{TR pop pop 270 rotate 1 -1 scale}if xflip yflip and{TR pop pop 90 rotate 1 -1 scale ppr 3 get ppr 1 get neg sub neg ppr 2 get ppr 0 get neg sub neg TR}if xflip yflip not and{TR pop pop 90 rotate ppr 3 get ppr 1 get neg sub neg 0 TR}if yflip xflip not and{TR pop pop 270 rotate ppr 2 get ppr 0 get neg sub neg 0 S TR}if}ifelse scaleby96{ppr aload pop 4 -1 roll add 2 div 3 1 roll add 2 div 2 copy TR .96 dup scale neg S neg S TR}if}N/cp{pop pop showpage pm restore}N end}if}if}N/normalscale{ Resolution 72 div VResolution 72 div neg scale magscale{DVImag dup scale }if 0 setgray}N/psfts{S 65781.76 div N}N/startTexFig{/psf$SavedState save N userdict maxlength dict begin/magscale true def normalscale currentpoint TR/psf$ury psfts/psf$urx psfts/psf$lly psfts/psf$llx psfts /psf$y psfts/psf$x psfts currentpoint/psf$cy X/psf$cx X/psf$sx psf$x psf$urx psf$llx sub div N/psf$sy psf$y psf$ury psf$lly sub div N psf$sx psf$sy scale psf$cx psf$sx div psf$llx sub psf$cy psf$sy div psf$ury sub TR/showpage{}N/erasepage{}N/copypage{}N/p 3 def @MacSetUp}N/doclip{ psf$llx psf$lly psf$urx psf$ury currentpoint 6 2 roll newpath 4 copy 4 2 roll moveto 6 -1 roll S lineto S lineto S lineto closepath clip newpath moveto}N/endTexFig{end psf$SavedState restore}N/@beginspecial{SDict begin/SpecialSave save N gsave normalscale currentpoint TR @SpecialDefaults count/ocount X/dcount countdictstack N}N/@setspecial{ CLIP 1 eq{newpath 0 0 moveto hs 0 rlineto 0 vs rlineto hs neg 0 rlineto closepath clip}if ho vo TR hsc vsc scale ang rotate rwiSeen{rwi urx llx sub div rhiSeen{rhi ury lly sub div}{dup}ifelse scale llx neg lly neg TR }{rhiSeen{rhi ury lly sub div dup scale llx neg lly neg TR}if}ifelse CLIP 2 eq{newpath llx lly moveto urx lly lineto urx ury lineto llx ury lineto closepath clip}if/showpage{}N/erasepage{}N/copypage{}N newpath}N /@endspecial{count ocount sub{pop}repeat countdictstack dcount sub{end} repeat grestore SpecialSave restore end}N/@defspecial{SDict begin}N /@fedspecial{end}B/li{lineto}B/rl{rlineto}B/rc{rcurveto}B/np{/SaveX currentpoint/SaveY X N 1 setlinecap newpath}N/st{stroke SaveX SaveY moveto}N/fil{fill SaveX SaveY moveto}N/ellipse{/endangle X/startangle X /yrad X/xrad X/savematrix matrix currentmatrix N TR xrad yrad scale 0 0 1 startangle endangle arc savematrix setmatrix}N end %%EndProcSet TeXDict begin 39158280 55380996 1000 600 600 (dddmp-2.0.dvi) @start /Fa 143[55 1[55 7[28 2[50 99[{TeXBase1Encoding ReEncodeFont}4 99.6264 /Helvetica rf %DVIPSBitmapFont: Fb cmr12 12 3 /Fb 3 53 df<14FF010713E090381F81F890383E007C01FC133F4848EB1F8049130F4848 EB07C04848EB03E0A2000F15F0491301001F15F8A2003F15FCA390C8FC4815FEA54815FF B3A46C15FEA56D1301003F15FCA3001F15F8A26C6CEB03F0A36C6CEB07E0000315C06D13 0F6C6CEB1F806C6CEB3F00013E137C90381F81F8903807FFE0010090C7FC28447CC131> 48 D<143014F013011303131F13FFB5FC13E713071200B3B3B0497E497E007FB6FCA320 4278C131>I52 D E %EndDVIPSBitmapFont /Fc 64[50 29[39 12[55 55 25[44 44 66 44 50 28 39 39 1[50 50 50 72 28 44 1[28 50 50 28 44 50 44 50 50 10[61 2[50 4[66 83 55 2[33 2[61 1[72 66 61 61 15[50 2[25 33 25 2[33 33 37[50 2[{TeXBase1Encoding ReEncodeFont}45 99.6264 /Times-Italic rf %DVIPSBitmapFont: Fd cmmi12 12 3 /Fd 3 103 df60 D<127012FCB4FCEA7FC0EA1FF0EA 07FCEA01FF38007FC0EB1FF0EB07FE903801FF809038007FE0EC1FF8EC03FE913800FF80 ED3FE0ED0FF8ED03FF030013C0EE3FF0EE0FFCEE01FF9338007FC0EF1FF0EF07FCEF01FF 9438007FC0F01FE0A2F07FC0943801FF00EF07FCEF1FF0EF7FC04C48C7FCEE0FFCEE3FF0 EEFFC0030390C8FCED0FF8ED3FE0EDFF80DA03FEC9FCEC1FF8EC7FE0903801FF80D907FE CAFCEB1FF0EB7FC04848CBFCEA07FCEA1FF0EA7FC048CCFC12FC12703B3878B44C>62 D102 D E %EndDVIPSBitmapFont /Fe 134[42 2[42 42 23 32 28 1[42 42 42 65 23 2[23 42 42 28 37 42 1[42 37 12[51 10[28 4[60 1[55 19[21 28 21 44[{TeXBase1Encoding ReEncodeFont}26 83.022 /Times-Roman rf %DVIPSBitmapFont: Ff cmr7 7 2 /Ff 2 51 df<13381378EA01F8121F12FE12E01200B3AB487EB512F8A215267BA521>49 D<13FF000313E0380E03F0381800F848137C48137E00787F12FC6CEB1F80A4127CC7FC15 005C143E147E147C5C495A495A5C495A010EC7FC5B5B903870018013E0EA018039030003 0012065A001FB5FC5A485BB5FCA219267DA521>I E %EndDVIPSBitmapFont /Fg 103[60 26[60 1[60 60 60 60 60 60 60 60 60 60 60 60 60 60 60 60 2[60 60 60 60 60 60 60 60 60 3[60 1[60 3[60 60 1[60 60 1[60 60 1[60 60 3[60 1[60 1[60 60 60 1[60 60 1[60 1[60 1[60 60 60 60 60 60 60 60 60 60 60 60 60 60 60 5[60 38[{TeXBase1Encoding ReEncodeFont}62 99.6264 /Courier rf %DVIPSBitmapFont: Fh cmr8 8 2 /Fh 2 51 df<130C133C137CEA03FC12FFEAFC7C1200B3B113FE387FFFFEA2172C7AAB23 >49 DI E %EndDVIPSBitmapFont /Fi 105[50 28[50 50 2[55 33 39 44 1[55 50 55 83 28 2[28 1[50 33 44 55 44 55 50 10[72 1[66 55 3[78 72 94 66 3[78 1[61 66 72 72 66 72 13[50 50 50 1[28 25 33 45[{ TeXBase1Encoding ReEncodeFont}40 99.6264 /Times-Bold rf /Fj 139[40 1[53 1[66 60 66 100 33 2[33 3[53 3[60 23[47 2[73 18[60 60 60 2[30 46[{TeXBase1Encoding ReEncodeFont}16 119.552 /Times-Bold rf %DVIPSBitmapFont: Fk cmsy10 12 1 /Fk 1 16 df<49B4FC010F13E0013F13F8497F48B6FC4815804815C04815E04815F0A248 15F8A24815FCA3B712FEA96C15FCA36C15F8A26C15F0A26C15E06C15C06C15806C15006C 6C13FC6D5B010F13E0010190C7FC27277BAB32>15 D E %EndDVIPSBitmapFont /Fl 64[44 42[44 44 24[44 50 50 72 50 50 28 39 33 50 50 50 50 78 28 50 28 28 50 50 33 44 50 44 50 44 6[61 1[72 94 72 72 61 55 66 72 55 72 72 89 61 1[39 33 72 72 55 61 72 66 66 72 3[56 1[28 28 50 50 50 50 50 50 50 50 50 50 28 25 33 25 2[33 33 36[55 55 2[{TeXBase1Encoding ReEncodeFont}74 99.6264 /Times-Roman rf %DVIPSBitmapFont: Fm cmsy10 14.4 2 /Fm 2 104 df102 DI E %EndDVIPSBitmapFont /Fn 105[60 27[53 4[60 33 47 40 60 60 60 60 93 33 2[33 1[60 40 53 60 53 60 53 7[86 4[73 66 1[86 66 3[73 2[40 1[86 1[73 86 80 1[86 110 5[33 60 4[60 1[60 60 60 1[30 40 30 44[{TeXBase1Encoding ReEncodeFont}42 119.552 /Times-Roman rf /Fo 136[104 1[80 48 56 64 1[80 72 80 120 40 80 1[40 1[72 1[64 80 64 80 72 12[96 80 104 1[88 1[104 135 3[56 2[88 1[104 104 96 104 6[48 1[72 72 72 72 72 72 72 72 72 1[36 46[{TeXBase1Encoding ReEncodeFont}41 143.462 /Times-Bold rf end %%EndProlog %%BeginSetup %%Feature: *Resolution 600dpi TeXDict begin %%BeginPaperSize: a4 a4 %%EndPaperSize %%EndSetup %%Page: 1 1 1 0 bop 472 600 a Fo(DDDMP:)35 b(Decision)f(Diagram)f(DuMP)j(package) 1480 830 y(Release)e(2.0)462 1230 y Fn(Gianpiero)c(Cabodi)2402 1232 y(Stef)o(ano)g(Quer)1316 1506 y(Politecnico)g(di)g(T)-10 b(orino)1024 1656 y(Dip.)30 b(di)g(Automatica)g(e)g(Informatica)1119 1805 y(Corso)f(Duca)h(de)n(gli)g(Abruzzi)g(24)1277 1955 y(I\22610129)e(T)-5 b(urin,)29 b(IT)-11 b(AL)f(Y)1038 2104 y(E-mail:)38 b Fm(f)p Fn(cabodi,quer)p Fm(g)p Fn(@polito.it)-189 2614 y Fo(1)143 b(Intr)m(oduction)-189 2837 y Fl(The)27 b(DDDMP)h(package)f(de\002nes)h(formats)f(and)g(rules)g(to)g(store)g (DD)g(on)g(\002le.)39 b(More)27 b(in)g(particular)g(it)g(contains)g(a) -189 2958 y(set)e(of)g(functions)e(to)i(dump)e(\(store)i(and)g(load\))g (DDs)f(and)h(DD)g(forests)f(on)h(\002le)g(in)f(dif)n(ferent)h(formats.) 47 3078 y(In)30 b(the)g(present)g(implementation,)f(BDDs)h(\(R)l (OBDDs\))h(and)f(ADD)g(\(Algebraic)g(Decision)g(Diagram\))g(of)-189 3199 y(the)g(CUDD)g(package)g(\(v)o(ersion)f(2.3.0)g(or)h(higher\))g (are)g(supported.)45 b(These)30 b(structures)f(can)h(be)g(represented)g (on)-189 3319 y(\002les)25 b(either)g(in)f(te)o(xt,)g(binary)-6 b(,)24 b(or)h(CNF)g(\(DIMA)l(CS\))h(formats.)47 3439 y(The)f(main)f(rules)h(used)f(are)i(follo)n(wing)d(rules:)-44 3643 y Fk(\017)49 b Fl(A)30 b(\002le)h(contains)e(a)i(single)e(BDD/ADD) h(or)g(a)h(forest)f(of)g(BDDs/ADD,)g(i.e.,)i(a)e(v)o(ector)g(of)g (Boolean)h(func-)55 3763 y(tions.)-44 3966 y Fk(\017)49 b Fl(Inte)o(ger)21 b(inde)o(x)o(es)f(are)i(used)f(instead)g(of)g (pointers)g(to)g(reference)i(nodes.)29 b(BDD/ADD)21 b(nodes)g(are)h (numbered)55 4087 y(with)j(contiguous)g(numbers,)g(from)h(1)g(to)f (NNodes)h(\(total)f(number)h(of)g(nodes)g(on)f(a)i(\002le\).)35 b(0)26 b(is)f(not)h(used)f(to)55 4207 y(allo)n(w)f(ne)o(gati)n(v)o(e)e (inde)o(x)o(es)h(for)i(complemented)f(edges.)-44 4411 y Fk(\017)49 b Fl(A)23 b(\002le)g(contains)f(a)h(header)l(,)h (including)d(se)n(v)o(eral)h(informations)f(about)h(v)n(ariables)h(and) f(roots)g(of)h(BDD)h(func-)55 4531 y(tions,)32 b(then)e(the)h(list)g (of)g(nodes.)49 b(The)32 b(header)f(is)g(al)o(w)o(ays)g(represented)h (in)f(te)o(xt)f(format)h(\(also)g(for)g(binary)55 4651 y(\002les\).)g(BDDs,)25 b(ADDs,)f(and)h(CNF)h(\002les)f(share)g(a)g (similar)f(format)g(header)-5 b(.)-44 4855 y Fk(\017)49 b Fl(BDD/ADD)40 b(nodes)g(are)h(listed)f(follo)n(wing)e(their)i (numbering,)j(which)d(is)g(produced)g(by)h(a)f(post-order)55 4975 y(tra)n(v)o(ersal,)24 b(in)h(such)f(a)h(w)o(ay)g(that)g(a)g(node)f (is)h(al)o(w)o(ays)f(listed)g(after)h(its)f(Then/Else)g(children.)47 5179 y(In)32 b(the)f(sequel)g(we)g(describe)h(more)f(in)g(detail)f(the) h(dif)n(ferent)g(formats)g(and)g(procedures)h(a)n(v)n(ailable.)49 b(First)-189 5299 y(of)26 b(all,)f(we)h(describe)f(BDDs)h(and)g(ADDs)f (formats)g(and)g(procedure.)33 b(Secondly)-6 b(,)26 b(we)f(concentrate) h(on)f(CNF)i(\002les,)-189 5419 y(i.e.,)e(ho)n(w)f(to)g(translate)g(a)i (BDD)f(or)g(a)g(forest)g(of)f(BDDs)h(into)f(a)h(CNF)h(formula)e(and)h (vice-v)o(ersa.)1794 5800 y(1)p eop %%Page: 2 2 2 1 bop -189 218 a Fo(2)143 b(BDD)35 b(and)g(ADD)g(Support)-189 441 y Fl(In)23 b(this)f(section)g(we)g(describe)h(format)g(and)f (procedure)h(re)o(garding)f(BDDs)h(and)f(ADDs.)30 b(W)-8 b(e)23 b(speci\002cally)g(refer)g(to)-189 562 y(BDDs)h(in)g(the)g (description)e(as)j(ADD)e(may)h(be)g(seen)g(as)h(an)f(e)o(xtension)e (and)i(will)f(be)h(described)g(later)-5 b(.)30 b(First)24 b(of)g(all,)-189 682 y(we)29 b(concentrate)f(on)g(the)g(format)g(used)g (to)g(store)g(these)g(structure,)h(then)f(we)g(describe)h(the)f (procedure)h(a)n(v)n(ailable)-189 802 y(to)24 b(store)h(and)g(load)f (them.)-189 1094 y Fj(2.1)119 b(F)m(ormat)-189 1281 y Fl(BDD)30 b(dump)f(\002les)g(are)i(composed)e(of)g(tw)o(o)g(sections:) 40 b(The)29 b(header)h(and)g(the)f(list)g(of)h(nodes.)44 b(The)30 b(header)g(has)g(a)-189 1402 y(common)c(\(te)o(xt\))h(format,) h(while)e(the)i(list)e(of)h(nodes)g(is)g(either)g(in)g(te)o(xt)g(or)g (binary)g(format.)38 b(In)28 b(te)o(xt)e(format)h(nodes)-189 1522 y(are)33 b(represented)f(with)f(redundant)g(informations,)h(where) h(the)f(main)f(goal)g(is)h(readability)-6 b(,)32 b(while)g(the)f (purpose)-189 1642 y(of)i(binary)f(format)g(is)g(minimizing)e(the)i(o)o (v)o(erall)f(storage)h(size)h(for)g(BDD)f(nodes.)54 b(The)32 b(header)h(format)f(is)g(k)o(ept)-189 1763 y(common)h(to)h(te)o(xt)g (and)g(binary)g(formats)g(for)h(sak)o(e)f(of)h(simplicity:)47 b(No)34 b(particular)g(optimization)f(is)h(presently)-189 1883 y(done)29 b(on)f(binary)h(\002le)g(headers,)h(whose)f(size)g(is)f (by)h(f)o(ar)g(dominated)f(by)h(node)f(lists)g(in)g(the)h(case)g(of)g (lar)n(ge)h(BDDs)-189 2003 y(\(se)n(v)o(eral)24 b(thousands)g(of)h(DD)f (nodes\).)-189 2266 y Fi(2.1.1)99 b(Header)-189 2453 y Fl(The)23 b(header)h(has)f(the)g(same)g(format)g(both)g(for)g(te)o (xtual)f(and)i(binary)e(dump.)30 b(F)o(or)23 b(sak)o(e)g(of)h (generality)e(and)h(because)-189 2574 y(of)f(dynamic)g(v)n(ariable)g (ordering)g(both)f(v)n(ariable)h(IDs)g(and)g(permutations)2377 2537 y Fh(1)2438 2574 y Fl(are)h(included.)29 b(Names)22 b(are)h(optionally)-189 2694 y(listed)35 b(for)h(input)f(v)n(ariables)g (and)h(for)h(the)e(stored)h(functions.)63 b(Ne)n(w)36 b(auxiliary)f(IDs)h(are)h(also)e(allo)n(wed.)64 b(Only)-189 2814 y(the)34 b(v)n(ariables)f(in)g(the)h(true)g(support)f(of)h(the)f (stored)h(BDDs)g(are)h(listed.)56 b(All)34 b(information)e(on)i(v)n (ariables)f(\(IDs,)-189 2935 y(permutations,)c(names,)i(auxiliary)e (IDs\))h(sorted)g(by)g(IDs,)h(and)e(the)o(y)h(are)g(restricted)g(to)f (the)h(true)g(support)f(of)h(the)-189 3055 y(dumped)22 b(BDD,)h(while)g(IDs)g(and)f(permutations)g(are)h(referred)i(to)d(the)h (writing)f(BDD)h(manager)-5 b(.)30 b(Names)22 b(can)i(thus)-189 3175 y(be)h(sorted)f(by)h(v)n(ariable)f(ordering)h(by)f(permuting)g (them)g(according)h(to)f(the)h(permutations)e(stored)h(in)h(the)f (\002le.)47 3296 y(As)h(an)g(e)o(xample,)f(the)g(header)i(\(in)e(te)o (xt)g(mode\))h(of)f(the)h(ne)o(xt)f(state)h(functions)e(of)i(circuit)g (s27)f(follo)n(ws:)-189 3494 y Fg(.ver)59 b(DDDMP-2.0)-189 3615 y(.mode)g(A)-189 3735 y(.varinfo)f(3)-189 3855 y(.dd)h(s27-delta) -189 3976 y(.nnodes)f(16)-189 4096 y(.nvars)g(10)-189 4216 y(.nsuppvars)g(7)-189 4337 y(.varnames)g(G0)h(G1)g(G2)h(G3)f(G5)g (G6)h(G7)-189 4457 y(.orderedvarnames)c(G0)k(G1)f(G2)g(G3)h(G5)f(G6)g (G7)-189 4578 y(.ids)g(0)g(1)h(2)g(3)f(4)h(5)f(6)-189 4698 y(.permids)f(0)i(1)f(2)h(3)f(5)h(7)f(9)-189 4818 y(.auxids)f(1)i(2)f(3)h(4)f(5)h(6)g(7)-189 4939 y(.nroots)e(3)-189 5059 y(.rootids)g(6)i(-13)f(-16)-189 5179 y(.rootnames)f(G10)h(G11)g (G13)47 5378 y Fl(The)25 b(lines)f(contain)g(the)h(follo)n(wing)e (informations:)p -189 5460 1607 4 v -77 5521 a Ff(1)-40 5551 y Fe(The)d(permutation)e(of)i(the)g(i-th)h(v)n(ariable)e(ID)h(is)h (the)f(relati)n(v)o(e)g(position)f(of)h(the)g(v)n(ariable)f(in)i(the)f (ordering.)1794 5800 y Fl(2)p eop %%Page: 3 3 3 2 bop -44 218 a Fk(\017)49 b Fl(Dddmp)24 b(v)o(ersion)f(information.) -44 411 y Fk(\017)49 b Fl(File)25 b(mode)f(\(A)h(for)g(ASCII)h(te)o (xt,)e(B)h(for)g(binary)g(mode\).)-44 604 y Fk(\017)49 b Fl(V)-11 b(ar)n(-e)o(xtra-info)25 b(\(0:)30 b(v)n(ariable)24 b(ID,)h(1:)31 b(permID,)24 b(2:)31 b(aux)25 b(ID,)g(3:)30 b(v)n(ariable)24 b(name,)h(4)g(no)f(e)o(xtra)h(info\).)-44 797 y Fk(\017)49 b Fl(Name)25 b(of)g(dd)f(\(optional\).)-44 990 y Fk(\017)49 b Fl(T)-8 b(otal)24 b(number)g(of)h(nodes)g(in)f(the)h (\002le.)-44 1183 y Fk(\017)49 b Fl(Number)24 b(of)h(v)n(ariables)f(of) h(the)g(writing)f(DD)g(manager)-5 b(.)-44 1375 y Fk(\017)49 b Fl(Number)24 b(of)h(v)n(ariables)f(in)h(the)f(true)h(support)f(of)h (the)f(stored)h(DDs.)-44 1568 y Fk(\017)49 b Fl(V)-11 b(ariable)25 b(names)f(\(optional\))g(for)h(all)g(the)f(v)n(ariables)g (in)h(the)f(BDD/ADD)h(support.)-44 1761 y Fk(\017)49 b Fl(V)-11 b(ariable)20 b(names)g(for)h(all)f(the)g(v)n(ariables)f(in)h (the)g(DD)h(manager)f(during)g(the)g(storing)f(phase.)29 b(Notice)20 b(that)g(this)55 1882 y(information)k(w)o(as)h(not)g (stored)g(by)g(pre)n(vious)f(v)o(ersions)g(of)i(the)f(same)g(tool.)32 b(Full)25 b(backw)o(ard)g(compatibility)55 2002 y(is)f(guaranteed)h(by) g(the)f(present)h(implementation)d(of)j(the)g(tool.)-44 2195 y Fk(\017)49 b Fl(V)-11 b(ariable)25 b(IDs.)-44 2388 y Fk(\017)49 b Fl(V)-11 b(ariable)25 b(permuted)f(IDs.)-44 2581 y Fk(\017)49 b Fl(V)-11 b(ariable)25 b(auxiliary)f(IDs)h (\(optional\).)-44 2774 y Fk(\017)49 b Fl(Number)24 b(of)h(BDD)g (roots.)-44 2967 y Fk(\017)49 b Fl(Inde)o(x)o(es)24 b(of)h(BDD)g(roots) f(\(complemented)g(edges)g(allo)n(wed\).)-44 3160 y Fk(\017)49 b Fl(Names)24 b(of)h(BDD)h(roots)e(\(optional\).)-189 3332 y(Notice)h(that)f(a)h(\002eld)-189 3504 y Fg(.add)-189 3676 y Fl(is)f(present)h(after)g(the)g(dddmp)f(v)o(ersion)f(for)j (\002les)e(containing)g(ADDs.)-189 3936 y Fi(2.1.2)99 b(T)-9 b(ext)25 b(F)n(ormat)-189 4124 y Fl(In)g(te)o(xt)f(mode)g(nodes) g(are)i(listed)e(on)g(a)h(te)o(xt)f(line)h(basis.)30 b(Each)25 b(a)g(node)f(is)h(represented)g(as)-189 4296 y Fg()57 b([])f()588 4416 y()h()-189 4588 y Fl(where)25 b(all)g(inde)o(x)o(es)e(are)j(inte)o(ger)e(numbers.)47 4709 y(This)h(format)g(is)g(redundant)f(\(due)i(to)f(the)g(node)g (ordering,)g Fd(<)p Fl(Node-inde)o(x)p Fd(>)f Fl(is)g(and)i (incremental)e(inte)o(ger\))-189 4829 y(b)n(ut)g(we)h(k)o(eep)g(it)g (for)g(readability)-6 b(.)47 4949 y Fd(<)p Fl(V)-11 b(ar)n(-e)o (xtra-info)p Fd(>)34 b Fl(\(optional)e(redundant)i(\002eld\))g(is)f (either)h(an)g(inte)o(ger)f(\(ID,)h(PermID,)g(or)g(auxID\))g(or)g(a) -189 5070 y(string)k(\(v)n(ariable)h(name\).)75 b Fd(<)p Fl(V)-11 b(ar)n(-internal-inde)o(x)p Fd(>)38 b Fl(is)h(an)g(internal)g (v)n(ariable)g(inde)o(x:)59 b(V)-11 b(ariables)39 b(in)g(the)g(true) -189 5190 y(support)25 b(of)h(the)g(stored)g(BDDs)g(are)h(numbered)e (with)g(ascending)h(inte)o(gers)f(starting)g(from)h(0,)g(and)g(follo)n (wing)e(the)-189 5311 y(v)n(ariable)g(ordering.)31 b Fd(<)p Fl(Then-inde)o(x)p Fd(>)23 b Fl(and)i Fd(<)p Fl(Else-inde)o(x)p Fd(>)e Fl(are)j(signed)e(inde)o(x)o(es)f(of)i(children)f(nodes.)47 5431 y(In)h(the)f(follo)n(wing,)f(we)i(report)f(the)g(list)g(of)h (nodes)f(of)g(the)h(s27)f(ne)o(xt)f(state)i(functions)e(\(see)i(pre)n (vious)e(header)-189 5551 y(e)o(xample\):)1794 5800 y(3)p eop %%Page: 4 4 4 3 bop -189 218 a Fg(.nodes)-189 338 y(1)60 b(T)f(1)h(0)f(0)-189 459 y(2)h(G7)f(6)g(1)h(-1)-189 579 y(3)g(G5)f(4)g(1)h(2)-189 699 y(4)g(G3)f(3)g(3)h(1)-189 820 y(5)g(G1)f(1)g(1)h(4)-189 940 y(6)g(G0)f(0)g(5)h(-1)-189 1061 y(7)g(G6)f(5)g(1)h(-1)-189 1181 y(8)g(G5)f(4)g(1)h(-7)-189 1301 y(9)g(G6)f(5)g(1)h(-2)-189 1422 y(10)f(G5)h(4)f(1)h(-9)-189 1542 y(11)f(G3)h(3)f(10)h(8)-189 1662 y(12)f(G1)h(1)f(8)h(11)-189 1783 y(13)f(G0)h(0)f(5)h(12)-189 1903 y(14)f(G2)h(2)f(1)h(-1)-189 2024 y(15)f(G2)h(2)f(1)h(-2)-189 2144 y(16)f(G1)h(1)f(14)h(15)-189 2264 y(.end)-189 2468 y Fl(The)27 b(list)f(is)h(enclosed)g(between)g(the)g Fg(.nodes)f Fl(and)h Fg(.end)f Fl(lines.)37 b(First)27 b(node)g(is)g(the)g(one)g(constant,)f(each)i(node)-189 2588 y(contains)c(the)h(optional)e(v)n(ariable)h(name.)47 2708 y(F)o(or)29 b(ADDs)f(more)h(than)f(one)h(constant)e(is)i(stored)f (in)g(the)g(\002le.)43 b(Each)29 b(constant)f(has)g(the)h(same)f (format)h(we)-189 2829 y(ha)n(v)o(e)c(just)e(analyzed)i(for)g(the)g (BDD)g(b)n(ut)g(the)f(represented)h(v)n(alue)f(is)h(stored)f(as)h(a)g (\003oat)g(number)-5 b(.)-189 3095 y Fi(2.1.3)99 b(Binary)25 b(F)n(ormat)-189 3283 y Fl(The)h(binary)g(format)f(is)h(not)f(allo)n (wed)g(for)i(ADDs.)33 b(As)26 b(a)h(consequence)f(we)g(concentrate)g (only)f(on)h(BDDs)g(in)g(this)-189 3403 y(section.)k(In)25 b(binary)f(mode)h(nodes)f(are)i(represented)f(as)g(a)g(sequence)g(of)g (bytes,)f(encoding)g(tuples)-189 3606 y Fg()-189 3727 y([])-189 3847 y([])-189 3968 y([])-189 4171 y Fl(in)30 b(an)g(optimized)f(w)o(ay)-6 b(.)46 b(Only)29 b(the)h(\002rst)g(byte)g(\(code\))h(is)e(mandatory)-6 b(,)30 b(while)g(inte)o(ger)f(inde)o(x)o(es)g(are)i(represented)-189 4291 y(in)c(absolute)f(or)h(relati)n(v)o(e)f(mode,)h(where)h(relati)n (v)o(e)e(means)g(of)n(fset)h(with)f(respect)i(to)e(a)i(Then/Else)e (node)h(info.)37 b(The)-189 4412 y(best)23 b(between)g(absolute)f(and)h (relati)n(v)o(e)e(representation)i(is)f(chosen)h(and)g(relati)n(v)o(e)f (1)h(is)f(directly)g(coded)h(in)g Fd(<)p Fl(Node-)-189 4532 y(code)p Fd(>)e Fl(without)f(an)o(y)g(e)o(xtra)h(info.)29 b(Suppose)21 b(V)-11 b(ar\(NodeId\),)22 b(Then\(NodeId\))f(and)g (Else\(NodeId\))f(represent)i(infos)-189 4652 y(about)i(a)h(gi)n(v)o (en)f(node.)30 b Fd(<)p Fl(Node-code)p Fd(>)25 b Fl(is)f(a)h(byte)g (which)f(contains)g(the)h(follo)n(wing)e(bit)h(\002elds)h(\(MSB)g(to)g (LSB\))-44 4856 y Fk(\017)49 b Fl(Unused)24 b(:)31 b(1)24 b(bit)-44 5059 y Fk(\017)49 b Fl(V)-11 b(ariable:)30 b(2)25 b(bits,)f(one)h(of)g(the)f(follo)n(wing)f(codes)171 5288 y Fi(\226)49 b Fl(DDDMP)p 636 5288 30 4 v 35 w(ABSOLUTE)p 1191 5288 V 36 w(ID:)22 b(V)-11 b(ar\(NodeId\))22 b(is)f(represented)h (in)g(absolute)f(form)g(as)h Fd(<)p Fl(V)-11 b(ar)n(-internal-)270 5408 y(info)p Fd(>)24 b Fl(=)h(V)-11 b(ar\(NodeId\))25 b(follo)n(ws)e(\(absolute)i(info\))1794 5800 y(4)p eop %%Page: 5 5 5 4 bop 171 218 a Fi(\226)49 b Fl(DDDMP)p 636 218 30 4 v 35 w(RELA)-11 b(TIVE)p 1147 218 V 36 w(ID:)32 b(V)-11 b(ar\(NodeId\))32 b(is)g(represented)g(in)f(relati)n(v)o(e)g(form)h(as) g Fd(<)p Fl(V)-11 b(ar)n(-internal-)270 338 y(info\277)24 b(=)h(Min\(V)-11 b(ar\(Then\(NodeId\)\),V)g(ar\(Else\(NodeId\)\)\)-V)g (ar\(NodeId\))171 500 y Fi(\226)49 b Fl(DDDMP)p 636 500 V 35 w(RELA)-11 b(TIVE)p 1147 500 V 36 w(1:)27 b(the)19 b(\002eld)g Fd(<)p Fl(V)-11 b(ar)n(-internal-info)p Fd(>)18 b Fl(does)h(not)f(follo)n(w)-6 b(,)18 b(because)h(V)-11 b(ar\(NodeId\))270 620 y(=)25 b(Min\(V)-11 b(ar\(Then\(NodeId\)\),V)g (ar\(Else\(NodeId\)\)\)-1)171 782 y Fi(\226)49 b Fl(DDDMP)p 636 782 V 35 w(TERMIN)m(AL:)24 b(Node)h(is)f(a)h(terminal,)f(no)g(v)n (ar)h(info)g(required)-44 1011 y Fk(\017)49 b Fl(T)25 b(:)f(2)h(bits,)f(with)g(codes)h(similar)e(to)i(V)171 1214 y Fi(\226)49 b Fl(DDDMP)p 636 1214 V 35 w(ABSOLUTE)p 1191 1214 V 36 w(ID:)20 b Fd(<)p Fl(Then-info)p Fd(>)f Fl(is)h(represented)g(in)g(absolute)f(form)h(as)g Fd(<)p Fl(Then-info)p Fd(>)270 1334 y Fl(=)25 b(Then\(NodeId\))171 1496 y Fi(\226)49 b Fl(DDDMP)p 636 1496 V 35 w(RELA)-11 b(TIVE)p 1147 1496 V 36 w(ID:)28 b(Then\(NodeId\))f(is)g(represented)h (in)g(relati)n(v)o(e)e(form)i(as)g Fd(<)p Fl(Then-info)p Fd(>)270 1617 y Fl(=)d(Nodeid-Then\(NodeId\))171 1779 y Fi(\226)49 b Fl(DDDMP)p 636 1779 V 35 w(RELA)-11 b(TIVE)p 1147 1779 V 36 w(1:)30 b(no)25 b Fd(<)p Fl(Then-info)p Fd(>)f Fl(follo)n(ws,)f(because)i(Then\(NodeId\))g(=)g(NodeId-1)171 1941 y Fi(\226)49 b Fl(DDDMP)p 636 1941 V 35 w(TERMIN)m(AL:)24 b(Then)h(Node)f(is)h(a)g(terminal,)f(no)g(info)h(required)f(\(for)i(R)l (OBDDs\))-44 2144 y Fk(\017)49 b Fl(Ecompl)24 b(:)30 b(1)25 b(bit,)f(if)h(1)g(means)f(that)g(the)h(else)g(edge)g(is)f (complemented)-44 2347 y Fk(\017)49 b Fl(E)25 b(:)f(2)h(bits,)f(with)g (codes)h(and)f(meanings)g(as)h(for)g(the)g(Then)f(edge)-189 2551 y(DD)35 b(node)f(codes)h(are)h(written)e(as)h(one)g(byte.)60 b Fd(<)p Fl(V)-11 b(ar)n(-internal-inde)o(x)p Fd(>)p Fl(,)36 b Fd(<)p Fl(Then-inde)o(x)p Fd(>)p Fl(,)g Fd(<)p Fl(Else-inde)o(x)p Fd(>)e Fl(\(if)-189 2671 y(required\))25 b(are)h(represented)f(as)g(unsigned)e(inte)o(ger)h(v)n(alues)g(on)h(a)g (suf)n(\002cient)f(set)h(of)g(bytes)f(\(MSByte)h(\002rst\).)47 2792 y(Inte)o(gers)h(of)f(an)o(y)h(length)e(are)j(written)e(as)h (sequences)g(of)g(\224link)o(ed\224)f(bytes)g(\(MSByte)h(\002rst\).)34 b(F)o(or)26 b(each)g(byte)-189 2912 y(7)f(bits)f(are)h(used)g(for)g (data)g(and)f(one)h(\(MSBit\))g(as)g(link)f(with)g(a)h(further)g(byte)g (\(MSB)g(=)g(1)g(means)f(one)h(more)g(byte\).)47 3032 y(Lo)n(w)f(le)n(v)o(el)g(read/write)h(of)g(bytes)f(\002lters)h Fd(<)p Fl(CR)p Fd(>)p Fl(,)g Fd(<)p Fl(LF)p Fd(>)g Fl(and)g Fd(<)p Fl(ctrl-Z)p Fd(>)f Fl(through)g(escape)h(sequences.)-189 3327 y Fj(2.2)119 b(Implementation)-189 3515 y Fl(Store)24 b(and)g(load)g(for)g(single)g(Boolean)g(functions)f(and)h(arrays)g(of)g (Boolean)g(functions)f(are)i(implemented.)k(More-)-189 3635 y(o)o(v)o(er)l(,)37 b(the)e(current)h(presentation)f(includes)f (functions)h(to)g(retrie)n(v)o(e)g(v)n(ariables)f(names,)k(auxiliary)d (identi\002erss,)-189 3756 y(and)c(all)g(the)g(information)f(contained) h(in)f(the)h(header)h(of)f(the)h(\002les.)50 b(This)30 b(information)g(can)h(be)h(used)f(as)g(a)g(pre-)-189 3876 y(processing)19 b(step)g(for)i(load)e(operations.)28 b(These)20 b(functions)f(allo)n(w)f(to)i(o)o(v)o(ercome)f(fe)n(w)g (limitations)f(of)h(the)h(pre)n(vious)-189 3997 y(implementations.)-189 4263 y Fi(2.2.1)99 b(Storing)25 b(Decision)g(Diagrams)-189 4450 y Fc(Dddmp)p 111 4450 V 35 w(cuddBddStor)l(e)f Fl(and)h Fc(Dddmp)p 1195 4450 V 35 w(cuddBddArr)o(ayStor)l(e)e Fl(are)j(the)f(tw)o(o)f(store)h(functions,)f(used)h(to)g(store)f(sin-) -189 4571 y(gle)f(BDD)h(or)g(a)f(forest)h(of)f(BDDs,)h(respecti)n(v)o (ely)-6 b(.)28 b(Internally)-6 b(,)23 b Fc(Dddmp)p 2275 4571 V 35 w(cuddBddStor)l(e)f Fl(b)n(uilds)g(a)i(dummy)e(1)h(entry)-189 4691 y(array)j(of)e(BDDs,)h(and)g(calls)g Fc(dddmp)p 1102 4691 V 35 w(cuddBddArr)o(ayStor)l(e)p Fl(.)47 4811 y(Since)30 b(con)l(v)o(ersion)e(from)h(DD)h(pointers)e(to)h(inte)o(ger) f(is)h(required,)i(DD)e(nodes)g(are)h(temporarily)e(remo)o(v)o(ed)-189 4932 y(from)23 b(the)f(unique)h(hash.)29 b(This)23 b(mak)o(es)f(room)g (in)h(their)f Fc(ne)n(xt)h Fl(\002eld)h(to)e(store)h(node)f(IDs.)30 b(Nodes)23 b(are)h(re-link)o(ed)e(after)-189 5052 y(the)i(store)g (operation,)g(possible)f(in)g(a)i(modi\002ed)e(order)-5 b(.)31 b(Dumping)22 b(is)i(either)g(in)g(te)o(xt)f(or)i(binary)f(form.) 30 b(Both)24 b(a)g(\002le)-189 5173 y(pointer)31 b(\()p Fc(fp)p Fl(\))g(and)g(a)h(\002le)g(name)f(\()p Fc(fname)p Fl(\))h(are)g(pro)o(vided)e(as)h(inputs)f(parameters)i(to)f(store)g (routines.)50 b(BDDs)31 b(are)-189 5293 y(stored)c(to)g(the)g(already)g (open)h(\002le)f Fc(fp)p Fl(,)h(if)f(not)g(NULL.)g(Otherwise)f(\002le)i (whose)f(name)g(is)g Fc(fname)g Fl(is)g(opened.)38 b(This)-189 5413 y(is)24 b(intended)g(to)h(allo)n(w)f(either)g(DD)h(storage)g (within)e(\002les)i(containing)f(other)g(data,)h(or)g(to)g(speci\002c)g (\002les.)1794 5800 y(5)p eop %%Page: 6 6 6 5 bop -189 218 a Fi(2.2.2)99 b(Loading)25 b(Decision)g(Diagrams)-189 405 y Fc(Dddmp)p 111 405 30 4 v 35 w(cuddBddLoad)37 b Fl(and)h Fc(Dddmp)p 1219 405 V 35 w(cuddBddArr)o(ayLoad)f Fl(are)h(the)g(load)g(functions,)i(which)e(read)g(a)g(BDD)-189 526 y(dump)24 b(\002le.)47 646 y(F)o(ollo)n(wing)34 b(the)h(store)h (function,)h(the)f(main)f(BDD)h(load)f(function,)j Fc(Dddmp)p 2813 646 V 35 w(cuddBddLoad)p Fl(,)f(is)f(imple-)-189 767 y(mented)g(by)g(calling)f(the)h(main)g(BDD-array)h(loading)f (function)f Fc(Dddmp)p 2466 767 V 35 w(cuddBddArr)o(ayLoad)p Fl(.)63 b(A)37 b(dynamic)-189 887 y(v)o(ector)24 b(of)h(DD)g(pointers)f (is)g(temporarily)g(allocated)h(to)f(support)g(con)l(v)o(ersion)f(from) i(DD)g(inde)o(x)o(es)e(to)h(pointers.)47 1007 y(Se)n(v)o(eral)40 b(criteria)f(are)i(supported)d(for)i(v)n(ariable)f(match)g(between)g (\002le)h(and)g(DD)f(manager)l(,)k(practically)-189 1128 y(allo)n(wing)37 b(v)n(ariable)h(permutations)f(or)i(compositions)d (while)i(loading)g(DDs.)71 b(V)-11 b(ariable)39 b(match)f(between)h (the)-189 1248 y(DD)32 b(manager)g(and)g(the)g(BDD)g(\002le)g(is)g (optionally)e(based)i(in)f Fc(IDs)p Fl(,)j Fc(perids)p Fl(,)f Fc(varnames)p Fl(,)g Fc(var)o(auxids)p Fl(;)g(also)f(direct)-189 1369 y(composition)j(between)j Fc(IDs)g Fl(and)f Fc(composeids)g Fl(is)g(supported.)68 b(The)38 b Fc(varmatc)o(hmode)e Fl(parameter)i(is)f(used)g(to)-189 1489 y(select)27 b(mathing)e(mode.) 37 b(More)27 b(in)f(detail,)h(tw)o(o)f(match)h(modes)f(use)h(the)f (information)g(within)f(the)i(DD)g(manager)l(,)-189 1609 y(the)e(other)f(ones)h(use)g(e)o(xtra)f(information,)f(which)i(support) f(an)o(y)g(v)n(ariable)g(remap)h(or)g(change)g(in)f(the)h(ordering.)-44 1813 y Fk(\017)49 b Fl(v)n(armatchnode=DDDMP)p 1040 1813 V 35 w(V)-13 b(AR)p 1272 1813 V 35 w(MA)i(TCHIDS)19 b(allo)n(ws)f (loading)g(a)h(DD)g(k)o(eeping)f(v)n(ariable)g(IDs)h(unchanged)55 1933 y(\(re)o(gardless)24 b(of)h(the)f(v)n(ariable)h(ordering)f(of)h (the)g(reading)f(manager)-5 b(.)55 2095 y(This)24 b(is)g(useful,)g(for) h(e)o(xample,)f(when)g(sw)o(apping)g(DDs)g(to)h(\002le)g(and)f (restoring)g(them)g(later)h(from)f(\002le,)h(after)55 2215 y(possible)e(v)n(ariable)i(reordering)g(acti)n(v)n(ations.)-44 2419 y Fk(\017)49 b Fl(v)n(armatchnode=DDDMP)p 1040 2419 V 35 w(V)-13 b(AR)p 1272 2419 V 35 w(MA)i(TCHPERMIDS)36 b(is)e(used)h(to)f(allo)n(w)g(v)n(ariable)g(match)h(according)55 2539 y(to)h(the)h(position)e(in)i(the)g(ordering)f(\(retrie)n(v)o(ed)g (by)h(array)h(of)f(permutations)e(stored)h(on)h(\002le)g(and)g(within) 55 2660 y(the)h(reading)g(DD)h(manager\).)72 b(A)38 b(possible)f (application)h(is)g(retrie)n(ving)f(BDDs)i(stored)f(after)h(dynamic)55 2780 y(reordering,)28 b(from)g(a)g(DD)g(manager)g(where)h(all)e(v)n (ariable)h(IDs)f(map)h(their)f(position)g(in)g(the)h(ordering,)g(and)55 2900 y(the)d(loaded)f(BDD)h(k)o(eeps)g(the)g(ordering)f(as)h(stored)f (on)h(\002le.)-44 3104 y Fk(\017)49 b Fl(v)n(armatchnode=DDDMP)p 1040 3104 V 35 w(V)-13 b(AR)p 1272 3104 V 35 w(MA)i(TCHN)m(AMES)26 b(requires)h(a)h(not)e(NULL)h(v)n(armatchmodes)f(param-)55 3224 y(eter;)34 b(this)c(is)g(a)h(v)o(ector)g(of)g(strings)e(in)i (one-to-one)f(correspondence)h(with)f(v)n(ariable)h(IDs)f(of)h(the)g (reading)55 3344 y(manager)-5 b(.)40 b(V)-11 b(ariables)28 b(in)g(the)g(DD)g(\002le)g(read)h(are)g(matched)f(with)f(manager)h(v)n (ariables)f(according)h(to)g(their)55 3465 y(name)35 b(\(a)h(not)f(NULL)g(v)n(arnames)g(parameter)h(w)o(as)f(required)h (while)f(storing)f(the)h(DD)g(\002le\).)64 b(The)35 b(most)55 3585 y(common)c(usage)h(of)g(this)f(feature)i(is)e(in)h(combination)e (with)i(a)g(v)n(ariable)g(ordering)g(stored)f(on)h(a)g(\002le)h(and)55 3706 y(based)28 b(on)h(v)n(ariables)f(names.)41 b(Names)29 b(must)e(be)i(loaded)f(in)g(an)h(array)g(of)g(strings)e(and)i(passed)f (to)g(the)h(DD)55 3826 y(load)24 b(procedure.)-44 4029 y Fk(\017)49 b Fl(v)n(armatchnode=DDDMP)p 1040 4029 V 35 w(V)-13 b(AR)p 1272 4029 V 35 w(MA)i(TCHIDS)25 b(has)g(a)g(meaning)f (similar)g(to)55 4150 y(DDDMP)p 421 4150 V 36 w(V)-13 b(AR)p 654 4150 V 35 w(MA)i(TCHN)m(AMES)26 b(b)n(ut)h(inte)o(ger)f (auxiliary)g(IDs)h(are)h(used)f(instead)f(of)h(strings.)36 b(The)28 b(ad-)55 4270 y(ditional)23 b(not)h(NULL)h(v)n(armathauxids)e (parameter)i(is)g(needed.)-44 4474 y Fk(\017)49 b Fl(v)n (armatchnode=DDDMP)p 1040 4474 V 35 w(V)-13 b(AR)p 1272 4474 V 35 w(COMPOSEIDS,)38 b(uses)f(the)f(additional)f(v)n (arcomposeids)g(parameter)55 4594 y(as)25 b(an)g(array)g(of)g(v)n (ariable)f(IDs)h(to)g(be)g(composed)f(with)g(IDs)g(stored)h(in)f (\002le.)-189 4860 y Fi(2.2.3)99 b(DD)25 b(Load/Stor)n(e)h(and)f(V)-9 b(ariable)25 b(Ordering)-189 5048 y Fl(Loading)31 b(of)i(Decision)e (Diagrams)h(from)g(\002le)g(supports)f(dif)n(ferent)h(v)n(ariables)g (ordering)f(strate)o(gies,)i(as)g(already)-189 5168 y(pointed)23 b(out)h(in)g(the)h(pre)n(vious)e(section.)30 b(This)24 b(allo)n(ws)f(or)h(e)o(xample)g(storing)f(dif)n(ferent)i(BDDs)f(each)h (with)f(its)g(o)n(wn)-189 5288 y(v)n(ariable)29 b(ordering,)h(and)g(to) f(mer)n(ge)h(them)f(within)f(the)i(same)f(DD)h(manager)f(by)h(means)f (of)g(proper)h(load)f(opera-)-189 5409 y(tions.)44 b(W)-8 b(e)30 b(suggest)f(using)f(DDDMP)p 1175 5409 V 36 w(V)-13 b(AR)p 1408 5409 V 36 w(MA)i(TCHIDS)30 b(whene)n(v)o(er)f(IDs)g(k)o (eeps)h(on)f(representing)h(the)f(same)-189 5529 y(entities)24 b(while)h(changing)f(v)n(ariable)h(ordering.)31 b(If)25 b(this)f(is)h(not)f(true,)h(v)n(ariable)g(names)g(\(if)g(a)n(v)n (ailable\))f(or)i(auxiliary)1794 5800 y(6)p eop %%Page: 7 7 7 6 bop -189 218 a Fl(IDs)34 b(are)h(a)g(good)e(w)o(ay)i(to)f (represent)g(in)l(v)n(ariant)f(attrib)n(uted)g(of)i(v)n(ariables)e (across)h(se)n(v)o(eral)g(runs)g(with)f(dif)n(ferent)-189 338 y(orderings.)50 b(DDDMP)p 629 338 30 4 v 35 w(V)-13 b(AR)p 861 338 V 36 w(COMPOSEIDS)32 b(is)f(an)h(alternati)n(v)o(e)e (solution,)h(that)g(practically)f(corresponds)h(to)-189 459 y(cascading)23 b(DDDMP)p 593 459 V 36 w(V)-13 b(AR)p 826 459 V 36 w(MA)i(TCHIDS)23 b(and)h(v)n(ariable)f(composition)e(with) h(a)i(gi)n(v)o(en)e(array)i(of)g(ne)n(w)f(v)n(ariables.)-189 797 y Fo(3)143 b(CNF)35 b(Support)-189 1050 y Fj(3.1)119 b(F)m(ormat)-189 1237 y Fl(Gi)n(v)o(en)30 b(a)h(BDD)g(representing)g(a) g(function)f Fd(f)11 b Fl(,)32 b(we)f(de)n(v)o(elop)f(three)h(basic)g (possible)e(w)o(ays)i(to)g(store)f(it)h(as)g(a)g(CNF)-189 1358 y(formula.)54 b(In)33 b(each)h(method)d(the)i(set)g(of)f(clauses)h (is)f(written)h(after)g(an)g(header)g(part.)55 b(Only)32 b(the)h(te)o(xt)f(format)g(is)-189 1478 y(allo)n(wed.)-189 1743 y Fi(3.1.1)99 b(Header)-189 1931 y Fl(The)23 b(header)h(part)f(of) g(each)h(CNF)g(\002le)f(has)g(basically)g(the)f(same)h(format)g (analyzed)g(for)h(the)f(BDD/ADD)g(\002les.)30 b(F)o(or)-189 2051 y(e)o(xample)h(the)g Fg(.rootids)f Fl(line)h(indicates)f(the)i(be) o(ginning)d(of)j(each)g(CNF)g(formula)f(represented)h(by)f(a)h(single) -189 2172 y(BDD.)j(T)-8 b(o)34 b(be)g(compatible)f(with)h(the)g(DIMA)l (CS)h(format)f(each)h(header)f(line)g(start)g(with)g(the)g(character)h (\223c\224)g(to)-189 2292 y(indicate)24 b(a)h(comment.)-189 2557 y Fi(3.1.2)99 b(T)-9 b(ext)25 b(F)n(ormat)-189 2745 y Fl(The)j(\002rst)g(method,)g(which)f(we)h(call)g Fi(Single-Node-Cut)p Fl(,)j(models)26 b(each)j(BDD)f(nodes,)h(b)n(ut)e(the)h(ones)f(with)h (both)-189 2865 y(the)c(children)g(equal)h(to)f(the)g(constant)g(node)g Fb(1)p Fl(,)g(as)h(a)g(multiple)o(x)o(er)-5 b(.)27 b(Each)e(multiple)o (x)o(er)d(has)i(tw)o(o)g(data)h(inputs)e(\(i.e.,)-189 2985 y(the)k(node)h(children\),)f(a)h(selection)f(input)f(\(i.e.,)i (the)g(node)f(v)n(ariable\))g(and)h(one)f(output)f(\(i.e.,)i(the)g (function)e(v)n(alue\))-189 3106 y(whose)h(v)n(alue)f(is)h(assigned)f (to)h(an)g(additional)f(CNF)i(v)n(ariable.)37 b(The)27 b(\002nal)h(number)e(of)h(v)n(ariables)g(is)f(equal)h(to)g(the)-189 3226 y(number)d(of)h(original)f(BDD)h(v)n(ariables)f(plus)g(the)h (number)f(of)h(\223internal\224)g(nodes)f(of)h(the)g(BDD.)47 3346 y(The)k(second)f(method,)g(which)h(we)f(call)h Fi(Maxterm-Cut)p Fl(,)h(create)g(clauses)e(starting)g(from)g Fd(f)39 b Fl(corresponds)-189 3467 y(to)25 b(the)h(of)n(f-set)g(\(i.e.,)f(all)h (the)g(paths-cubes)f(from)g(the)h(root)g(node)f(to)h(the)f(terminal)g Fg(0)p Fl(\))h(of)g(the)g(function)e Fd(f)11 b Fl(.)34 b(W)l(ithin)-189 3587 y(the)29 b(BDD)g(for)g Fd(f)11 b Fl(,)30 b(such)f(clauses)f(are)i(found)e(by)h(follo)n(wing)e(all)i (the)f(paths)h(from)f(the)h(root)g(node)f(of)h(the)g(BDD)g(to)-189 3708 y(the)c(constant)f(node)g Fb(0)p Fl(.)31 b(The)25 b(\002nal)g(number)f(of)h(v)n(ariables)f(is)g(equal)h(to)f(the)h (number)f(of)h(original)f(BDD)h(v)n(ariables.)47 3828 y(The)k(third)g(method,)g(which)g(we)g(call)g Fi(A)-5 b(uxiliary-V)c(ariable-Cut)p Fl(,)30 b(is)f(a)h(trade-of)n(f)f(between) g(the)g(\002rst)g(tw)o(o)-189 3948 y(strate)o(gies.)69 b(Internal)37 b(v)n(ariables,)j(i.e.,)h(cutting)c(points,)j(are)e (added)g(in)f(order)h(to)g(decompose)f(the)h(BDD)g(into)-189 4069 y(multiple)27 b(sub-trees)i(each)h(of)f(which)f(is)h(stored)g (follo)n(wing)e(the)h(second)h(strate)o(gy)-6 b(.)42 b(The)29 b(trade-of)n(f)g(is)g(guided)f(by)-189 4189 y(the)23 b(cutting)f(point)g(selection)g(strate)o(gy)-6 b(,)22 b(and)h(we)g(e)o(xperiment)f(with)g(tw)o(o)g(methodologies.)28 b(In)23 b(the)g(\002rst)g(method,)g(a)-189 4310 y(ne)n(w)f(CNF)h(v)n (ariable)f(is)f(inserted)h(in)g(correspondence)g(to)g(the)g(shared)g (nodes)g(of)g(the)h(BDD,)f(i.e.,)h(the)f(nodes)f(which)-189 4430 y(ha)n(v)o(e)29 b(more)g(than)h(one)f(incoming)f(edge.)45 b(This)29 b(technique,)h(albeit)e(optimizing)g(the)h(number)g(of)h (literals)e(stored,)-189 4550 y(can)35 b(produce)g(clauses)f(with)g(a)h (high)f(number)h(of)f(literals)1894 4514 y Fh(2)1933 4550 y Fl(.)60 b(T)-8 b(o)35 b(a)n(v)n(oid)f(this)g(dra)o(wback,)j(the) e(second)f(method,)-189 4671 y(introduces)28 b(all)g(the)g(pre)n (viously)e(indicated)i(cutting)f(points)g(more)h(the)h(ones)f (necessary)g(to)g(break)h(the)f(length)g(of)-189 4791 y(the)d(path)f(to)h(a)g(maximum)e(\(user\))i(selected)g(v)n(alue.)47 4911 y(Actually)-6 b(,)37 b(all)f(the)f(methods)g(described)h(abo)o(v)o (e)e(can)j(be)e(re-conducted)h(to)g(the)f(basic)h(idea)g(of)g(possibly) -189 5032 y(breaking)24 b(the)h(BDD)g(through)f(the)g(use)h(of)f (additional)g(cutting)f(v)n(ariables)h(and)h(dumping)e(the)h(paths)g (between)h(the)-189 5152 y(root)34 b(of)h(the)f(BDD,)h(the)g(cutting)e (v)n(ariables)h(and)g(the)h(terminal)e(nodes.)60 b(Such)35 b(internal)f(cutting)f(v)n(ariables)h(are)-189 5273 y(added)25 b(al)o(w)o(ays)f(\(for)i(each)f(node\),)g(ne)n(v)o(er)f(or)h(sometimes) e(respecti)n(v)o(ely)-6 b(.)p -189 5360 1607 4 v -77 5422 a Ff(2)-40 5452 y Fe(This)27 b(v)n(alue)f(is)i(superiorly)d (limited)h(by)g(the)h(number)e(of)h(v)n(ariables)g(of)g(the)h(BDD,)g (i.e.,)h(the)f(longest)f(path)g(from)g(the)h(root)f(to)g(the)-189 5551 y(terminal)19 b(node.)1794 5800 y Fl(7)p eop %%Page: 8 8 8 7 bop 47 218 a Fl(While)33 b(the)f Fc(Single-Node-Cut)h Fl(method)f(minimizes)f(the)i(length)f(of)h(the)f(clauses)h(produced,)i (b)n(ut)d(it)g(also)-189 338 y(requires)d(the)h(higher)f(number)g(of)g (CNF)i(v)n(ariables,)e(the)h Fc(Maxterm-Cut)f Fl(technique)g(minimizes) f(the)h(number)g(of)-189 459 y(CNF)36 b(v)n(ariables)d(required.)61 b(This)34 b(adv)n(antage)g(is)g(counter)n(-balanced)h(by)f(the)h(f)o (act)g(that)f(in)g(the)h(w)o(orst)f(case)h(the)-189 579 y(number)23 b(of)g(clauses,)g(as)h(well)e(as)i(the)f(total)f(number)h (of)g(literals,)g(produced)g(is)g(e)o(xponential)e(in)i(the)g(BDD)h (size)f(\(in)-189 699 y(terms)28 b(of)i(number)e(of)h(nodes\).)43 b(The)29 b(application)f(of)h(this)f(method)g(is)g(then)h(limited)e(to) i(the)g(cases)g(in)f(which)h(the)-189 820 y(\223of)n(f-set\224)c(of)f (the)g(represented)h(function)f Fd(f)35 b Fl(has)24 b(a)h(small)f (cardinality)-6 b(.)29 b(The)c Fc(A)n(uxiliary-V)-11 b(ariable-Cut)22 b Fl(strate)o(gy)h(is)-189 940 y(a)k(trade-of)n(f)h (between)f(the)g(\002rst)g(tw)o(o)g(methods)f(and)h(the)g(ones)f(which) h(gi)n(v)o(es)f(more)h(compact)f(results.)37 b(As)27 b(a)h(\002nal)-189 1061 y(remark)f(notice)e(that)h(the)g(method)g(is)f (able)i(to)f(store)g(both)f(monolithic)f(BDDs)j(and)f(conjuncti)n(v)o (e)e(forms.)35 b(In)26 b(each)-189 1181 y(case)f(we)g(generate)h(CNF)f (\002les)g(using)f(the)h(standard)f(DIMA)l(CS)i(format.)-189 1365 y Fi(Example)f(1)49 b Fc(F)l(igur)l(e)20 b(1)h(shows)f(an)h(e)n (xample)g(of)f(how)h(our)f(pr)l(ocedur)l(e)h(works)f(to)h(stor)l(e)f(a) h(small)f(monolithic)f(BDD.)-189 1486 y(F)l(igur)l(e)j(1\(a\))h(r)l (epr)l(esents)g(a)g(BDD)g(with)g Fb(4)g Fc(nodes.)30 b(BDD)23 b(variables)f(ar)l(e)h(named)g(after)f(inte)l(g)o(er)g(number) o(s)h(r)o(anging)-189 1606 y(fr)l(om)k Fb(1)h Fc(to)g Fb(4)p Fc(,)h(to)f(have)g(an)g(easy-to-follow)f(corr)l(espondence)h (with)g(the)g(CNF)h(variables.)40 b(F)l(igur)l(e)27 b(1\(b\),)i(\(c\))g (and)-189 1727 y(\(d\))c(show)g(the)f(corr)l(esponding)f(CNF)j(r)l(epr) l(esentations)d(g)o(ener)o(ated)h(by)h(our)f(thr)l(ee)h(methods.)30 b(As)24 b(in)h(the)f(standar)l(d)-189 1847 y(format)i Fa(p)i Fc(indicates)e(the)h(total)f(number)g(of)h(variables)f(used)h (\()p Fb(4)g Fc(is)g(the)g(minimum)f(value)h(as)g(the)g(BDD)g(itself)f (has)-189 1967 y Fb(4)f Fc(variables\),)e(and)i Fa(cnf)g Fc(the)f(total)g(number)g(of)h(clauses.)47 2088 y(As)i(a)g(\002nal)f(r) l(emark)h(notice)f(that)g(for)g(this)g(speci\002c)h(e)n(xample)g(the)f (\223Maxterm-Cut\224)i(appr)l(oac)o(h)d(is)h(the)h(one)-189 2208 y(whic)o(h)36 b(gives)g(the)g(most)f(compact)h(CNF)h(r)l(epr)l (esentation)e(b)n(ut)h(also)f(the)h(clause)g(with)g(the)g(lar)l(g)o (est)g(number)f(of)-189 2328 y(liter)o(als)23 b(\()p Fb(4)p Fc(\).)188 2471 y 6339814 10777681 0 0 11709153 19997655 startTexFig 188 2471 a %%BeginDocument: bdd.eps %!PS-Adobe-2.0 EPSF-2.0 %%Title: bdd.eps %%Creator: fig2dev Version 3.2 Patchlevel 3c %%CreationDate: Mon Sep 9 14:21:26 2002 %%For: quer@pcsq (Stefano Quer) %%BoundingBox: 0 0 178 304 %%Magnification: 1.0000 %%EndComments /$F2psDict 200 dict def $F2psDict begin $F2psDict /mtrx matrix put /col-1 {0 setgray} bind def /col0 {0.000 0.000 0.000 srgb} bind def /col1 {0.000 0.000 1.000 srgb} bind def /col2 {0.000 1.000 0.000 srgb} bind def /col3 {0.000 1.000 1.000 srgb} bind def /col4 {1.000 0.000 0.000 srgb} bind def /col5 {1.000 0.000 1.000 srgb} bind def /col6 {1.000 1.000 0.000 srgb} bind def /col7 {1.000 1.000 1.000 srgb} bind def /col8 {0.000 0.000 0.560 srgb} bind def /col9 {0.000 0.000 0.690 srgb} bind def /col10 {0.000 0.000 0.820 srgb} bind def /col11 {0.530 0.810 1.000 srgb} bind def /col12 {0.000 0.560 0.000 srgb} bind def /col13 {0.000 0.690 0.000 srgb} bind def /col14 {0.000 0.820 0.000 srgb} bind def /col15 {0.000 0.560 0.560 srgb} bind def /col16 {0.000 0.690 0.690 srgb} bind def /col17 {0.000 0.820 0.820 srgb} bind def /col18 {0.560 0.000 0.000 srgb} bind def /col19 {0.690 0.000 0.000 srgb} bind def /col20 {0.820 0.000 0.000 srgb} bind def /col21 {0.560 0.000 0.560 srgb} bind def /col22 {0.690 0.000 0.690 srgb} bind def /col23 {0.820 0.000 0.820 srgb} bind def /col24 {0.500 0.190 0.000 srgb} bind def /col25 {0.630 0.250 0.000 srgb} bind def /col26 {0.750 0.380 0.000 srgb} bind def /col27 {1.000 0.500 0.500 srgb} bind def /col28 {1.000 0.630 0.630 srgb} bind def /col29 {1.000 0.750 0.750 srgb} bind def /col30 {1.000 0.880 0.880 srgb} bind def /col31 {1.000 0.840 0.000 srgb} bind def end save newpath 0 304 moveto 0 0 lineto 178 0 lineto 178 304 lineto closepath clip newpath -51.0 319.0 translate 1 -1 scale /cp {closepath} bind def /ef {eofill} bind def /gr {grestore} bind def /gs {gsave} bind def /sa {save} bind def /rs {restore} bind def /l {lineto} bind def /m {moveto} bind def /rm {rmoveto} bind def /n {newpath} bind def /s {stroke} bind def /sh {show} bind def /slc {setlinecap} bind def /slj {setlinejoin} bind def /slw {setlinewidth} bind def /srgb {setrgbcolor} bind def /rot {rotate} bind def /sc {scale} bind def /sd {setdash} bind def /ff {findfont} bind def /sf {setfont} bind def /scf {scalefont} bind def /sw {stringwidth} bind def /tr {translate} bind def /tnt {dup dup currentrgbcolor 4 -2 roll dup 1 exch sub 3 -1 roll mul add 4 -2 roll dup 1 exch sub 3 -1 roll mul add 4 -2 roll dup 1 exch sub 3 -1 roll mul add srgb} bind def /shd {dup dup currentrgbcolor 4 -2 roll mul 4 -2 roll mul 4 -2 roll mul srgb} bind def /DrawEllipse { /endangle exch def /startangle exch def /yrad exch def /xrad exch def /y exch def /x exch def /savematrix mtrx currentmatrix def x y tr xrad yrad sc 0 0 1 startangle endangle arc closepath savematrix setmatrix } def /$F2psBegin {$F2psDict begin /$F2psEnteredState save def} def /$F2psEnd {$F2psEnteredState restore end} def $F2psBegin %%Page: 1 1 10 setmiterlimit 0.06299 0.06299 sc % % Fig objects follow % % Polyline 15.000 slw n 2010 4515 m 2550 4515 l 2550 5040 l 2010 5040 l cp gs col0 s gr /Times-Roman ff 300.00 scf sf 2205 4875 m gs 1 -1 sc (1) col0 sh gr % Ellipse n 1515 1800 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 2250 900 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 2970 2715 270 270 0 360 DrawEllipse gs col0 s gr % Ellipse n 2280 3705 270 270 0 360 DrawEllipse gs col0 s gr 7.500 slw % Ellipse n 3555 3555 64 64 0 360 DrawEllipse gs 0.00 setgray ef gr gs col0 s gr % Ellipse n 2712 1726 64 64 0 360 DrawEllipse gs 0.00 setgray ef gr gs col0 s gr % Ellipse n 2430 4230 64 64 0 360 DrawEllipse gs 0.00 setgray ef gr gs col0 s gr % Polyline 15.000 slw n 2805 2910 m 2250 3450 l gs col0 s gr % Polyline [90] 0 sd gs clippath 2940 2472 m 3010 2445 l 2931 2239 l 2957 2411 l 2861 2266 l cp eoclip n 2460 1110 m 2970 2445 l gs col0 s gr gr [] 0 sd % arrowhead n 2861 2266 m 2957 2411 l 2931 2239 l 2908 2284 l 2861 2266 l cp gs 0.00 setgray ef gr col0 s % Polyline gs clippath 1478 1511 m 1528 1568 l 1693 1422 l 1542 1506 l 1643 1366 l cp eoclip n 2025 1080 m 1515 1530 l gs col0 s gr gr % arrowhead n 1643 1366 m 1542 1506 l 1693 1422 l 1643 1416 l 1643 1366 l cp gs 0.00 setgray ef gr col0 s % Polyline gs clippath 2212 645 m 2287 645 l 2287 425 l 2250 594 l 2212 425 l cp eoclip n 2250 270 m 2250 630 l gs col0 s gr gr % arrowhead n 2212 425 m 2250 594 l 2287 425 l 2250 459 l 2212 425 l cp gs 0.00 setgray ef gr col0 s % Polyline [90] 0 sd gs clippath 2692 2664 m 2732 2601 l 2546 2485 l 2670 2606 l 2506 2548 l cp eoclip n 1710 2010 m 2700 2625 l gs col0 s gr gr [] 0 sd % arrowhead n 2506 2548 m 2670 2606 l 2546 2485 l 2555 2534 l 2506 2548 l cp gs 0.00 setgray ef gr col0 s % Polyline 2 slj [90] 0 sd gs clippath 2504 4653 m 2539 4720 l 2733 4616 l 2567 4663 l 2698 4550 l cp eoclip n 3180 2910 m 3181 2911 l 3183 2913 l 3186 2916 l 3192 2921 l 3200 2929 l 3210 2939 l 3223 2951 l 3238 2966 l 3255 2984 l 3274 3003 l 3295 3025 l 3317 3049 l 3339 3075 l 3362 3103 l 3385 3131 l 3407 3161 l 3429 3192 l 3450 3225 l 3470 3258 l 3488 3293 l 3504 3329 l 3519 3367 l 3531 3406 l 3541 3447 l 3548 3490 l 3552 3536 l 3552 3583 l 3548 3634 l 3540 3686 l 3528 3740 l 3510 3795 l 3490 3844 l 3467 3892 l 3441 3939 l 3413 3985 l 3382 4028 l 3350 4070 l 3317 4110 l 3283 4148 l 3248 4184 l 3211 4219 l 3174 4253 l 3136 4285 l 3098 4316 l 3059 4347 l 3020 4376 l 2980 4405 l 2941 4432 l 2901 4459 l 2862 4484 l 2824 4509 l 2787 4532 l 2751 4554 l 2717 4575 l 2686 4593 l 2657 4610 l 2631 4626 l 2608 4639 l 2589 4650 l 2572 4659 l 2559 4666 l 2550 4672 l 2535 4680 l gs col0 s gr gr [] 0 sd % arrowhead 0 slj n 2698 4550 m 2567 4663 l 2733 4616 l 2686 4599 l 2698 4550 l cp gs 0.00 setgray ef gr col0 s % Polyline 2 slj gs clippath 1985 4734 m 2028 4672 l 1847 4548 l 1965 4675 l 1804 4609 l cp eoclip n 1350 2025 m 1349 2026 l 1348 2027 l 1345 2030 l 1340 2035 l 1334 2042 l 1325 2051 l 1314 2063 l 1301 2078 l 1286 2095 l 1268 2114 l 1249 2137 l 1227 2161 l 1205 2188 l 1181 2218 l 1156 2249 l 1131 2282 l 1105 2316 l 1080 2352 l 1054 2390 l 1029 2428 l 1005 2468 l 981 2509 l 959 2552 l 938 2595 l 918 2640 l 900 2687 l 884 2736 l 870 2786 l 858 2839 l 848 2894 l 841 2951 l 837 3011 l 836 3074 l 838 3139 l 845 3206 l 855 3275 l 870 3345 l 888 3412 l 910 3477 l 934 3542 l 961 3604 l 990 3665 l 1022 3723 l 1054 3779 l 1088 3833 l 1124 3885 l 1160 3935 l 1198 3983 l 1236 4029 l 1275 4074 l 1315 4118 l 1356 4160 l 1397 4201 l 1438 4241 l 1480 4280 l 1522 4318 l 1563 4355 l 1605 4390 l 1645 4424 l 1685 4457 l 1723 4488 l 1760 4517 l 1795 4545 l 1827 4570 l 1857 4593 l 1884 4613 l 1909 4632 l 1930 4647 l 1947 4660 l 1962 4671 l 1973 4679 l 1982 4686 l 1995 4695 l gs col0 s gr gr % arrowhead 0 slj n 1804 4609 m 1965 4675 l 1847 4548 l 1854 4598 l 1804 4609 l cp gs 0.00 setgray ef gr col0 s % Polyline 2 slj [90] 0 sd gs clippath 2300 4492 m 2363 4532 l 2481 4347 l 2359 4470 l 2417 4307 l cp eoclip n 2340 3960 m 2341 3962 l 2344 3966 l 2348 3973 l 2354 3982 l 2362 3995 l 2370 4010 l 2379 4028 l 2389 4046 l 2397 4066 l 2406 4088 l 2413 4111 l 2420 4137 l 2425 4165 l 2429 4197 l 2430 4230 l 2429 4263 l 2425 4295 l 2420 4323 l 2413 4349 l 2406 4372 l 2397 4394 l 2389 4414 l 2379 4433 l 2370 4450 l 2362 4465 l 2354 4478 l 2340 4500 l gs col0 s gr gr [] 0 sd % arrowhead 0 slj n 2417 4307 m 2359 4470 l 2481 4347 l 2431 4356 l 2417 4307 l cp gs 0.00 setgray ef gr col0 s % Polyline 2 slj gs clippath 2136 4532 m 2199 4492 l 2082 4307 l 2141 4470 l 2018 4347 l cp eoclip n 2160 3960 m 2159 3962 l 2156 3966 l 2152 3973 l 2146 3982 l 2138 3995 l 2130 4010 l 2121 4028 l 2111 4046 l 2103 4066 l 2094 4088 l 2087 4111 l 2080 4137 l 2075 4165 l 2071 4197 l 2070 4230 l 2071 4263 l 2075 4295 l 2080 4323 l 2087 4349 l 2094 4372 l 2103 4394 l 2111 4414 l 2121 4433 l 2130 4450 l 2138 4465 l 2146 4478 l 2160 4500 l gs col0 s gr gr % arrowhead 0 slj n 2018 4347 m 2141 4470 l 2082 4307 l 2068 4356 l 2018 4347 l cp gs 0.00 setgray ef gr col0 s /Times-Roman ff 300.00 scf sf 2175 990 m gs 1 -1 sc (1) col0 sh gr /Times-Roman ff 300.00 scf sf 1440 1890 m gs 1 -1 sc (2) col0 sh gr /Times-Roman ff 300.00 scf sf 2895 2805 m gs 1 -1 sc (3) col0 sh gr /Times-Roman ff 300.00 scf sf 2205 3795 m gs 1 -1 sc (4) col0 sh gr $F2psEnd rs %%EndDocument endTexFig 531 3990 a Fc(\(a\))1512 2504 y Fg(p)60 b(cnf)f(7)g(11)1512 2624 y(-5)g(3)h(0)1512 2745 y(-5)f(4)h(0)1512 2865 y(5)g(-3)f(-4)g(0) 1512 2985 y(6)h(-2)f(0)1512 3106 y(6)h(-5)f(0)1512 3226 y(-6)g(2)h(5)f(0)1512 3347 y(7)h(1)f(5)h(0)1512 3467 y(-7)f(1)h(-5)f(0)1512 3587 y(7)h(-1)f(-6)g(0)1512 3708 y(-7)g(-1)h(6)f(0)1512 3828 y(7)h(0)1836 3990 y Fc(\(b\))2541 2525 y Fg(p)f(cnf)g(4)h(3)2541 2645 y(1)f(-3)h(-4)f(0)2541 2766 y(-1)g(2)h(3)f(0)2541 2886 y(-1)g(2)h(-3)f(4)h(0)2868 3048 y Fc(\(c\))2541 3251 y Fg(p)f(cnf)g(5)h(5)2541 3371 y(-5)f(1)h(0)2541 3492 y(5)f(-1)h(2)f(0)2541 3612 y(-3)g(-4)g(5)h(0) 2541 3733 y(3)f(-5)h(0)2541 3853 y(-3)f(4)h(-5)f(0)2865 3990 y Fc(\(d\))-189 4138 y Fl(Figure)46 b(1:)71 b(\(a\))47 b(BDD;)e(\(b\))h(\223Single-Node-Cut\224)g(format;)55 b(\(c\))46 b(\223Maxterm-Cut\224)g(format;)55 b(\(d\))45 b(\223)-8 b(Auxiliary-)-189 4258 y(V)d(ariable-Cut\224)25 b(F)o(ormat.)-189 4625 y Fj(3.2)119 b(Implementation)-189 4813 y Fl(Store)25 b(and)g(Load)g(for)g(a)g(single)f(BDD)h(or)g(a)g (forest)g(of)g(BDDs)g(is)f(currently)h(implemented.)-189 5073 y Fi(3.2.1)99 b(Storing)25 b(Decision)g(Diagrams)f(as)g(CNF)h(F)n (ormulas)-189 5260 y Fl(As)g(f)o(ar)g(as)g(the)g(storing)e(process)i (is)f(concerned)i(three)f(possible)e(formats)h(are)i(a)n(v)n(ailable:) -44 5431 y Fk(\017)49 b Fl(DDDMP)p 421 5431 30 4 v 36 w(CNF)p 650 5431 V 36 w(MODE)p 980 5431 V 35 w(NODE:)21 b(store)f(a)h(BDD)h(by)e(introducing)f(an)i(auxiliary)g(v)n(ariable)f (for)h(each)g(BDD)55 5551 y(node)1794 5800 y(8)p eop %%Page: 9 9 9 8 bop -44 218 a Fk(\017)49 b Fl(DDDMP)p 421 218 30 4 v 36 w(CNF)p 650 218 V 36 w(MODE)p 980 218 V 35 w(MAXTERM:)20 b(store)g(a)h(BDD)h(by)e(follo)n(wing)f(the)h(maxterm)g(of)h(the)g (represented)55 338 y(function)-44 542 y Fk(\017)49 b Fl(DDDMP)p 421 542 V 36 w(CNF)p 650 542 V 36 w(MODE)p 980 542 V 35 w(BEST)-5 b(:)32 b(trade-of)f(between)h(the)f(tw)o(o)f (pre)n(vious)g(solution,)h(trying)f(to)h(optimize)55 662 y(the)25 b(number)f(of)h(literals)f(stored.)-189 865 y(See)c(procedures)f(Dddmp)p 736 865 V 35 w(cuddBddStoreCnf)g(\(to) g(store)f(a)h(single)f(BDD)i(as)e(a)i(CNF)f(formula\))g(and)g(Dddmp)p 3609 865 V 34 w(cuddBddArrayStoreCnf)-189 986 y(\(to)25 b(store)f(an)h(array)h(of)f(BDDs)g(as)f(a)i(CNF)f(formula\).)-189 1252 y Fi(3.2.2)99 b(Loadinf)26 b(CNF)e(F)n(ormulas)g(as)h(BDDs)-189 1439 y Fl(As)g(f)o(ar)g(as)g(the)g(loading)e(process)i(is)f(concerned)i (three)f(possible)e(formats)i(are)g(a)n(v)n(ailable:)-44 1643 y Fk(\017)49 b Fl(DDDMP)p 421 1643 V 36 w(CNF)p 650 1643 V 36 w(MODE)p 980 1643 V 35 w(NO)p 1159 1643 V 36 w(CONJ:)25 b(Return)g(the)f(Clauses)h(without)f(Conjunction)-44 1846 y Fk(\017)49 b Fl(DDDMP)p 421 1846 V 36 w(CNF)p 650 1846 V 36 w(MODE)p 980 1846 V 35 w(NO)p 1159 1846 V 36 w(Q)o(U)l(ANT)-5 b(:)24 b(Return)h(the)g(sets)f(of)h(BDDs)g (without)f(Quanti\002cation)-44 2050 y Fk(\017)49 b Fl(DDDMP)p 421 2050 V 36 w(CNF)p 650 2050 V 36 w(MODE)p 980 2050 V 35 w(CONJ)p 1264 2050 V 36 w(Q)o(U)l(ANT)-5 b(:)23 b(Return)h(the)g(sets)f(of)h(BDDs)g(AFTER)g(Existential)e(Quanti\002-) 55 2170 y(cation)-189 2373 y(See)e(procedures)f(Dddmp)p 736 2373 V 35 w(cuddBddLoadCnf)f(\(to)h(load)f(a)i(CNF)f(formula)g(as)g (a)g(single)f(BDD\))h(and)g(Dddmp)p 3581 2373 V 35 w (cuddBddArrayLoadCnf)-189 2494 y(\(to)35 b(load)h(a)g(CNF)g(formula)f (as)h(an)g(array)g(of)g(BDDs\).)63 b(See)36 b(also)g(Dddmp)p 2485 2494 V 34 w(cuddHeaderLoadCnf)h(to)e(load)g(the)-189 2614 y(header)25 b(of)g(a)g(CNF)h(\002le)f(to)g(gather)f(information)f (on)i(the)g(sa)n(v)o(ed)f(structure.)-189 2954 y Fo(4)143 b(T)-13 b(est)35 b(Pr)m(ogram)f(and)h(Regr)m(ession)f(T)-13 b(ests)-189 3177 y Fl(The)20 b Fc(testddmp.c)e Fl(\002le,)j(pro)o (vided)d(with)h(this)f(distrib)n(ution,)g(e)o(x)o(empli\002es)g(some)h (of)h(the)f(abo)o(v)o(e)g(features.)29 b(Moreo)o(v)o(er)l(,)-189 3298 y(in)d(the)h Fc(e)n(xp)g Fl(e)o(xperiments)e(a)j(fe)n(w)e (scripts,)h(named)f Fc(test\241n\277.script)f Fl(are)i(a)n(v)n(ailable) f(for)h(a)g(sanity)f(check)h(of)g(the)g(tool)-189 3418 y(and)e(to)f(tak)o(e)h(a)g(look)f(at)h(some)f(runs)h(e)o(x)o (empli\002cation.)-189 3758 y Fo(5)143 b(Documentation)-189 3981 y Fl(F)o(or)27 b(further)f(documentation)f(on)i(the)f(package)h (see)g(the)g(on-line)f(documentation)f(automatically)g(created)i(from) -189 4102 y(the)e(source)g(code)g(\002les.)-189 4441 y Fo(6)143 b(Ackno)o(wledgments)-189 4665 y Fl(W)-8 b(e)19 b(are)h(particular)f(indebted)f(with)g(F)o(abio)g(Somenzi,)i(for)f (discussions,)f(advice,)i(and)f(for)g(including)e(the)i(DDDMP)-189 4785 y(package)28 b(into)f(the)h(CUDD)g(distrib)n(ution.)37 b(W)-8 b(e)29 b(also)e(thank)g(all)h(the)g(user)g(of)g(the)f(package)i (for)f(their)f(useful)h(indi-)-189 4905 y(cation)c(and)h(comments)f(on) g(the)h(it.)1794 5800 y(9)p eop %%Page: 10 10 10 9 bop -189 218 a Fo(7)143 b(FTP)35 b(Site)-189 441 y Fl(The)25 b(package)g(is)f(singularly)g(a)n(v)n(ailable)g(from:)-189 645 y Fg(site:)59 b(ftp.polito.it)-189 765 y(user:)g(anonymous)-189 885 y(directory:)f(/pub/research/dddmp)-189 1089 y Fl(or)25 b(directly)f(from)h(the)f(author)h(WEB)g(pages:)-189 1292 y Fg(WWW:)59 b(http://www.polito.it/\230{cabodi)o(,quer)o(})-189 1632 y Fo(8)143 b(F)l(eedback)-189 1855 y Fl(Send)25 b(feedback)h(to:)-189 2059 y Fg(Gianpiero)58 b(Cabodi)g(&)i(Stefano)e (Quer)-189 2179 y(Politecnico)f(di)j(Torino)-189 2300 y(Dipartimento)d(di)i(Automatica)f(e)i(Informatica)-189 2420 y(Corso)f(Duca)g(degli)f(Abruzzi,)g(24)-189 2540 y(I-10129)g(Torino)-189 2661 y(Italy)-189 2781 y(E-mail:)g ({cabodi,quer}@polito.it)-189 2901 y(WWW:)h (http://www.polito.it/\230{cabodi)o(,quer)o(})1769 5800 y Fl(10)p eop %%Trailer end userdict /end-hook known{end-hook}if %%EOF