2 %%Creator: dvips(k) 5.86 Copyright 1999 Radical Eye Software
6 %%BoundingBox: 0 0 596 842
7 %%DocumentFonts: Times-Bold Times-Roman Courier Times-Italic Helvetica
8 %%DocumentPaperSizes: a4
10 %DVIPSWebPage: (www.radicaleye.com)
11 %DVIPSCommandLine: dvips -t a4 -f dddmp-2.0
12 %DVIPSParameters: dpi=600, compressed
13 %DVIPSSource: TeX output 2002.12.11:0557
14 %%BeginProcSet: texc.pro
16 /TeXDict 300 dict def TeXDict begin/N{def}def/B{bind def}N/S{exch}N/X{S
17 N}B/A{dup}B/TR{translate}N/isls false N/vsize 11 72 mul N/hsize 8.5 72
18 mul N/landplus90{false}def/@rigin{isls{[0 landplus90{1 -1}{-1 1}ifelse 0
19 0 0]concat}if 72 Resolution div 72 VResolution div neg scale isls{
20 landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div hsize
21 mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul TR[
22 matrix currentmatrix{A A round sub abs 0.00001 lt{round}if}forall round
23 exch round exch]setmatrix}N/@landscape{/isls true N}B/@manualfeed{
24 statusdict/manualfeed true put}B/@copies{/#copies X}B/FMat[1 0 0 -1 0 0]
25 N/FBB[0 0 0 0]N/nn 0 N/IEn 0 N/ctr 0 N/df-tail{/nn 8 dict N nn begin
26 /FontType 3 N/FontMatrix fntrx N/FontBBox FBB N string/base X array
27 /BitMaps X/BuildChar{CharBuilder}N/Encoding IEn N end A{/foo setfont}2
28 array copy cvx N load 0 nn put/ctr 0 N[}B/sf 0 N/df{/sf 1 N/fntrx FMat N
29 df-tail}B/dfs{div/sf X/fntrx[sf 0 0 sf neg 0 0]N df-tail}B/E{pop nn A
30 definefont setfont}B/Cw{Cd A length 5 sub get}B/Ch{Cd A length 4 sub get
31 }B/Cx{128 Cd A length 3 sub get sub}B/Cy{Cd A length 2 sub get 127 sub}
32 B/Cdx{Cd A length 1 sub get}B/Ci{Cd A type/stringtype ne{ctr get/ctr ctr
33 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
34 1 roll S A/base get 2 index get S/BitMaps get S get/Cd X pop/ctr 0 N Cdx
35 0 Cx Cy Ch sub Cx Cw add Cy setcachedevice Cw Ch true[1 0 0 -1 -.1 Cx
36 sub Cy .1 sub]/id Ci N/rw Cw 7 add 8 idiv string N/rc 0 N/gp 0 N/cp 0 N{
37 rc 0 ne{rc 1 sub/rc X rw}{G}ifelse}imagemask restore}B/G{{id gp get/gp
38 gp 1 add N A 18 mod S 18 idiv pl S get exec}loop}B/adv{cp add/cp X}B
39 /chg{rw cp id gp 4 index getinterval putinterval A gp add/gp X adv}B/nd{
40 /cp 0 N rw exit}B/lsh{rw cp 2 copy get A 0 eq{pop 1}{A 255 eq{pop 254}{
41 A A add 255 and S 1 and or}ifelse}ifelse put 1 adv}B/rsh{rw cp 2 copy
42 get A 0 eq{pop 128}{A 255 eq{pop 127}{A 2 idiv S 128 and or}ifelse}
43 ifelse put 1 adv}B/clr{rw cp 2 index string putinterval adv}B/set{rw cp
44 fillstr 0 4 index getinterval putinterval adv}B/fillstr 18 string 0 1 17
45 {2 copy 255 put pop}for N/pl[{adv 1 chg}{adv 1 chg nd}{1 add chg}{1 add
46 chg nd}{adv lsh}{adv lsh nd}{adv rsh}{adv rsh nd}{1 add adv}{/rc X nd}{
47 1 add set}{1 add clr}{adv 2 chg}{adv 2 chg nd}{pop nd}]A{bind pop}
48 forall N/D{/cc X A type/stringtype ne{]}if nn/base get cc ctr put nn
49 /BitMaps get S ctr S sf 1 ne{A A length 1 sub A 2 index S get sf div put
50 }if put/ctr ctr 1 add N}B/I{cc 1 add D}B/bop{userdict/bop-hook known{
51 bop-hook}if/SI save N @rigin 0 0 moveto/V matrix currentmatrix A 1 get A
52 mul exch 0 get A mul add .99 lt{/QV}{/RV}ifelse load def pop pop}N/eop{
53 SI restore userdict/eop-hook known{eop-hook}if showpage}N/@start{
54 userdict/start-hook known{start-hook}if pop/VResolution X/Resolution X
55 1000 div/DVImag X/IEn 256 array N 2 string 0 1 255{IEn S A 360 add 36 4
56 index cvrs cvn put}for pop 65781.76 div/vsize X 65781.76 div/hsize X}N
57 /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{
58 /Ry X/Rx X V}B statusdict begin/product where{pop false[(Display)(NeXT)
59 (LaserWriter 16/600)]{A length product length le{A length product exch 0
60 exch getinterval eq{pop true exit}if}{pop}ifelse}forall}{false}ifelse
61 end{{gsave TR -.1 .1 TR 1 1 scale Rx Ry false RMat{BDot}imagemask
62 grestore}}{{gsave TR -.1 .1 TR Rx Ry scale 1 1 false RMat{BDot}
63 imagemask grestore}}ifelse B/QV{gsave newpath transform round exch round
64 exch itransform moveto Rx 0 rlineto 0 Ry neg rlineto Rx neg 0 rlineto
65 fill grestore}B/a{moveto}B/delta 0 N/tail{A/delta X 0 rmoveto}B/M{S p
66 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}
67 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{
68 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
69 rmoveto}B/y{3 2 roll p a}B/bos{/SS save N}B/eos{SS restore}B end
72 %%BeginProcSet: 8r.enc
74 % author = "S. Rahtz, P. MacKay, Alan Jeffrey, B. Horn, K. Berry",
76 % date = "22 June 1996",
77 % filename = "8r.enc",
78 % email = "kb@@mail.tug.org",
79 % address = "135 Center Hill Rd. // Plymouth, MA 02360",
80 % codetable = "ISO/ASCII",
81 % checksum = "119 662 4424",
82 % docstring = "Encoding for TrueType or Type 1 fonts to be used with TeX."
85 % Idea is to have all the characters normally included in Type 1 fonts
86 % available for typesetting. This is effectively the characters in Adobe
87 % Standard Encoding + ISO Latin 1 + extra characters from Lucida.
89 % Character code assignments were made as follows:
91 % (1) the Windows ANSI characters are almost all in their Windows ANSI
92 % positions, because some Windows users cannot easily reencode the
93 % fonts, and it makes no difference on other systems. The only Windows
94 % ANSI characters not available are those that make no sense for
95 % typesetting -- rubout (127 decimal), nobreakspace (160), softhyphen
96 % (173). quotesingle and grave are moved just because it's such an
97 % irritation not having them in TeX positions.
99 % (2) Remaining characters are assigned arbitrarily to the lower part
100 % of the range, avoiding 0, 10 and 13 in case we meet dumb software.
102 % (3) Y&Y Lucida Bright includes some extra text characters; in the
103 % hopes that other PostScript fonts, perhaps created for public
104 % consumption, will include them, they are included starting at 0x12.
106 % (4) Remaining positions left undefined are for use in (hopefully)
107 % upward-compatible revisions, if someday more characters are generally
110 % (5) hyphen appears twice for compatibility with both ASCII and Windows.
113 % 0x00 (encoded characters from Adobe Standard not in Windows 3.1)
114 /.notdef /dotaccent /fi /fl
115 /fraction /hungarumlaut /Lslash /lslash
116 /ogonek /ring /.notdef
117 /breve /minus /.notdef
118 % These are the only two remaining unencoded characters, so may as
123 % (unusual TeX characters available in, e.g., Lucida Bright)
124 /dotlessj /ff /ffi /ffl
125 /.notdef /.notdef /.notdef /.notdef
126 /.notdef /.notdef /.notdef /.notdef
127 % very contentious; it's so painful not having quoteleft and quoteright
128 % at 96 and 145 that we move the things normally found there down to here.
130 % 0x20 (ASCII begins)
131 /space /exclam /quotedbl /numbersign
132 /dollar /percent /ampersand /quoteright
133 /parenleft /parenright /asterisk /plus /comma /hyphen /period /slash
135 /zero /one /two /three /four /five /six /seven
136 /eight /nine /colon /semicolon /less /equal /greater /question
138 /at /A /B /C /D /E /F /G /H /I /J /K /L /M /N /O
140 /P /Q /R /S /T /U /V /W
141 /X /Y /Z /bracketleft /backslash /bracketright /asciicircum /underscore
143 /quoteleft /a /b /c /d /e /f /g /h /i /j /k /l /m /n /o
145 /p /q /r /s /t /u /v /w
146 /x /y /z /braceleft /bar /braceright /asciitilde
147 /.notdef % rubout; ASCII ends
149 /.notdef /.notdef /quotesinglbase /florin
150 /quotedblbase /ellipsis /dagger /daggerdbl
151 /circumflex /perthousand /Scaron /guilsinglleft
152 /OE /.notdef /.notdef /.notdef
154 /.notdef /.notdef /.notdef /quotedblleft
155 /quotedblright /bullet /endash /emdash
156 /tilde /trademark /scaron /guilsinglright
157 /oe /.notdef /.notdef /Ydieresis
159 /.notdef % nobreakspace
160 /exclamdown /cent /sterling
161 /currency /yen /brokenbar /section
162 /dieresis /copyright /ordfeminine /guillemotleft
164 /hyphen % Y&Y (also at 45); Windows' softhyphen
168 /degree /plusminus /twosuperior /threesuperior
169 /acute /mu /paragraph /periodcentered
170 /cedilla /onesuperior /ordmasculine /guillemotright
171 /onequarter /onehalf /threequarters /questiondown
173 /Agrave /Aacute /Acircumflex /Atilde /Adieresis /Aring /AE /Ccedilla
174 /Egrave /Eacute /Ecircumflex /Edieresis
175 /Igrave /Iacute /Icircumflex /Idieresis
177 /Eth /Ntilde /Ograve /Oacute
178 /Ocircumflex /Otilde /Odieresis /multiply
179 /Oslash /Ugrave /Uacute /Ucircumflex
180 /Udieresis /Yacute /Thorn /germandbls
182 /agrave /aacute /acircumflex /atilde
183 /adieresis /aring /ae /ccedilla
184 /egrave /eacute /ecircumflex /edieresis
185 /igrave /iacute /icircumflex /idieresis
187 /eth /ntilde /ograve /oacute
188 /ocircumflex /otilde /odieresis /divide
189 /oslash /ugrave /uacute /ucircumflex
190 /udieresis /yacute /thorn /ydieresis
194 %%BeginProcSet: texps.pro
196 TeXDict begin/rf{findfont dup length 1 add dict begin{1 index/FID ne 2
197 index/UniqueID ne and{def}{pop pop}ifelse}forall[1 index 0 6 -1 roll
198 exec 0 exch 5 -1 roll VResolution Resolution div mul neg 0 0]/Metrics
199 exch def dict begin Encoding{exch dup type/integertype ne{pop pop 1 sub
200 dup 0 le{pop}{[}ifelse}{FontMatrix 0 get div Metrics 0 get div def}
201 ifelse}forall Metrics/Metrics currentdict end def[2 index currentdict
202 end definefont 3 -1 roll makefont/setfont cvx]cvx def}def/ObliqueSlant{
203 dup sin S cos div neg}B/SlantFont{4 index mul add}def/ExtendFont{3 -1
204 roll mul exch}def/ReEncodeFont{CharStrings rcheck{/Encoding false def
205 dup[exch{dup CharStrings exch known not{pop/.notdef/Encoding true def}
206 if}forall Encoding{]exch pop}{cleartomark}ifelse}if/Encoding exch def}
210 %%BeginProcSet: special.pro
212 TeXDict begin/SDict 200 dict N SDict begin/@SpecialDefaults{/hs 612 N
213 /vs 792 N/ho 0 N/vo 0 N/hsc 1 N/vsc 1 N/ang 0 N/CLIP 0 N/rwiSeen false N
214 /rhiSeen false N/letter{}N/note{}N/a4{}N/legal{}N}B/@scaleunit 100 N
215 /@hscale{@scaleunit div/hsc X}B/@vscale{@scaleunit div/vsc X}B/@hsize{
216 /hs X/CLIP 1 N}B/@vsize{/vs X/CLIP 1 N}B/@clip{/CLIP 2 N}B/@hoffset{/ho
217 X}B/@voffset{/vo X}B/@angle{/ang X}B/@rwi{10 div/rwi X/rwiSeen true N}B
218 /@rhi{10 div/rhi X/rhiSeen true N}B/@llx{/llx X}B/@lly{/lly X}B/@urx{
219 /urx X}B/@ury{/ury X}B/magscale true def end/@MacSetUp{userdict/md known
220 {userdict/md get type/dicttype eq{userdict begin md length 10 add md
221 maxlength ge{/md md dup length 20 add dict copy def}if end md begin
222 /letter{}N/note{}N/legal{}N/od{txpose 1 0 mtx defaultmatrix dtransform S
223 atan/pa X newpath clippath mark{transform{itransform moveto}}{transform{
224 itransform lineto}}{6 -2 roll transform 6 -2 roll transform 6 -2 roll
225 transform{itransform 6 2 roll itransform 6 2 roll itransform 6 2 roll
226 curveto}}{{closepath}}pathforall newpath counttomark array astore/gc xdf
227 pop ct 39 0 put 10 fz 0 fs 2 F/|______Courier fnt invertflag{PaintBlack}
228 if}N/txpose{pxs pys scale ppr aload pop por{noflips{pop S neg S TR pop 1
229 -1 scale}if xflip yflip and{pop S neg S TR 180 rotate 1 -1 scale ppr 3
230 get ppr 1 get neg sub neg ppr 2 get ppr 0 get neg sub neg TR}if xflip
231 yflip not and{pop S neg S TR pop 180 rotate ppr 3 get ppr 1 get neg sub
232 neg 0 TR}if yflip xflip not and{ppr 1 get neg ppr 0 get neg TR}if}{
233 noflips{TR pop pop 270 rotate 1 -1 scale}if xflip yflip and{TR pop pop
234 90 rotate 1 -1 scale ppr 3 get ppr 1 get neg sub neg ppr 2 get ppr 0 get
235 neg sub neg TR}if xflip yflip not and{TR pop pop 90 rotate ppr 3 get ppr
236 1 get neg sub neg 0 TR}if yflip xflip not and{TR pop pop 270 rotate ppr
237 2 get ppr 0 get neg sub neg 0 S TR}if}ifelse scaleby96{ppr aload pop 4
238 -1 roll add 2 div 3 1 roll add 2 div 2 copy TR .96 dup scale neg S neg S
239 TR}if}N/cp{pop pop showpage pm restore}N end}if}if}N/normalscale{
240 Resolution 72 div VResolution 72 div neg scale magscale{DVImag dup scale
241 }if 0 setgray}N/psfts{S 65781.76 div N}N/startTexFig{/psf$SavedState
242 save N userdict maxlength dict begin/magscale true def normalscale
243 currentpoint TR/psf$ury psfts/psf$urx psfts/psf$lly psfts/psf$llx psfts
244 /psf$y psfts/psf$x psfts currentpoint/psf$cy X/psf$cx X/psf$sx psf$x
245 psf$urx psf$llx sub div N/psf$sy psf$y psf$ury psf$lly sub div N psf$sx
246 psf$sy scale psf$cx psf$sx div psf$llx sub psf$cy psf$sy div psf$ury sub
247 TR/showpage{}N/erasepage{}N/copypage{}N/p 3 def @MacSetUp}N/doclip{
248 psf$llx psf$lly psf$urx psf$ury currentpoint 6 2 roll newpath 4 copy 4 2
249 roll moveto 6 -1 roll S lineto S lineto S lineto closepath clip newpath
250 moveto}N/endTexFig{end psf$SavedState restore}N/@beginspecial{SDict
251 begin/SpecialSave save N gsave normalscale currentpoint TR
252 @SpecialDefaults count/ocount X/dcount countdictstack N}N/@setspecial{
253 CLIP 1 eq{newpath 0 0 moveto hs 0 rlineto 0 vs rlineto hs neg 0 rlineto
254 closepath clip}if ho vo TR hsc vsc scale ang rotate rwiSeen{rwi urx llx
255 sub div rhiSeen{rhi ury lly sub div}{dup}ifelse scale llx neg lly neg TR
256 }{rhiSeen{rhi ury lly sub div dup scale llx neg lly neg TR}if}ifelse
257 CLIP 2 eq{newpath llx lly moveto urx lly lineto urx ury lineto llx ury
258 lineto closepath clip}if/showpage{}N/erasepage{}N/copypage{}N newpath}N
259 /@endspecial{count ocount sub{pop}repeat countdictstack dcount sub{end}
260 repeat grestore SpecialSave restore end}N/@defspecial{SDict begin}N
261 /@fedspecial{end}B/li{lineto}B/rl{rlineto}B/rc{rcurveto}B/np{/SaveX
262 currentpoint/SaveY X N 1 setlinecap newpath}N/st{stroke SaveX SaveY
263 moveto}N/fil{fill SaveX SaveY moveto}N/ellipse{/endangle X/startangle X
264 /yrad X/xrad X/savematrix matrix currentmatrix N TR xrad yrad scale 0 0
265 1 startangle endangle arc savematrix setmatrix}N end
268 TeXDict begin 39158280 55380996 1000 600 600 (dddmp-2.0.dvi)
269 @start /Fa 143[55 1[55 7[28 2[50 99[{TeXBase1Encoding ReEncodeFont}4
270 99.6264 /Helvetica rf
271 %DVIPSBitmapFont: Fb cmr12 12 3
272 /Fb 3 53 df<14FF010713E090381F81F890383E007C01FC133F4848EB1F8049130F4848
273 EB07C04848EB03E0A2000F15F0491301001F15F8A2003F15FCA390C8FC4815FEA54815FF
274 B3A46C15FEA56D1301003F15FCA3001F15F8A26C6CEB03F0A36C6CEB07E0000315C06D13
275 0F6C6CEB1F806C6CEB3F00013E137C90381F81F8903807FFE0010090C7FC28447CC131>
276 48 D<143014F013011303131F13FFB5FC13E713071200B3B3B0497E497E007FB6FCA320
277 4278C131>I<ED0380A21507150FA2151F153FA2157F15FFA25CEC03BF153F1407140614
278 0C141C141814301470146014C013011480EB03005B13065B131C13185B1370136013E048
279 5A5B120390C7FC1206120E120C5A123812305A12E0B812C0A3C8383F8000ADEDFFE0027F
280 EBFFC0A32A437DC231>52 D E
282 /Fc 64[50 29[39 12[55 55 25[44 44 66 44 50 28 39 39 1[50
283 50 50 72 28 44 1[28 50 50 28 44 50 44 50 50 10[61 2[50
284 4[66 83 55 2[33 2[61 1[72 66 61 61 15[50 2[25 33 25 2[33
285 33 37[50 2[{TeXBase1Encoding ReEncodeFont}45 99.6264
287 %DVIPSBitmapFont: Fd cmmi12 12 3
288 /Fd 3 103 df<F001C0F007E0181FF07FC0943801FF00EF07FCEF1FF0EF7FC04C48C7FC
289 EE0FFCEE3FF0EEFFC0030390C8FCED0FF8ED3FE0EDFF80DA03FEC9FCEC1FF8EC7FE09038
290 01FF80D907FECAFCEB1FF0EB7FC04848CBFCEA07FCEA1FF0EA7FC048CCFCA2EA7FC0EA1F
291 F0EA07FCEA01FF38007FC0EB1FF0EB07FE903801FF809038007FE0EC1FF8EC03FE913800
292 FF80ED3FE0ED0FF8ED03FF030013C0EE3FF0EE0FFCEE01FF9338007FC0EF1FF0EF07FCEF
293 01FF9438007FC0F01FE01807F001C03B3878B44C>60 D<127012FCB4FCEA7FC0EA1FF0EA
294 07FCEA01FF38007FC0EB1FF0EB07FE903801FF809038007FE0EC1FF8EC03FE913800FF80
295 ED3FE0ED0FF8ED03FF030013C0EE3FF0EE0FFCEE01FF9338007FC0EF1FF0EF07FCEF01FF
296 9438007FC0F01FE0A2F07FC0943801FF00EF07FCEF1FF0EF7FC04C48C7FCEE0FFCEE3FF0
297 EEFFC0030390C8FCED0FF8ED3FE0EDFF80DA03FEC9FCEC1FF8EC7FE0903801FF80D907FE
298 CAFCEB1FF0EB7FC04848CBFCEA07FCEA1FF0EA7FC048CCFC12FC12703B3878B44C>62
299 D<EE07E0EE1FF8EE7C1CEEF80E923801F03E923803E07F17FFED07E116C117FE92380FC0
300 FC177817004B5AA4153F93C7FCA45D157EA491B61280A3DA00FCC7FCA314015DA414035D
301 A414075DA4140F5DA5141F5DA4143F92C8FCA45C147EA45CA45C1301A25CA2EA1C03007F
302 5B12FF5C13075C4848C9FC12F8EA601EEA783CEA1FF0EA07C0305A7BC530>102
305 /Fe 134[42 2[42 42 23 32 28 1[42 42 42 65 23 2[23 42
306 42 28 37 42 1[42 37 12[51 10[28 4[60 1[55 19[21 28 21
307 44[{TeXBase1Encoding ReEncodeFont}26 83.022 /Times-Roman
309 %DVIPSBitmapFont: Ff cmr7 7 2
310 /Ff 2 51 df<13381378EA01F8121F12FE12E01200B3AB487EB512F8A215267BA521>49
311 D<13FF000313E0380E03F0381800F848137C48137E00787F12FC6CEB1F80A4127CC7FC15
312 005C143E147E147C5C495A495A5C495A010EC7FC5B5B903870018013E0EA018039030003
313 0012065A001FB5FC5A485BB5FCA219267DA521>I E
315 /Fg 103[60 26[60 1[60 60 60 60 60 60 60 60 60 60 60 60
316 60 60 60 60 2[60 60 60 60 60 60 60 60 60 3[60 1[60 3[60
317 60 1[60 60 1[60 60 1[60 60 3[60 1[60 1[60 60 60 1[60
318 60 1[60 1[60 1[60 60 60 60 60 60 60 60 60 60 60 60 60
319 60 60 5[60 38[{TeXBase1Encoding ReEncodeFont}62 99.6264
321 %DVIPSBitmapFont: Fh cmr8 8 2
322 /Fh 2 51 df<130C133C137CEA03FC12FFEAFC7C1200B3B113FE387FFFFEA2172C7AAB23
323 >49 D<EB7F803801FFF0380780FC380E003F48EB1F8048EB0FC05A0060EB07E012F000FC
324 14F07E1403A3007C1307C7FCA215E0140F15C0141F1580EC3F00147E147C5C495A495A49
325 5A495A011EC7FC5B5B4913305B485A4848136048C7FC000E14E0001FB5FC5A4814C0B6FC
328 /Fi 105[50 28[50 50 2[55 33 39 44 1[55 50 55 83 28 2[28
329 1[50 33 44 55 44 55 50 10[72 1[66 55 3[78 72 94 66 3[78
330 1[61 66 72 72 66 72 13[50 50 50 1[28 25 33 45[{
331 TeXBase1Encoding ReEncodeFont}40 99.6264 /Times-Bold
332 rf /Fj 139[40 1[53 1[66 60 66 100 33 2[33 3[53 3[60 23[47
333 2[73 18[60 60 60 2[30 46[{TeXBase1Encoding ReEncodeFont}16
334 119.552 /Times-Bold rf
335 %DVIPSBitmapFont: Fk cmsy10 12 1
336 /Fk 1 16 df<49B4FC010F13E0013F13F8497F48B6FC4815804815C04815E04815F0A248
337 15F8A24815FCA3B712FEA96C15FCA36C15F8A26C15F0A26C15E06C15C06C15806C15006C
338 6C13FC6D5B010F13E0010190C7FC27277BAB32>15 D E
340 /Fl 64[44 42[44 44 24[44 50 50 72 50 50 28 39 33 50 50
341 50 50 78 28 50 28 28 50 50 33 44 50 44 50 44 6[61 1[72
342 94 72 72 61 55 66 72 55 72 72 89 61 1[39 33 72 72 55
343 61 72 66 66 72 3[56 1[28 28 50 50 50 50 50 50 50 50 50
344 50 28 25 33 25 2[33 33 36[55 55 2[{TeXBase1Encoding ReEncodeFont}74
345 99.6264 /Times-Roman rf
346 %DVIPSBitmapFont: Fm cmsy10 14.4 2
347 /Fm 2 104 df<EE1FE0ED01FF150F92383FF800EDFFC04A90C7FC4A5A4A5A4A5A4A5A5D
348 A2143F5DB3B1147F5D14FF92C8FC5B495A495A495AEB3FE0EBFF80D87FFEC9FCEAFFF8A2
349 EA7FFEC66C7EEB3FE0EB0FF86D7E6D7E6D7E7F81147F81143FB3B181141FA2816E7E6E7E
350 6E7E6E7E6E13C0ED3FF892380FFFE01501ED001F2B7878D93C>102
351 D<B4FC13F813FF000313C038007FF0EB1FF8EB07FC6D7E6D7E6D7F147FA281143FB3B181
352 141F81140F816E7E6E7E6E7E6E6C7EED3FF092380FFFC0030113E0A2030F13C092383FF0
353 00ED7F804A48C7FC4A5A4A5A4A5A5D141F5D143F5DB3B1147F5DA214FF4990C8FC495A49
354 5AEB1FF8EB7FF03803FFC0B5C9FC13F890CAFC2B7878D93C>I E
356 /Fn 105[60 27[53 4[60 33 47 40 60 60 60 60 93 33 2[33
357 1[60 40 53 60 53 60 53 7[86 4[73 66 1[86 66 3[73 2[40
358 1[86 1[73 86 80 1[86 110 5[33 60 4[60 1[60 60 60 1[30
359 40 30 44[{TeXBase1Encoding ReEncodeFont}42 119.552 /Times-Roman
360 rf /Fo 136[104 1[80 48 56 64 1[80 72 80 120 40 80 1[40
361 1[72 1[64 80 64 80 72 12[96 80 104 1[88 1[104 135 3[56
362 2[88 1[104 104 96 104 6[48 1[72 72 72 72 72 72 72 72
363 72 1[36 46[{TeXBase1Encoding ReEncodeFont}41 143.462
367 %%Feature: *Resolution 600dpi
375 1 0 bop 472 600 a Fo(DDDMP:)35 b(Decision)f(Diagram)f(DuMP)j(package)
376 1480 830 y(Release)e(2.0)462 1230 y Fn(Gianpiero)c(Cabodi)2402
377 1232 y(Stef)o(ano)g(Quer)1316 1506 y(Politecnico)g(di)g(T)-10
378 b(orino)1024 1656 y(Dip.)30 b(di)g(Automatica)g(e)g(Informatica)1119
379 1805 y(Corso)f(Duca)h(de)n(gli)g(Abruzzi)g(24)1277 1955
380 y(I\22610129)e(T)-5 b(urin,)29 b(IT)-11 b(AL)f(Y)1038
381 2104 y(E-mail:)38 b Fm(f)p Fn(cabodi,quer)p Fm(g)p Fn(@polito.it)-189
382 2614 y Fo(1)143 b(Intr)m(oduction)-189 2837 y Fl(The)27
383 b(DDDMP)h(package)f(de\002nes)h(formats)f(and)g(rules)g(to)g(store)g
384 (DD)g(on)g(\002le.)39 b(More)27 b(in)g(particular)g(it)g(contains)g(a)
385 -189 2958 y(set)e(of)g(functions)e(to)i(dump)e(\(store)i(and)g(load\))g
386 (DDs)f(and)h(DD)g(forests)f(on)h(\002le)g(in)f(dif)n(ferent)h(formats.)
387 47 3078 y(In)30 b(the)g(present)g(implementation,)f(BDDs)h(\(R)l
388 (OBDDs\))h(and)f(ADD)g(\(Algebraic)g(Decision)g(Diagram\))g(of)-189
389 3199 y(the)g(CUDD)g(package)g(\(v)o(ersion)f(2.3.0)g(or)h(higher\))g
390 (are)g(supported.)45 b(These)30 b(structures)f(can)h(be)g(represented)g
391 (on)-189 3319 y(\002les)25 b(either)g(in)f(te)o(xt,)g(binary)-6
392 b(,)24 b(or)h(CNF)g(\(DIMA)l(CS\))h(formats.)47 3439
393 y(The)f(main)f(rules)h(used)f(are)i(follo)n(wing)d(rules:)-44
394 3643 y Fk(\017)49 b Fl(A)30 b(\002le)h(contains)e(a)i(single)e(BDD/ADD)
395 h(or)g(a)h(forest)f(of)g(BDDs/ADD,)g(i.e.,)i(a)e(v)o(ector)g(of)g
396 (Boolean)h(func-)55 3763 y(tions.)-44 3966 y Fk(\017)49
397 b Fl(Inte)o(ger)21 b(inde)o(x)o(es)f(are)i(used)f(instead)g(of)g
398 (pointers)g(to)g(reference)i(nodes.)29 b(BDD/ADD)21 b(nodes)g(are)h
399 (numbered)55 4087 y(with)j(contiguous)g(numbers,)g(from)h(1)g(to)f
400 (NNodes)h(\(total)f(number)h(of)g(nodes)g(on)f(a)i(\002le\).)35
401 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
402 (inde)o(x)o(es)h(for)i(complemented)f(edges.)-44 4411
403 y Fk(\017)49 b Fl(A)23 b(\002le)g(contains)f(a)h(header)l(,)h
404 (including)d(se)n(v)o(eral)h(informations)f(about)h(v)n(ariables)h(and)
405 f(roots)g(of)h(BDD)h(func-)55 4531 y(tions,)32 b(then)e(the)h(list)g
406 (of)g(nodes.)49 b(The)32 b(header)f(is)g(al)o(w)o(ays)g(represented)h
407 (in)f(te)o(xt)f(format)h(\(also)g(for)g(binary)55 4651
408 y(\002les\).)g(BDDs,)25 b(ADDs,)f(and)h(CNF)h(\002les)f(share)g(a)g
409 (similar)f(format)g(header)-5 b(.)-44 4855 y Fk(\017)49
410 b Fl(BDD/ADD)40 b(nodes)g(are)h(listed)f(follo)n(wing)e(their)i
411 (numbering,)j(which)d(is)g(produced)g(by)h(a)f(post-order)55
412 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
413 (is)h(al)o(w)o(ays)f(listed)g(after)h(its)f(Then/Else)g(children.)47
414 5179 y(In)32 b(the)f(sequel)g(we)g(describe)h(more)f(in)g(detail)f(the)
415 h(dif)n(ferent)g(formats)g(and)g(procedures)h(a)n(v)n(ailable.)49
416 b(First)-189 5299 y(of)26 b(all,)f(we)h(describe)f(BDDs)h(and)g(ADDs)f
417 (formats)g(and)g(procedure.)33 b(Secondly)-6 b(,)26 b(we)f(concentrate)
418 h(on)f(CNF)i(\002les,)-189 5419 y(i.e.,)e(ho)n(w)f(to)g(translate)g(a)i
419 (BDD)f(or)g(a)g(forest)g(of)f(BDDs)h(into)f(a)h(CNF)h(formula)e(and)h
420 (vice-v)o(ersa.)1794 5800 y(1)p eop
422 2 1 bop -189 218 a Fo(2)143 b(BDD)35 b(and)g(ADD)g(Support)-189
423 441 y Fl(In)23 b(this)f(section)g(we)g(describe)h(format)g(and)f
424 (procedure)h(re)o(garding)f(BDDs)h(and)f(ADDs.)30 b(W)-8
425 b(e)23 b(speci\002cally)g(refer)g(to)-189 562 y(BDDs)h(in)g(the)g
426 (description)e(as)j(ADD)e(may)h(be)g(seen)g(as)h(an)f(e)o(xtension)e
427 (and)i(will)f(be)h(described)g(later)-5 b(.)30 b(First)24
428 b(of)g(all,)-189 682 y(we)29 b(concentrate)f(on)g(the)g(format)g(used)g
429 (to)g(store)g(these)g(structure,)h(then)f(we)g(describe)h(the)f
430 (procedure)h(a)n(v)n(ailable)-189 802 y(to)24 b(store)h(and)g(load)f
431 (them.)-189 1094 y Fj(2.1)119 b(F)m(ormat)-189 1281 y
432 Fl(BDD)30 b(dump)f(\002les)g(are)i(composed)e(of)g(tw)o(o)g(sections:)
433 40 b(The)29 b(header)h(and)g(the)f(list)g(of)h(nodes.)44
434 b(The)30 b(header)g(has)g(a)-189 1402 y(common)c(\(te)o(xt\))h(format,)
435 h(while)e(the)i(list)e(of)h(nodes)g(is)g(either)g(in)g(te)o(xt)g(or)g
436 (binary)g(format.)38 b(In)28 b(te)o(xt)e(format)h(nodes)-189
437 1522 y(are)33 b(represented)f(with)f(redundant)g(informations,)h(where)
438 h(the)f(main)f(goal)g(is)h(readability)-6 b(,)32 b(while)g(the)f
439 (purpose)-189 1642 y(of)i(binary)f(format)g(is)g(minimizing)e(the)i(o)o
440 (v)o(erall)f(storage)h(size)h(for)g(BDD)f(nodes.)54 b(The)32
441 b(header)h(format)f(is)g(k)o(ept)-189 1763 y(common)h(to)h(te)o(xt)g
442 (and)g(binary)g(formats)g(for)h(sak)o(e)f(of)h(simplicity:)47
443 b(No)34 b(particular)g(optimization)f(is)h(presently)-189
444 1883 y(done)29 b(on)f(binary)h(\002le)g(headers,)h(whose)f(size)g(is)f
445 (by)h(f)o(ar)g(dominated)f(by)h(node)f(lists)g(in)g(the)h(case)g(of)g
446 (lar)n(ge)h(BDDs)-189 2003 y(\(se)n(v)o(eral)24 b(thousands)g(of)h(DD)f
447 (nodes\).)-189 2266 y Fi(2.1.1)99 b(Header)-189 2453
448 y Fl(The)23 b(header)h(has)f(the)g(same)g(format)g(both)g(for)g(te)o
449 (xtual)f(and)i(binary)e(dump.)30 b(F)o(or)23 b(sak)o(e)g(of)h
450 (generality)e(and)h(because)-189 2574 y(of)f(dynamic)g(v)n(ariable)g
451 (ordering)g(both)f(v)n(ariable)h(IDs)g(and)g(permutations)2377
452 2537 y Fh(1)2438 2574 y Fl(are)h(included.)29 b(Names)22
453 b(are)h(optionally)-189 2694 y(listed)35 b(for)h(input)f(v)n(ariables)g
454 (and)h(for)h(the)e(stored)h(functions.)63 b(Ne)n(w)36
455 b(auxiliary)f(IDs)h(are)h(also)e(allo)n(wed.)64 b(Only)-189
456 2814 y(the)34 b(v)n(ariables)f(in)g(the)h(true)g(support)f(of)h(the)f
457 (stored)h(BDDs)g(are)h(listed.)56 b(All)34 b(information)e(on)i(v)n
458 (ariables)f(\(IDs,)-189 2935 y(permutations,)c(names,)i(auxiliary)e
459 (IDs\))h(sorted)g(by)g(IDs,)h(and)e(the)o(y)h(are)g(restricted)g(to)f
460 (the)h(true)g(support)f(of)h(the)-189 3055 y(dumped)22
461 b(BDD,)h(while)g(IDs)g(and)f(permutations)g(are)h(referred)i(to)d(the)h
462 (writing)f(BDD)h(manager)-5 b(.)30 b(Names)22 b(can)i(thus)-189
463 3175 y(be)h(sorted)f(by)h(v)n(ariable)f(ordering)h(by)f(permuting)g
464 (them)g(according)h(to)f(the)h(permutations)e(stored)h(in)h(the)f
465 (\002le.)47 3296 y(As)h(an)g(e)o(xample,)f(the)g(header)i(\(in)e(te)o
466 (xt)g(mode\))h(of)f(the)h(ne)o(xt)f(state)h(functions)e(of)i(circuit)g
467 (s27)f(follo)n(ws:)-189 3494 y Fg(.ver)59 b(DDDMP-2.0)-189
468 3615 y(.mode)g(A)-189 3735 y(.varinfo)f(3)-189 3855 y(.dd)h(s27-delta)
469 -189 3976 y(.nnodes)f(16)-189 4096 y(.nvars)g(10)-189
470 4216 y(.nsuppvars)g(7)-189 4337 y(.varnames)g(G0)h(G1)g(G2)h(G3)f(G5)g
471 (G6)h(G7)-189 4457 y(.orderedvarnames)c(G0)k(G1)f(G2)g(G3)h(G5)f(G6)g
472 (G7)-189 4578 y(.ids)g(0)g(1)h(2)g(3)f(4)h(5)f(6)-189
473 4698 y(.permids)f(0)i(1)f(2)h(3)f(5)h(7)f(9)-189 4818
474 y(.auxids)f(1)i(2)f(3)h(4)f(5)h(6)g(7)-189 4939 y(.nroots)e(3)-189
475 5059 y(.rootids)g(6)i(-13)f(-16)-189 5179 y(.rootnames)f(G10)h(G11)g
476 (G13)47 5378 y Fl(The)25 b(lines)f(contain)g(the)h(follo)n(wing)e
477 (informations:)p -189 5460 1607 4 v -77 5521 a Ff(1)-40
478 5551 y Fe(The)d(permutation)e(of)i(the)g(i-th)h(v)n(ariable)e(ID)h(is)h
479 (the)f(relati)n(v)o(e)g(position)f(of)h(the)g(v)n(ariable)f(in)i(the)f
480 (ordering.)1794 5800 y Fl(2)p eop
482 3 2 bop -44 218 a Fk(\017)49 b Fl(Dddmp)24 b(v)o(ersion)f(information.)
483 -44 411 y Fk(\017)49 b Fl(File)25 b(mode)f(\(A)h(for)g(ASCII)h(te)o
484 (xt,)e(B)h(for)g(binary)g(mode\).)-44 604 y Fk(\017)49
485 b Fl(V)-11 b(ar)n(-e)o(xtra-info)25 b(\(0:)30 b(v)n(ariable)24
486 b(ID,)h(1:)31 b(permID,)24 b(2:)31 b(aux)25 b(ID,)g(3:)30
487 b(v)n(ariable)24 b(name,)h(4)g(no)f(e)o(xtra)h(info\).)-44
488 797 y Fk(\017)49 b Fl(Name)25 b(of)g(dd)f(\(optional\).)-44
489 990 y Fk(\017)49 b Fl(T)-8 b(otal)24 b(number)g(of)h(nodes)g(in)f(the)h
490 (\002le.)-44 1183 y Fk(\017)49 b Fl(Number)24 b(of)h(v)n(ariables)f(of)
491 h(the)g(writing)f(DD)g(manager)-5 b(.)-44 1375 y Fk(\017)49
492 b Fl(Number)24 b(of)h(v)n(ariables)f(in)h(the)f(true)h(support)f(of)h
493 (the)f(stored)h(DDs.)-44 1568 y Fk(\017)49 b Fl(V)-11
494 b(ariable)25 b(names)f(\(optional\))g(for)h(all)g(the)f(v)n(ariables)g
495 (in)h(the)f(BDD/ADD)h(support.)-44 1761 y Fk(\017)49
496 b Fl(V)-11 b(ariable)20 b(names)g(for)h(all)f(the)g(v)n(ariables)f(in)h
497 (the)g(DD)h(manager)f(during)g(the)g(storing)f(phase.)29
498 b(Notice)20 b(that)g(this)55 1882 y(information)k(w)o(as)h(not)g
499 (stored)g(by)g(pre)n(vious)f(v)o(ersions)g(of)i(the)f(same)g(tool.)32
500 b(Full)25 b(backw)o(ard)g(compatibility)55 2002 y(is)f(guaranteed)h(by)
501 g(the)f(present)h(implementation)d(of)j(the)g(tool.)-44
502 2195 y Fk(\017)49 b Fl(V)-11 b(ariable)25 b(IDs.)-44
503 2388 y Fk(\017)49 b Fl(V)-11 b(ariable)25 b(permuted)f(IDs.)-44
504 2581 y Fk(\017)49 b Fl(V)-11 b(ariable)25 b(auxiliary)f(IDs)h
505 (\(optional\).)-44 2774 y Fk(\017)49 b Fl(Number)24 b(of)h(BDD)g
506 (roots.)-44 2967 y Fk(\017)49 b Fl(Inde)o(x)o(es)24 b(of)h(BDD)g(roots)
507 f(\(complemented)g(edges)g(allo)n(wed\).)-44 3160 y Fk(\017)49
508 b Fl(Names)24 b(of)h(BDD)h(roots)e(\(optional\).)-189
509 3332 y(Notice)h(that)f(a)h(\002eld)-189 3504 y Fg(.add)-189
510 3676 y Fl(is)f(present)h(after)g(the)g(dddmp)f(v)o(ersion)f(for)j
511 (\002les)e(containing)g(ADDs.)-189 3936 y Fi(2.1.2)99
512 b(T)-9 b(ext)25 b(F)n(ormat)-189 4124 y Fl(In)g(te)o(xt)f(mode)g(nodes)
513 g(are)i(listed)e(on)g(a)h(te)o(xt)f(line)h(basis.)30
514 b(Each)25 b(a)g(node)f(is)h(represented)g(as)-189 4296
515 y Fg(<Node-index>)57 b([<Var-extra-info>])f(<Var-internal-index>)588
516 4416 y(<Then-index>)h(<Else-index>)-189 4588 y Fl(where)25
517 b(all)g(inde)o(x)o(es)e(are)j(inte)o(ger)e(numbers.)47
518 4709 y(This)h(format)g(is)g(redundant)f(\(due)i(to)f(the)g(node)g
519 (ordering,)g Fd(<)p Fl(Node-inde)o(x)p Fd(>)f Fl(is)g(and)i
520 (incremental)e(inte)o(ger\))-189 4829 y(b)n(ut)g(we)h(k)o(eep)g(it)g
521 (for)g(readability)-6 b(.)47 4949 y Fd(<)p Fl(V)-11 b(ar)n(-e)o
522 (xtra-info)p Fd(>)34 b Fl(\(optional)e(redundant)i(\002eld\))g(is)f
523 (either)h(an)g(inte)o(ger)f(\(ID,)h(PermID,)g(or)g(auxID\))g(or)g(a)
524 -189 5070 y(string)k(\(v)n(ariable)h(name\).)75 b Fd(<)p
525 Fl(V)-11 b(ar)n(-internal-inde)o(x)p Fd(>)38 b Fl(is)h(an)g(internal)g
526 (v)n(ariable)g(inde)o(x:)59 b(V)-11 b(ariables)39 b(in)g(the)g(true)
527 -189 5190 y(support)25 b(of)h(the)g(stored)g(BDDs)g(are)h(numbered)e
528 (with)g(ascending)h(inte)o(gers)f(starting)g(from)h(0,)g(and)g(follo)n
529 (wing)e(the)-189 5311 y(v)n(ariable)g(ordering.)31 b
530 Fd(<)p Fl(Then-inde)o(x)p Fd(>)23 b Fl(and)i Fd(<)p Fl(Else-inde)o(x)p
531 Fd(>)e Fl(are)j(signed)e(inde)o(x)o(es)f(of)i(children)f(nodes.)47
532 5431 y(In)h(the)f(follo)n(wing,)f(we)i(report)f(the)g(list)g(of)h
533 (nodes)f(of)g(the)h(s27)f(ne)o(xt)f(state)i(functions)e(\(see)i(pre)n
534 (vious)e(header)-189 5551 y(e)o(xample\):)1794 5800 y(3)p
537 4 3 bop -189 218 a Fg(.nodes)-189 338 y(1)60 b(T)f(1)h(0)f(0)-189
538 459 y(2)h(G7)f(6)g(1)h(-1)-189 579 y(3)g(G5)f(4)g(1)h(2)-189
539 699 y(4)g(G3)f(3)g(3)h(1)-189 820 y(5)g(G1)f(1)g(1)h(4)-189
540 940 y(6)g(G0)f(0)g(5)h(-1)-189 1061 y(7)g(G6)f(5)g(1)h(-1)-189
541 1181 y(8)g(G5)f(4)g(1)h(-7)-189 1301 y(9)g(G6)f(5)g(1)h(-2)-189
542 1422 y(10)f(G5)h(4)f(1)h(-9)-189 1542 y(11)f(G3)h(3)f(10)h(8)-189
543 1662 y(12)f(G1)h(1)f(8)h(11)-189 1783 y(13)f(G0)h(0)f(5)h(12)-189
544 1903 y(14)f(G2)h(2)f(1)h(-1)-189 2024 y(15)f(G2)h(2)f(1)h(-2)-189
545 2144 y(16)f(G1)h(1)f(14)h(15)-189 2264 y(.end)-189 2468
546 y Fl(The)27 b(list)f(is)h(enclosed)g(between)g(the)g
547 Fg(.nodes)f Fl(and)h Fg(.end)f Fl(lines.)37 b(First)27
548 b(node)g(is)g(the)g(one)g(constant,)f(each)i(node)-189
549 2588 y(contains)c(the)h(optional)e(v)n(ariable)h(name.)47
550 2708 y(F)o(or)29 b(ADDs)f(more)h(than)f(one)h(constant)e(is)i(stored)f
551 (in)g(the)g(\002le.)43 b(Each)29 b(constant)f(has)g(the)h(same)f
552 (format)h(we)-189 2829 y(ha)n(v)o(e)c(just)e(analyzed)i(for)g(the)g
553 (BDD)g(b)n(ut)g(the)f(represented)h(v)n(alue)f(is)h(stored)f(as)h(a)g
554 (\003oat)g(number)-5 b(.)-189 3095 y Fi(2.1.3)99 b(Binary)25
555 b(F)n(ormat)-189 3283 y Fl(The)h(binary)g(format)f(is)h(not)f(allo)n
556 (wed)g(for)i(ADDs.)33 b(As)26 b(a)h(consequence)f(we)g(concentrate)g
557 (only)f(on)h(BDDs)g(in)g(this)-189 3403 y(section.)k(In)25
558 b(binary)f(mode)h(nodes)f(are)i(represented)f(as)g(a)g(sequence)g(of)g
559 (bytes,)f(encoding)g(tuples)-189 3606 y Fg(<Node-code>)-189
560 3727 y([<Var-internal-info>])-189 3847 y([<Then-info>])-189
561 3968 y([<Else-info>])-189 4171 y Fl(in)30 b(an)g(optimized)f(w)o(ay)-6
562 b(.)46 b(Only)29 b(the)h(\002rst)g(byte)g(\(code\))h(is)e(mandatory)-6
563 b(,)30 b(while)g(inte)o(ger)f(inde)o(x)o(es)g(are)i(represented)-189
564 4291 y(in)c(absolute)f(or)h(relati)n(v)o(e)f(mode,)h(where)h(relati)n
565 (v)o(e)e(means)g(of)n(fset)h(with)f(respect)i(to)e(a)i(Then/Else)e
566 (node)h(info.)37 b(The)-189 4412 y(best)23 b(between)g(absolute)f(and)h
567 (relati)n(v)o(e)e(representation)i(is)f(chosen)h(and)g(relati)n(v)o(e)f
568 (1)h(is)f(directly)g(coded)h(in)g Fd(<)p Fl(Node-)-189
569 4532 y(code)p Fd(>)e Fl(without)f(an)o(y)g(e)o(xtra)h(info.)29
570 b(Suppose)21 b(V)-11 b(ar\(NodeId\),)22 b(Then\(NodeId\))f(and)g
571 (Else\(NodeId\))f(represent)i(infos)-189 4652 y(about)i(a)h(gi)n(v)o
572 (en)f(node.)30 b Fd(<)p Fl(Node-code)p Fd(>)25 b Fl(is)f(a)h(byte)g
573 (which)f(contains)g(the)h(follo)n(wing)e(bit)h(\002elds)h(\(MSB)g(to)g
574 (LSB\))-44 4856 y Fk(\017)49 b Fl(Unused)24 b(:)31 b(1)24
575 b(bit)-44 5059 y Fk(\017)49 b Fl(V)-11 b(ariable:)30
576 b(2)25 b(bits,)f(one)h(of)g(the)f(follo)n(wing)f(codes)171
577 5288 y Fi(\226)49 b Fl(DDDMP)p 636 5288 30 4 v 35 w(ABSOLUTE)p
578 1191 5288 V 36 w(ID:)22 b(V)-11 b(ar\(NodeId\))22 b(is)f(represented)h
579 (in)g(absolute)f(form)g(as)h Fd(<)p Fl(V)-11 b(ar)n(-internal-)270
580 5408 y(info)p Fd(>)24 b Fl(=)h(V)-11 b(ar\(NodeId\))25
581 b(follo)n(ws)e(\(absolute)i(info\))1794 5800 y(4)p eop
583 5 4 bop 171 218 a Fi(\226)49 b Fl(DDDMP)p 636 218 30
584 4 v 35 w(RELA)-11 b(TIVE)p 1147 218 V 36 w(ID:)32 b(V)-11
585 b(ar\(NodeId\))32 b(is)g(represented)g(in)f(relati)n(v)o(e)g(form)h(as)
586 g Fd(<)p Fl(V)-11 b(ar)n(-internal-)270 338 y(info\277)24
587 b(=)h(Min\(V)-11 b(ar\(Then\(NodeId\)\),V)g(ar\(Else\(NodeId\)\)\)-V)g
588 (ar\(NodeId\))171 500 y Fi(\226)49 b Fl(DDDMP)p 636 500
589 V 35 w(RELA)-11 b(TIVE)p 1147 500 V 36 w(1:)27 b(the)19
590 b(\002eld)g Fd(<)p Fl(V)-11 b(ar)n(-internal-info)p Fd(>)18
591 b Fl(does)h(not)f(follo)n(w)-6 b(,)18 b(because)h(V)-11
592 b(ar\(NodeId\))270 620 y(=)25 b(Min\(V)-11 b(ar\(Then\(NodeId\)\),V)g
593 (ar\(Else\(NodeId\)\)\)-1)171 782 y Fi(\226)49 b Fl(DDDMP)p
594 636 782 V 35 w(TERMIN)m(AL:)24 b(Node)h(is)f(a)h(terminal,)f(no)g(v)n
595 (ar)h(info)g(required)-44 1011 y Fk(\017)49 b Fl(T)25
596 b(:)f(2)h(bits,)f(with)g(codes)h(similar)e(to)i(V)171
597 1214 y Fi(\226)49 b Fl(DDDMP)p 636 1214 V 35 w(ABSOLUTE)p
598 1191 1214 V 36 w(ID:)20 b Fd(<)p Fl(Then-info)p Fd(>)f
599 Fl(is)h(represented)g(in)g(absolute)f(form)h(as)g Fd(<)p
600 Fl(Then-info)p Fd(>)270 1334 y Fl(=)25 b(Then\(NodeId\))171
601 1496 y Fi(\226)49 b Fl(DDDMP)p 636 1496 V 35 w(RELA)-11
602 b(TIVE)p 1147 1496 V 36 w(ID:)28 b(Then\(NodeId\))f(is)g(represented)h
603 (in)g(relati)n(v)o(e)e(form)i(as)g Fd(<)p Fl(Then-info)p
604 Fd(>)270 1617 y Fl(=)d(Nodeid-Then\(NodeId\))171 1779
605 y Fi(\226)49 b Fl(DDDMP)p 636 1779 V 35 w(RELA)-11 b(TIVE)p
606 1147 1779 V 36 w(1:)30 b(no)25 b Fd(<)p Fl(Then-info)p
607 Fd(>)f Fl(follo)n(ws,)f(because)i(Then\(NodeId\))g(=)g(NodeId-1)171
608 1941 y Fi(\226)49 b Fl(DDDMP)p 636 1941 V 35 w(TERMIN)m(AL:)24
609 b(Then)h(Node)f(is)h(a)g(terminal,)f(no)g(info)h(required)f(\(for)i(R)l
610 (OBDDs\))-44 2144 y Fk(\017)49 b Fl(Ecompl)24 b(:)30
611 b(1)25 b(bit,)f(if)h(1)g(means)f(that)g(the)h(else)g(edge)g(is)f
612 (complemented)-44 2347 y Fk(\017)49 b Fl(E)25 b(:)f(2)h(bits,)f(with)g
613 (codes)h(and)f(meanings)g(as)h(for)g(the)g(Then)f(edge)-189
614 2551 y(DD)35 b(node)f(codes)h(are)h(written)e(as)h(one)g(byte.)60
615 b Fd(<)p Fl(V)-11 b(ar)n(-internal-inde)o(x)p Fd(>)p
616 Fl(,)36 b Fd(<)p Fl(Then-inde)o(x)p Fd(>)p Fl(,)g Fd(<)p
617 Fl(Else-inde)o(x)p Fd(>)e Fl(\(if)-189 2671 y(required\))25
618 b(are)h(represented)f(as)g(unsigned)e(inte)o(ger)h(v)n(alues)g(on)h(a)g
619 (suf)n(\002cient)f(set)h(of)g(bytes)f(\(MSByte)h(\002rst\).)47
620 2792 y(Inte)o(gers)h(of)f(an)o(y)h(length)e(are)j(written)e(as)h
621 (sequences)g(of)g(\224link)o(ed\224)f(bytes)g(\(MSByte)h(\002rst\).)34
622 b(F)o(or)26 b(each)g(byte)-189 2912 y(7)f(bits)f(are)h(used)g(for)g
623 (data)g(and)f(one)h(\(MSBit\))g(as)g(link)f(with)g(a)h(further)g(byte)g
624 (\(MSB)g(=)g(1)g(means)f(one)h(more)g(byte\).)47 3032
625 y(Lo)n(w)f(le)n(v)o(el)g(read/write)h(of)g(bytes)f(\002lters)h
626 Fd(<)p Fl(CR)p Fd(>)p Fl(,)g Fd(<)p Fl(LF)p Fd(>)g Fl(and)g
627 Fd(<)p Fl(ctrl-Z)p Fd(>)f Fl(through)g(escape)h(sequences.)-189
628 3327 y Fj(2.2)119 b(Implementation)-189 3515 y Fl(Store)24
629 b(and)g(load)g(for)g(single)g(Boolean)g(functions)f(and)h(arrays)g(of)g
630 (Boolean)g(functions)f(are)i(implemented.)k(More-)-189
631 3635 y(o)o(v)o(er)l(,)37 b(the)e(current)h(presentation)f(includes)f
632 (functions)h(to)g(retrie)n(v)o(e)g(v)n(ariables)f(names,)k(auxiliary)d
633 (identi\002erss,)-189 3756 y(and)c(all)g(the)g(information)f(contained)
634 h(in)f(the)h(header)h(of)f(the)h(\002les.)50 b(This)30
635 b(information)g(can)h(be)h(used)f(as)g(a)g(pre-)-189
636 3876 y(processing)19 b(step)g(for)i(load)e(operations.)28
637 b(These)20 b(functions)f(allo)n(w)f(to)i(o)o(v)o(ercome)f(fe)n(w)g
638 (limitations)f(of)h(the)h(pre)n(vious)-189 3997 y(implementations.)-189
639 4263 y Fi(2.2.1)99 b(Storing)25 b(Decision)g(Diagrams)-189
640 4450 y Fc(Dddmp)p 111 4450 V 35 w(cuddBddStor)l(e)f Fl(and)h
641 Fc(Dddmp)p 1195 4450 V 35 w(cuddBddArr)o(ayStor)l(e)e
642 Fl(are)j(the)f(tw)o(o)f(store)h(functions,)f(used)h(to)g(store)f(sin-)
643 -189 4571 y(gle)f(BDD)h(or)g(a)f(forest)h(of)f(BDDs,)h(respecti)n(v)o
644 (ely)-6 b(.)28 b(Internally)-6 b(,)23 b Fc(Dddmp)p 2275
645 4571 V 35 w(cuddBddStor)l(e)f Fl(b)n(uilds)g(a)i(dummy)e(1)h(entry)-189
646 4691 y(array)j(of)e(BDDs,)h(and)g(calls)g Fc(dddmp)p
647 1102 4691 V 35 w(cuddBddArr)o(ayStor)l(e)p Fl(.)47 4811
648 y(Since)30 b(con)l(v)o(ersion)e(from)h(DD)h(pointers)e(to)h(inte)o(ger)
649 f(is)h(required,)i(DD)e(nodes)g(are)h(temporarily)e(remo)o(v)o(ed)-189
650 4932 y(from)23 b(the)f(unique)h(hash.)29 b(This)23 b(mak)o(es)f(room)g
651 (in)h(their)f Fc(ne)n(xt)h Fl(\002eld)h(to)e(store)h(node)f(IDs.)30
652 b(Nodes)23 b(are)h(re-link)o(ed)e(after)-189 5052 y(the)i(store)g
653 (operation,)g(possible)f(in)g(a)i(modi\002ed)e(order)-5
654 b(.)31 b(Dumping)22 b(is)i(either)g(in)g(te)o(xt)f(or)i(binary)f(form.)
655 30 b(Both)24 b(a)g(\002le)-189 5173 y(pointer)31 b(\()p
656 Fc(fp)p Fl(\))g(and)g(a)h(\002le)g(name)f(\()p Fc(fname)p
657 Fl(\))h(are)g(pro)o(vided)e(as)h(inputs)f(parameters)i(to)f(store)g
658 (routines.)50 b(BDDs)31 b(are)-189 5293 y(stored)c(to)g(the)g(already)g
659 (open)h(\002le)f Fc(fp)p Fl(,)h(if)f(not)g(NULL.)g(Otherwise)f(\002le)i
660 (whose)f(name)g(is)g Fc(fname)g Fl(is)g(opened.)38 b(This)-189
661 5413 y(is)24 b(intended)g(to)h(allo)n(w)f(either)g(DD)h(storage)g
662 (within)e(\002les)i(containing)f(other)g(data,)h(or)g(to)g(speci\002c)g
663 (\002les.)1794 5800 y(5)p eop
665 6 5 bop -189 218 a Fi(2.2.2)99 b(Loading)25 b(Decision)g(Diagrams)-189
666 405 y Fc(Dddmp)p 111 405 30 4 v 35 w(cuddBddLoad)37 b
667 Fl(and)h Fc(Dddmp)p 1219 405 V 35 w(cuddBddArr)o(ayLoad)f
668 Fl(are)h(the)g(load)g(functions,)i(which)e(read)g(a)g(BDD)-189
669 526 y(dump)24 b(\002le.)47 646 y(F)o(ollo)n(wing)34 b(the)h(store)h
670 (function,)h(the)f(main)f(BDD)h(load)f(function,)j Fc(Dddmp)p
671 2813 646 V 35 w(cuddBddLoad)p Fl(,)f(is)f(imple-)-189
672 767 y(mented)g(by)g(calling)f(the)h(main)g(BDD-array)h(loading)f
673 (function)f Fc(Dddmp)p 2466 767 V 35 w(cuddBddArr)o(ayLoad)p
674 Fl(.)63 b(A)37 b(dynamic)-189 887 y(v)o(ector)24 b(of)h(DD)g(pointers)f
675 (is)g(temporarily)g(allocated)h(to)f(support)g(con)l(v)o(ersion)f(from)
676 i(DD)g(inde)o(x)o(es)e(to)h(pointers.)47 1007 y(Se)n(v)o(eral)40
677 b(criteria)f(are)i(supported)d(for)i(v)n(ariable)f(match)g(between)g
678 (\002le)h(and)g(DD)f(manager)l(,)k(practically)-189 1128
679 y(allo)n(wing)37 b(v)n(ariable)h(permutations)f(or)i(compositions)d
680 (while)i(loading)g(DDs.)71 b(V)-11 b(ariable)39 b(match)f(between)h
681 (the)-189 1248 y(DD)32 b(manager)g(and)g(the)g(BDD)g(\002le)g(is)g
682 (optionally)e(based)i(in)f Fc(IDs)p Fl(,)j Fc(perids)p
683 Fl(,)f Fc(varnames)p Fl(,)g Fc(var)o(auxids)p Fl(;)g(also)f(direct)-189
684 1369 y(composition)j(between)j Fc(IDs)g Fl(and)f Fc(composeids)g
685 Fl(is)g(supported.)68 b(The)38 b Fc(varmatc)o(hmode)e
686 Fl(parameter)i(is)f(used)g(to)-189 1489 y(select)27 b(mathing)e(mode.)
687 37 b(More)27 b(in)f(detail,)h(tw)o(o)f(match)h(modes)f(use)h(the)f
688 (information)g(within)f(the)i(DD)g(manager)l(,)-189 1609
689 y(the)e(other)f(ones)h(use)g(e)o(xtra)f(information,)f(which)i(support)
690 f(an)o(y)g(v)n(ariable)g(remap)h(or)g(change)g(in)f(the)h(ordering.)-44
691 1813 y Fk(\017)49 b Fl(v)n(armatchnode=DDDMP)p 1040 1813
692 V 35 w(V)-13 b(AR)p 1272 1813 V 35 w(MA)i(TCHIDS)19 b(allo)n(ws)f
693 (loading)g(a)h(DD)g(k)o(eeping)f(v)n(ariable)g(IDs)h(unchanged)55
694 1933 y(\(re)o(gardless)24 b(of)h(the)f(v)n(ariable)h(ordering)f(of)h
695 (the)g(reading)f(manager)-5 b(.)55 2095 y(This)24 b(is)g(useful,)g(for)
696 h(e)o(xample,)f(when)g(sw)o(apping)g(DDs)g(to)h(\002le)g(and)f
697 (restoring)g(them)g(later)h(from)f(\002le,)h(after)55
698 2215 y(possible)e(v)n(ariable)i(reordering)g(acti)n(v)n(ations.)-44
699 2419 y Fk(\017)49 b Fl(v)n(armatchnode=DDDMP)p 1040 2419
700 V 35 w(V)-13 b(AR)p 1272 2419 V 35 w(MA)i(TCHPERMIDS)36
701 b(is)e(used)h(to)f(allo)n(w)g(v)n(ariable)g(match)h(according)55
702 2539 y(to)h(the)h(position)e(in)i(the)g(ordering)f(\(retrie)n(v)o(ed)g
703 (by)h(array)h(of)f(permutations)e(stored)h(on)h(\002le)g(and)g(within)
704 55 2660 y(the)h(reading)g(DD)h(manager\).)72 b(A)38 b(possible)f
705 (application)h(is)g(retrie)n(ving)f(BDDs)i(stored)f(after)h(dynamic)55
706 2780 y(reordering,)28 b(from)g(a)g(DD)g(manager)g(where)h(all)e(v)n
707 (ariable)h(IDs)f(map)h(their)f(position)g(in)g(the)h(ordering,)g(and)55
708 2900 y(the)d(loaded)f(BDD)h(k)o(eeps)g(the)g(ordering)f(as)h(stored)f
709 (on)h(\002le.)-44 3104 y Fk(\017)49 b Fl(v)n(armatchnode=DDDMP)p
710 1040 3104 V 35 w(V)-13 b(AR)p 1272 3104 V 35 w(MA)i(TCHN)m(AMES)26
711 b(requires)h(a)h(not)e(NULL)h(v)n(armatchmodes)f(param-)55
712 3224 y(eter;)34 b(this)c(is)g(a)h(v)o(ector)g(of)g(strings)e(in)i
713 (one-to-one)f(correspondence)h(with)f(v)n(ariable)h(IDs)f(of)h(the)g
714 (reading)55 3344 y(manager)-5 b(.)40 b(V)-11 b(ariables)28
715 b(in)g(the)g(DD)g(\002le)g(read)h(are)g(matched)f(with)f(manager)h(v)n
716 (ariables)f(according)h(to)g(their)55 3465 y(name)35
717 b(\(a)h(not)f(NULL)g(v)n(arnames)g(parameter)h(w)o(as)f(required)h
718 (while)f(storing)f(the)h(DD)g(\002le\).)64 b(The)35 b(most)55
719 3585 y(common)c(usage)h(of)g(this)f(feature)i(is)e(in)h(combination)e
720 (with)i(a)g(v)n(ariable)g(ordering)g(stored)f(on)h(a)g(\002le)h(and)55
721 3706 y(based)28 b(on)h(v)n(ariables)f(names.)41 b(Names)29
722 b(must)e(be)i(loaded)f(in)g(an)h(array)g(of)g(strings)e(and)i(passed)f
723 (to)g(the)h(DD)55 3826 y(load)24 b(procedure.)-44 4029
724 y Fk(\017)49 b Fl(v)n(armatchnode=DDDMP)p 1040 4029 V
725 35 w(V)-13 b(AR)p 1272 4029 V 35 w(MA)i(TCHIDS)25 b(has)g(a)g(meaning)f
726 (similar)g(to)55 4150 y(DDDMP)p 421 4150 V 36 w(V)-13
727 b(AR)p 654 4150 V 35 w(MA)i(TCHN)m(AMES)26 b(b)n(ut)h(inte)o(ger)f
728 (auxiliary)g(IDs)h(are)h(used)f(instead)f(of)h(strings.)36
729 b(The)28 b(ad-)55 4270 y(ditional)23 b(not)h(NULL)h(v)n(armathauxids)e
730 (parameter)i(is)g(needed.)-44 4474 y Fk(\017)49 b Fl(v)n
731 (armatchnode=DDDMP)p 1040 4474 V 35 w(V)-13 b(AR)p 1272
732 4474 V 35 w(COMPOSEIDS,)38 b(uses)f(the)f(additional)f(v)n
733 (arcomposeids)g(parameter)55 4594 y(as)25 b(an)g(array)g(of)g(v)n
734 (ariable)f(IDs)h(to)g(be)g(composed)f(with)g(IDs)g(stored)h(in)f
735 (\002le.)-189 4860 y Fi(2.2.3)99 b(DD)25 b(Load/Stor)n(e)h(and)f(V)-9
736 b(ariable)25 b(Ordering)-189 5048 y Fl(Loading)31 b(of)i(Decision)e
737 (Diagrams)h(from)g(\002le)g(supports)f(dif)n(ferent)h(v)n(ariables)g
738 (ordering)f(strate)o(gies,)i(as)g(already)-189 5168 y(pointed)23
739 b(out)h(in)g(the)h(pre)n(vious)e(section.)30 b(This)24
740 b(allo)n(ws)f(or)h(e)o(xample)g(storing)f(dif)n(ferent)i(BDDs)f(each)h
741 (with)f(its)g(o)n(wn)-189 5288 y(v)n(ariable)29 b(ordering,)h(and)g(to)
742 f(mer)n(ge)h(them)f(within)f(the)i(same)f(DD)h(manager)f(by)h(means)f
743 (of)g(proper)h(load)f(opera-)-189 5409 y(tions.)44 b(W)-8
744 b(e)30 b(suggest)f(using)f(DDDMP)p 1175 5409 V 36 w(V)-13
745 b(AR)p 1408 5409 V 36 w(MA)i(TCHIDS)30 b(whene)n(v)o(er)f(IDs)g(k)o
746 (eeps)h(on)f(representing)h(the)f(same)-189 5529 y(entities)24
747 b(while)h(changing)f(v)n(ariable)h(ordering.)31 b(If)25
748 b(this)f(is)h(not)f(true,)h(v)n(ariable)g(names)g(\(if)g(a)n(v)n
749 (ailable\))f(or)i(auxiliary)1794 5800 y(6)p eop
751 7 6 bop -189 218 a Fl(IDs)34 b(are)h(a)g(good)e(w)o(ay)i(to)f
752 (represent)g(in)l(v)n(ariant)f(attrib)n(uted)g(of)i(v)n(ariables)e
753 (across)h(se)n(v)o(eral)g(runs)g(with)f(dif)n(ferent)-189
754 338 y(orderings.)50 b(DDDMP)p 629 338 30 4 v 35 w(V)-13
755 b(AR)p 861 338 V 36 w(COMPOSEIDS)32 b(is)f(an)h(alternati)n(v)o(e)e
756 (solution,)h(that)g(practically)f(corresponds)h(to)-189
757 459 y(cascading)23 b(DDDMP)p 593 459 V 36 w(V)-13 b(AR)p
758 826 459 V 36 w(MA)i(TCHIDS)23 b(and)h(v)n(ariable)f(composition)e(with)
759 h(a)i(gi)n(v)o(en)e(array)i(of)g(ne)n(w)f(v)n(ariables.)-189
760 797 y Fo(3)143 b(CNF)35 b(Support)-189 1050 y Fj(3.1)119
761 b(F)m(ormat)-189 1237 y Fl(Gi)n(v)o(en)30 b(a)h(BDD)g(representing)g(a)
762 g(function)f Fd(f)11 b Fl(,)32 b(we)f(de)n(v)o(elop)f(three)h(basic)g
763 (possible)e(w)o(ays)i(to)g(store)f(it)h(as)g(a)g(CNF)-189
764 1358 y(formula.)54 b(In)33 b(each)h(method)d(the)i(set)g(of)f(clauses)h
765 (is)f(written)h(after)g(an)g(header)g(part.)55 b(Only)32
766 b(the)h(te)o(xt)f(format)g(is)-189 1478 y(allo)n(wed.)-189
767 1743 y Fi(3.1.1)99 b(Header)-189 1931 y Fl(The)23 b(header)h(part)f(of)
768 g(each)h(CNF)g(\002le)f(has)g(basically)g(the)f(same)h(format)g
769 (analyzed)g(for)h(the)f(BDD/ADD)g(\002les.)30 b(F)o(or)-189
770 2051 y(e)o(xample)h(the)g Fg(.rootids)f Fl(line)h(indicates)f(the)i(be)
771 o(ginning)d(of)j(each)g(CNF)g(formula)f(represented)h(by)f(a)h(single)
772 -189 2172 y(BDD.)j(T)-8 b(o)34 b(be)g(compatible)f(with)h(the)g(DIMA)l
773 (CS)h(format)f(each)h(header)f(line)g(start)g(with)g(the)g(character)h
774 (\223c\224)g(to)-189 2292 y(indicate)24 b(a)h(comment.)-189
775 2557 y Fi(3.1.2)99 b(T)-9 b(ext)25 b(F)n(ormat)-189 2745
776 y Fl(The)j(\002rst)g(method,)g(which)f(we)h(call)g Fi(Single-Node-Cut)p
777 Fl(,)j(models)26 b(each)j(BDD)f(nodes,)h(b)n(ut)e(the)h(ones)f(with)h
778 (both)-189 2865 y(the)c(children)g(equal)h(to)f(the)g(constant)g(node)g
779 Fb(1)p Fl(,)g(as)h(a)g(multiple)o(x)o(er)-5 b(.)27 b(Each)e(multiple)o
780 (x)o(er)d(has)i(tw)o(o)g(data)h(inputs)e(\(i.e.,)-189
781 2985 y(the)k(node)h(children\),)f(a)h(selection)f(input)f(\(i.e.,)i
782 (the)g(node)f(v)n(ariable\))g(and)h(one)f(output)f(\(i.e.,)i(the)g
783 (function)e(v)n(alue\))-189 3106 y(whose)h(v)n(alue)f(is)h(assigned)f
784 (to)h(an)g(additional)f(CNF)i(v)n(ariable.)37 b(The)27
785 b(\002nal)h(number)e(of)h(v)n(ariables)g(is)f(equal)h(to)g(the)-189
786 3226 y(number)d(of)h(original)f(BDD)h(v)n(ariables)f(plus)g(the)h
787 (number)f(of)h(\223internal\224)g(nodes)f(of)h(the)g(BDD.)47
788 3346 y(The)k(second)f(method,)g(which)h(we)f(call)h Fi(Maxterm-Cut)p
789 Fl(,)h(create)g(clauses)e(starting)g(from)g Fd(f)39 b
790 Fl(corresponds)-189 3467 y(to)25 b(the)h(of)n(f-set)g(\(i.e.,)f(all)h
791 (the)g(paths-cubes)f(from)g(the)h(root)g(node)f(to)h(the)f(terminal)g
792 Fg(0)p Fl(\))h(of)g(the)g(function)e Fd(f)11 b Fl(.)34
793 b(W)l(ithin)-189 3587 y(the)29 b(BDD)g(for)g Fd(f)11
794 b Fl(,)30 b(such)f(clauses)f(are)i(found)e(by)h(follo)n(wing)e(all)i
795 (the)f(paths)h(from)f(the)h(root)g(node)f(of)h(the)g(BDD)g(to)-189
796 3708 y(the)c(constant)f(node)g Fb(0)p Fl(.)31 b(The)25
797 b(\002nal)g(number)f(of)h(v)n(ariables)f(is)g(equal)h(to)f(the)h
798 (number)f(of)h(original)f(BDD)h(v)n(ariables.)47 3828
799 y(The)k(third)g(method,)g(which)g(we)g(call)g Fi(A)-5
800 b(uxiliary-V)c(ariable-Cut)p Fl(,)30 b(is)f(a)h(trade-of)n(f)f(between)
801 g(the)g(\002rst)g(tw)o(o)-189 3948 y(strate)o(gies.)69
802 b(Internal)37 b(v)n(ariables,)j(i.e.,)h(cutting)c(points,)j(are)e
803 (added)g(in)f(order)h(to)g(decompose)f(the)h(BDD)g(into)-189
804 4069 y(multiple)27 b(sub-trees)i(each)h(of)f(which)f(is)h(stored)g
805 (follo)n(wing)e(the)h(second)h(strate)o(gy)-6 b(.)42
806 b(The)29 b(trade-of)n(f)g(is)g(guided)f(by)-189 4189
807 y(the)23 b(cutting)f(point)g(selection)g(strate)o(gy)-6
808 b(,)22 b(and)h(we)g(e)o(xperiment)f(with)g(tw)o(o)g(methodologies.)28
809 b(In)23 b(the)g(\002rst)g(method,)g(a)-189 4310 y(ne)n(w)f(CNF)h(v)n
810 (ariable)f(is)f(inserted)h(in)g(correspondence)g(to)g(the)g(shared)g
811 (nodes)g(of)g(the)h(BDD,)f(i.e.,)h(the)f(nodes)f(which)-189
812 4430 y(ha)n(v)o(e)29 b(more)g(than)h(one)f(incoming)f(edge.)45
813 b(This)29 b(technique,)h(albeit)e(optimizing)g(the)h(number)g(of)h
814 (literals)e(stored,)-189 4550 y(can)35 b(produce)g(clauses)f(with)g(a)h
815 (high)f(number)h(of)f(literals)1894 4514 y Fh(2)1933
816 4550 y Fl(.)60 b(T)-8 b(o)35 b(a)n(v)n(oid)f(this)g(dra)o(wback,)j(the)
817 e(second)f(method,)-189 4671 y(introduces)28 b(all)g(the)g(pre)n
818 (viously)e(indicated)i(cutting)f(points)g(more)h(the)h(ones)f
819 (necessary)g(to)g(break)h(the)f(length)g(of)-189 4791
820 y(the)d(path)f(to)h(a)g(maximum)e(\(user\))i(selected)g(v)n(alue.)47
821 4911 y(Actually)-6 b(,)37 b(all)f(the)f(methods)g(described)h(abo)o(v)o
822 (e)e(can)j(be)e(re-conducted)h(to)g(the)f(basic)h(idea)g(of)g(possibly)
823 -189 5032 y(breaking)24 b(the)h(BDD)g(through)f(the)g(use)h(of)f
824 (additional)g(cutting)f(v)n(ariables)h(and)h(dumping)e(the)h(paths)g
825 (between)h(the)-189 5152 y(root)34 b(of)h(the)f(BDD,)h(the)g(cutting)e
826 (v)n(ariables)h(and)g(the)h(terminal)e(nodes.)60 b(Such)35
827 b(internal)f(cutting)f(v)n(ariables)h(are)-189 5273 y(added)25
828 b(al)o(w)o(ays)f(\(for)i(each)f(node\),)g(ne)n(v)o(er)f(or)h(sometimes)
829 e(respecti)n(v)o(ely)-6 b(.)p -189 5360 1607 4 v -77
830 5422 a Ff(2)-40 5452 y Fe(This)27 b(v)n(alue)f(is)i(superiorly)d
831 (limited)h(by)g(the)h(number)e(of)h(v)n(ariables)g(of)g(the)h(BDD,)g
832 (i.e.,)h(the)f(longest)f(path)g(from)g(the)h(root)f(to)g(the)-189
833 5551 y(terminal)19 b(node.)1794 5800 y Fl(7)p eop
835 8 7 bop 47 218 a Fl(While)33 b(the)f Fc(Single-Node-Cut)h
836 Fl(method)f(minimizes)f(the)i(length)f(of)h(the)f(clauses)h(produced,)i
837 (b)n(ut)d(it)g(also)-189 338 y(requires)d(the)h(higher)f(number)g(of)g
838 (CNF)i(v)n(ariables,)e(the)h Fc(Maxterm-Cut)f Fl(technique)g(minimizes)
839 f(the)h(number)g(of)-189 459 y(CNF)36 b(v)n(ariables)d(required.)61
840 b(This)34 b(adv)n(antage)g(is)g(counter)n(-balanced)h(by)f(the)h(f)o
841 (act)g(that)f(in)g(the)h(w)o(orst)f(case)h(the)-189 579
842 y(number)23 b(of)g(clauses,)g(as)h(well)e(as)i(the)f(total)f(number)h
843 (of)g(literals,)g(produced)g(is)g(e)o(xponential)e(in)i(the)g(BDD)h
844 (size)f(\(in)-189 699 y(terms)28 b(of)i(number)e(of)h(nodes\).)43
845 b(The)29 b(application)f(of)h(this)f(method)g(is)g(then)h(limited)e(to)
846 i(the)g(cases)g(in)f(which)h(the)-189 820 y(\223of)n(f-set\224)c(of)f
847 (the)g(represented)h(function)f Fd(f)35 b Fl(has)24 b(a)h(small)f
848 (cardinality)-6 b(.)29 b(The)c Fc(A)n(uxiliary-V)-11
849 b(ariable-Cut)22 b Fl(strate)o(gy)h(is)-189 940 y(a)k(trade-of)n(f)h
850 (between)f(the)g(\002rst)g(tw)o(o)g(methods)f(and)h(the)g(ones)f(which)
851 h(gi)n(v)o(es)f(more)h(compact)f(results.)37 b(As)27
852 b(a)h(\002nal)-189 1061 y(remark)f(notice)e(that)h(the)g(method)g(is)f
853 (able)i(to)f(store)g(both)f(monolithic)f(BDDs)j(and)f(conjuncti)n(v)o
854 (e)e(forms.)35 b(In)26 b(each)-189 1181 y(case)f(we)g(generate)h(CNF)f
855 (\002les)g(using)f(the)h(standard)f(DIMA)l(CS)i(format.)-189
856 1365 y Fi(Example)f(1)49 b Fc(F)l(igur)l(e)20 b(1)h(shows)f(an)h(e)n
857 (xample)g(of)f(how)h(our)f(pr)l(ocedur)l(e)h(works)f(to)h(stor)l(e)f(a)
858 h(small)f(monolithic)f(BDD.)-189 1486 y(F)l(igur)l(e)j(1\(a\))h(r)l
859 (epr)l(esents)g(a)g(BDD)g(with)g Fb(4)g Fc(nodes.)30
860 b(BDD)23 b(variables)f(ar)l(e)h(named)g(after)f(inte)l(g)o(er)g(number)
861 o(s)h(r)o(anging)-189 1606 y(fr)l(om)k Fb(1)h Fc(to)g
862 Fb(4)p Fc(,)h(to)f(have)g(an)g(easy-to-follow)f(corr)l(espondence)h
863 (with)g(the)g(CNF)h(variables.)40 b(F)l(igur)l(e)27 b(1\(b\),)i(\(c\))g
864 (and)-189 1727 y(\(d\))c(show)g(the)f(corr)l(esponding)f(CNF)j(r)l(epr)
865 l(esentations)d(g)o(ener)o(ated)h(by)h(our)f(thr)l(ee)h(methods.)30
866 b(As)24 b(in)h(the)f(standar)l(d)-189 1847 y(format)i
867 Fa(p)i Fc(indicates)e(the)h(total)f(number)g(of)h(variables)f(used)h
868 (\()p Fb(4)g Fc(is)g(the)g(minimum)f(value)h(as)g(the)g(BDD)g(itself)f
869 (has)-189 1967 y Fb(4)f Fc(variables\),)e(and)i Fa(cnf)g
870 Fc(the)f(total)g(number)g(of)h(clauses.)47 2088 y(As)i(a)g(\002nal)f(r)
871 l(emark)h(notice)f(that)g(for)g(this)g(speci\002c)h(e)n(xample)g(the)f
872 (\223Maxterm-Cut\224)i(appr)l(oac)o(h)d(is)h(the)h(one)-189
873 2208 y(whic)o(h)36 b(gives)g(the)g(most)f(compact)h(CNF)h(r)l(epr)l
874 (esentation)e(b)n(ut)h(also)f(the)h(clause)g(with)g(the)g(lar)l(g)o
875 (est)g(number)f(of)-189 2328 y(liter)o(als)23 b(\()p
876 Fb(4)p Fc(\).)188 2471 y
877 6339814 10777681 0 0 11709153 19997655 startTexFig
879 %%BeginDocument: bdd.eps
880 %!PS-Adobe-2.0 EPSF-2.0
882 %%Creator: fig2dev Version 3.2 Patchlevel 3c
883 %%CreationDate: Mon Sep 9 14:21:26 2002
884 %%For: quer@pcsq (Stefano Quer)
885 %%BoundingBox: 0 0 178 304
886 %%Magnification: 1.0000
888 /$F2psDict 200 dict def
890 $F2psDict /mtrx matrix put
891 /col-1 {0 setgray} bind def
892 /col0 {0.000 0.000 0.000 srgb} bind def
893 /col1 {0.000 0.000 1.000 srgb} bind def
894 /col2 {0.000 1.000 0.000 srgb} bind def
895 /col3 {0.000 1.000 1.000 srgb} bind def
896 /col4 {1.000 0.000 0.000 srgb} bind def
897 /col5 {1.000 0.000 1.000 srgb} bind def
898 /col6 {1.000 1.000 0.000 srgb} bind def
899 /col7 {1.000 1.000 1.000 srgb} bind def
900 /col8 {0.000 0.000 0.560 srgb} bind def
901 /col9 {0.000 0.000 0.690 srgb} bind def
902 /col10 {0.000 0.000 0.820 srgb} bind def
903 /col11 {0.530 0.810 1.000 srgb} bind def
904 /col12 {0.000 0.560 0.000 srgb} bind def
905 /col13 {0.000 0.690 0.000 srgb} bind def
906 /col14 {0.000 0.820 0.000 srgb} bind def
907 /col15 {0.000 0.560 0.560 srgb} bind def
908 /col16 {0.000 0.690 0.690 srgb} bind def
909 /col17 {0.000 0.820 0.820 srgb} bind def
910 /col18 {0.560 0.000 0.000 srgb} bind def
911 /col19 {0.690 0.000 0.000 srgb} bind def
912 /col20 {0.820 0.000 0.000 srgb} bind def
913 /col21 {0.560 0.000 0.560 srgb} bind def
914 /col22 {0.690 0.000 0.690 srgb} bind def
915 /col23 {0.820 0.000 0.820 srgb} bind def
916 /col24 {0.500 0.190 0.000 srgb} bind def
917 /col25 {0.630 0.250 0.000 srgb} bind def
918 /col26 {0.750 0.380 0.000 srgb} bind def
919 /col27 {1.000 0.500 0.500 srgb} bind def
920 /col28 {1.000 0.630 0.630 srgb} bind def
921 /col29 {1.000 0.750 0.750 srgb} bind def
922 /col30 {1.000 0.880 0.880 srgb} bind def
923 /col31 {1.000 0.840 0.000 srgb} bind def
927 newpath 0 304 moveto 0 0 lineto 178 0 lineto 178 304 lineto closepath clip newpath
928 -51.0 319.0 translate
931 /cp {closepath} bind def
932 /ef {eofill} bind def
933 /gr {grestore} bind def
936 /rs {restore} bind def
939 /rm {rmoveto} bind def
940 /n {newpath} bind def
943 /slc {setlinecap} bind def
944 /slj {setlinejoin} bind def
945 /slw {setlinewidth} bind def
946 /srgb {setrgbcolor} bind def
947 /rot {rotate} bind def
949 /sd {setdash} bind def
950 /ff {findfont} bind def
951 /sf {setfont} bind def
952 /scf {scalefont} bind def
953 /sw {stringwidth} bind def
954 /tr {translate} bind def
955 /tnt {dup dup currentrgbcolor
956 4 -2 roll dup 1 exch sub 3 -1 roll mul add
957 4 -2 roll dup 1 exch sub 3 -1 roll mul add
958 4 -2 roll dup 1 exch sub 3 -1 roll mul add srgb}
960 /shd {dup dup currentrgbcolor 4 -2 roll mul 4 -2 roll mul
961 4 -2 roll mul srgb} bind def
969 /savematrix mtrx currentmatrix def
970 x y tr xrad yrad sc 0 0 1 startangle endangle arc
975 /$F2psBegin {$F2psDict begin /$F2psEnteredState save def} def
976 /$F2psEnd {$F2psEnteredState restore end} def
987 n 2010 4515 m 2550 4515 l 2550 5040 l 2010 5040 l
989 /Times-Roman ff 300.00 scf sf
991 gs 1 -1 sc (1) col0 sh gr
993 n 1515 1800 270 270 0 360 DrawEllipse gs col0 s gr
996 n 2250 900 270 270 0 360 DrawEllipse gs col0 s gr
999 n 2970 2715 270 270 0 360 DrawEllipse gs col0 s gr
1002 n 2280 3705 270 270 0 360 DrawEllipse gs col0 s gr
1006 n 3555 3555 64 64 0 360 DrawEllipse gs 0.00 setgray ef gr gs col0 s gr
1009 n 2712 1726 64 64 0 360 DrawEllipse gs 0.00 setgray ef gr gs col0 s gr
1012 n 2430 4230 64 64 0 360 DrawEllipse gs 0.00 setgray ef gr gs col0 s gr
1017 2250 3450 l gs col0 s gr
1021 2940 2472 m 3010 2445 l 2931 2239 l 2957 2411 l 2861 2266 l cp
1024 2970 2445 l gs col0 s gr gr
1027 n 2861 2266 m 2957 2411 l 2931 2239 l 2908 2284 l 2861 2266 l
1028 cp gs 0.00 setgray ef gr col0 s
1031 1478 1511 m 1528 1568 l 1693 1422 l 1542 1506 l 1643 1366 l cp
1034 1515 1530 l gs col0 s gr gr
1037 n 1643 1366 m 1542 1506 l 1693 1422 l 1643 1416 l 1643 1366 l
1038 cp gs 0.00 setgray ef gr col0 s
1041 2212 645 m 2287 645 l 2287 425 l 2250 594 l 2212 425 l cp
1044 2250 630 l gs col0 s gr gr
1047 n 2212 425 m 2250 594 l 2287 425 l 2250 459 l 2212 425 l
1048 cp gs 0.00 setgray ef gr col0 s
1052 2692 2664 m 2732 2601 l 2546 2485 l 2670 2606 l 2506 2548 l cp
1055 2700 2625 l gs col0 s gr gr
1058 n 2506 2548 m 2670 2606 l 2546 2485 l 2555 2534 l 2506 2548 l
1059 cp gs 0.00 setgray ef gr col0 s
1064 2504 4653 m 2539 4720 l 2733 4616 l 2567 4663 l 2698 4550 l cp
1066 n 3180 2910 m 3181 2911 l 3183 2913 l 3186 2916 l 3192 2921 l 3200 2929 l
1067 3210 2939 l 3223 2951 l 3238 2966 l 3255 2984 l 3274 3003 l
1068 3295 3025 l 3317 3049 l 3339 3075 l 3362 3103 l 3385 3131 l
1069 3407 3161 l 3429 3192 l 3450 3225 l 3470 3258 l 3488 3293 l
1070 3504 3329 l 3519 3367 l 3531 3406 l 3541 3447 l 3548 3490 l
1071 3552 3536 l 3552 3583 l 3548 3634 l 3540 3686 l 3528 3740 l
1072 3510 3795 l 3490 3844 l 3467 3892 l 3441 3939 l 3413 3985 l
1073 3382 4028 l 3350 4070 l 3317 4110 l 3283 4148 l 3248 4184 l
1074 3211 4219 l 3174 4253 l 3136 4285 l 3098 4316 l 3059 4347 l
1075 3020 4376 l 2980 4405 l 2941 4432 l 2901 4459 l 2862 4484 l
1076 2824 4509 l 2787 4532 l 2751 4554 l 2717 4575 l 2686 4593 l
1077 2657 4610 l 2631 4626 l 2608 4639 l 2589 4650 l 2572 4659 l
1078 2559 4666 l 2550 4672 l
1079 2535 4680 l gs col0 s gr gr
1083 n 2698 4550 m 2567 4663 l 2733 4616 l 2686 4599 l 2698 4550 l
1084 cp gs 0.00 setgray ef gr col0 s
1088 1985 4734 m 2028 4672 l 1847 4548 l 1965 4675 l 1804 4609 l cp
1090 n 1350 2025 m 1349 2026 l 1348 2027 l 1345 2030 l 1340 2035 l 1334 2042 l
1091 1325 2051 l 1314 2063 l 1301 2078 l 1286 2095 l 1268 2114 l
1092 1249 2137 l 1227 2161 l 1205 2188 l 1181 2218 l 1156 2249 l
1093 1131 2282 l 1105 2316 l 1080 2352 l 1054 2390 l 1029 2428 l
1094 1005 2468 l 981 2509 l 959 2552 l 938 2595 l 918 2640 l
1095 900 2687 l 884 2736 l 870 2786 l 858 2839 l 848 2894 l
1096 841 2951 l 837 3011 l 836 3074 l 838 3139 l 845 3206 l
1097 855 3275 l 870 3345 l 888 3412 l 910 3477 l 934 3542 l
1098 961 3604 l 990 3665 l 1022 3723 l 1054 3779 l 1088 3833 l
1099 1124 3885 l 1160 3935 l 1198 3983 l 1236 4029 l 1275 4074 l
1100 1315 4118 l 1356 4160 l 1397 4201 l 1438 4241 l 1480 4280 l
1101 1522 4318 l 1563 4355 l 1605 4390 l 1645 4424 l 1685 4457 l
1102 1723 4488 l 1760 4517 l 1795 4545 l 1827 4570 l 1857 4593 l
1103 1884 4613 l 1909 4632 l 1930 4647 l 1947 4660 l 1962 4671 l
1104 1973 4679 l 1982 4686 l
1105 1995 4695 l gs col0 s gr gr
1109 n 1804 4609 m 1965 4675 l 1847 4548 l 1854 4598 l 1804 4609 l
1110 cp gs 0.00 setgray ef gr col0 s
1115 2300 4492 m 2363 4532 l 2481 4347 l 2359 4470 l 2417 4307 l cp
1117 n 2340 3960 m 2341 3962 l 2344 3966 l 2348 3973 l 2354 3982 l 2362 3995 l
1118 2370 4010 l 2379 4028 l 2389 4046 l 2397 4066 l 2406 4088 l
1119 2413 4111 l 2420 4137 l 2425 4165 l 2429 4197 l 2430 4230 l
1120 2429 4263 l 2425 4295 l 2420 4323 l 2413 4349 l 2406 4372 l
1121 2397 4394 l 2389 4414 l 2379 4433 l 2370 4450 l 2362 4465 l
1123 2340 4500 l gs col0 s gr gr
1127 n 2417 4307 m 2359 4470 l 2481 4347 l 2431 4356 l 2417 4307 l
1128 cp gs 0.00 setgray ef gr col0 s
1132 2136 4532 m 2199 4492 l 2082 4307 l 2141 4470 l 2018 4347 l cp
1134 n 2160 3960 m 2159 3962 l 2156 3966 l 2152 3973 l 2146 3982 l 2138 3995 l
1135 2130 4010 l 2121 4028 l 2111 4046 l 2103 4066 l 2094 4088 l
1136 2087 4111 l 2080 4137 l 2075 4165 l 2071 4197 l 2070 4230 l
1137 2071 4263 l 2075 4295 l 2080 4323 l 2087 4349 l 2094 4372 l
1138 2103 4394 l 2111 4414 l 2121 4433 l 2130 4450 l 2138 4465 l
1140 2160 4500 l gs col0 s gr gr
1144 n 2018 4347 m 2141 4470 l 2082 4307 l 2068 4356 l 2018 4347 l
1145 cp gs 0.00 setgray ef gr col0 s
1146 /Times-Roman ff 300.00 scf sf
1148 gs 1 -1 sc (1) col0 sh gr
1149 /Times-Roman ff 300.00 scf sf
1151 gs 1 -1 sc (2) col0 sh gr
1152 /Times-Roman ff 300.00 scf sf
1154 gs 1 -1 sc (3) col0 sh gr
1155 /Times-Roman ff 300.00 scf sf
1157 gs 1 -1 sc (4) col0 sh gr
1164 531 3990 a Fc(\(a\))1512 2504 y Fg(p)60 b(cnf)f(7)g(11)1512
1165 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)
1166 1512 2985 y(6)h(-2)f(0)1512 3106 y(6)h(-5)f(0)1512 3226
1167 y(-6)g(2)h(5)f(0)1512 3347 y(7)h(1)f(5)h(0)1512 3467
1168 y(-7)f(1)h(-5)f(0)1512 3587 y(7)h(-1)f(-6)g(0)1512 3708
1169 y(-7)g(-1)h(6)f(0)1512 3828 y(7)h(0)1836 3990 y Fc(\(b\))2541
1170 2525 y Fg(p)f(cnf)g(4)h(3)2541 2645 y(1)f(-3)h(-4)f(0)2541
1171 2766 y(-1)g(2)h(3)f(0)2541 2886 y(-1)g(2)h(-3)f(4)h(0)2868
1172 3048 y Fc(\(c\))2541 3251 y Fg(p)f(cnf)g(5)h(5)2541 3371
1173 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)
1174 2541 3733 y(3)f(-5)h(0)2541 3853 y(-3)f(4)h(-5)f(0)2865
1175 3990 y Fc(\(d\))-189 4138 y Fl(Figure)46 b(1:)71 b(\(a\))47
1176 b(BDD;)e(\(b\))h(\223Single-Node-Cut\224)g(format;)55
1177 b(\(c\))46 b(\223Maxterm-Cut\224)g(format;)55 b(\(d\))45
1178 b(\223)-8 b(Auxiliary-)-189 4258 y(V)d(ariable-Cut\224)25
1179 b(F)o(ormat.)-189 4625 y Fj(3.2)119 b(Implementation)-189
1180 4813 y Fl(Store)25 b(and)g(Load)g(for)g(a)g(single)f(BDD)h(or)g(a)g
1181 (forest)g(of)g(BDDs)g(is)f(currently)h(implemented.)-189
1182 5073 y Fi(3.2.1)99 b(Storing)25 b(Decision)g(Diagrams)f(as)g(CNF)h(F)n
1183 (ormulas)-189 5260 y Fl(As)g(f)o(ar)g(as)g(the)g(storing)e(process)i
1184 (is)f(concerned)i(three)f(possible)e(formats)h(are)i(a)n(v)n(ailable:)
1185 -44 5431 y Fk(\017)49 b Fl(DDDMP)p 421 5431 30 4 v 36
1186 w(CNF)p 650 5431 V 36 w(MODE)p 980 5431 V 35 w(NODE:)21
1187 b(store)f(a)h(BDD)h(by)e(introducing)f(an)i(auxiliary)g(v)n(ariable)f
1188 (for)h(each)g(BDD)55 5551 y(node)1794 5800 y(8)p eop
1190 9 8 bop -44 218 a Fk(\017)49 b Fl(DDDMP)p 421 218 30
1191 4 v 36 w(CNF)p 650 218 V 36 w(MODE)p 980 218 V 35 w(MAXTERM:)20
1192 b(store)g(a)h(BDD)h(by)e(follo)n(wing)f(the)h(maxterm)g(of)h(the)g
1193 (represented)55 338 y(function)-44 542 y Fk(\017)49 b
1194 Fl(DDDMP)p 421 542 V 36 w(CNF)p 650 542 V 36 w(MODE)p
1195 980 542 V 35 w(BEST)-5 b(:)32 b(trade-of)f(between)h(the)f(tw)o(o)f
1196 (pre)n(vious)g(solution,)h(trying)f(to)h(optimize)55
1197 662 y(the)25 b(number)f(of)h(literals)f(stored.)-189
1198 865 y(See)c(procedures)f(Dddmp)p 736 865 V 35 w(cuddBddStoreCnf)g(\(to)
1199 g(store)f(a)h(single)f(BDD)i(as)e(a)i(CNF)f(formula\))g(and)g(Dddmp)p
1200 3609 865 V 34 w(cuddBddArrayStoreCnf)-189 986 y(\(to)25
1201 b(store)f(an)h(array)h(of)f(BDDs)g(as)f(a)i(CNF)f(formula\).)-189
1202 1252 y Fi(3.2.2)99 b(Loadinf)26 b(CNF)e(F)n(ormulas)g(as)h(BDDs)-189
1203 1439 y Fl(As)g(f)o(ar)g(as)g(the)g(loading)e(process)i(is)f(concerned)i
1204 (three)f(possible)e(formats)i(are)g(a)n(v)n(ailable:)-44
1205 1643 y Fk(\017)49 b Fl(DDDMP)p 421 1643 V 36 w(CNF)p
1206 650 1643 V 36 w(MODE)p 980 1643 V 35 w(NO)p 1159 1643
1207 V 36 w(CONJ:)25 b(Return)g(the)f(Clauses)h(without)f(Conjunction)-44
1208 1846 y Fk(\017)49 b Fl(DDDMP)p 421 1846 V 36 w(CNF)p
1209 650 1846 V 36 w(MODE)p 980 1846 V 35 w(NO)p 1159 1846
1210 V 36 w(Q)o(U)l(ANT)-5 b(:)24 b(Return)h(the)g(sets)f(of)h(BDDs)g
1211 (without)f(Quanti\002cation)-44 2050 y Fk(\017)49 b Fl(DDDMP)p
1212 421 2050 V 36 w(CNF)p 650 2050 V 36 w(MODE)p 980 2050
1213 V 35 w(CONJ)p 1264 2050 V 36 w(Q)o(U)l(ANT)-5 b(:)23
1214 b(Return)h(the)g(sets)f(of)h(BDDs)g(AFTER)g(Existential)e(Quanti\002-)
1215 55 2170 y(cation)-189 2373 y(See)e(procedures)f(Dddmp)p
1216 736 2373 V 35 w(cuddBddLoadCnf)f(\(to)h(load)f(a)i(CNF)f(formula)g(as)g
1217 (a)g(single)f(BDD\))h(and)g(Dddmp)p 3581 2373 V 35 w
1218 (cuddBddArrayLoadCnf)-189 2494 y(\(to)35 b(load)h(a)g(CNF)g(formula)f
1219 (as)h(an)g(array)g(of)g(BDDs\).)63 b(See)36 b(also)g(Dddmp)p
1220 2485 2494 V 34 w(cuddHeaderLoadCnf)h(to)e(load)g(the)-189
1221 2614 y(header)25 b(of)g(a)g(CNF)h(\002le)f(to)g(gather)f(information)f
1222 (on)i(the)g(sa)n(v)o(ed)f(structure.)-189 2954 y Fo(4)143
1223 b(T)-13 b(est)35 b(Pr)m(ogram)f(and)h(Regr)m(ession)f(T)-13
1224 b(ests)-189 3177 y Fl(The)20 b Fc(testddmp.c)e Fl(\002le,)j(pro)o
1225 (vided)d(with)h(this)f(distrib)n(ution,)g(e)o(x)o(empli\002es)g(some)h
1226 (of)h(the)f(abo)o(v)o(e)g(features.)29 b(Moreo)o(v)o(er)l(,)-189
1227 3298 y(in)d(the)h Fc(e)n(xp)g Fl(e)o(xperiments)e(a)j(fe)n(w)e
1228 (scripts,)h(named)f Fc(test\241n\277.script)f Fl(are)i(a)n(v)n(ailable)
1229 f(for)h(a)g(sanity)f(check)h(of)g(the)g(tool)-189 3418
1230 y(and)e(to)f(tak)o(e)h(a)g(look)f(at)h(some)f(runs)h(e)o(x)o
1231 (empli\002cation.)-189 3758 y Fo(5)143 b(Documentation)-189
1232 3981 y Fl(F)o(or)27 b(further)f(documentation)f(on)i(the)f(package)h
1233 (see)g(the)g(on-line)f(documentation)f(automatically)g(created)i(from)
1234 -189 4102 y(the)e(source)g(code)g(\002les.)-189 4441
1235 y Fo(6)143 b(Ackno)o(wledgments)-189 4665 y Fl(W)-8 b(e)19
1236 b(are)h(particular)f(indebted)f(with)g(F)o(abio)g(Somenzi,)i(for)f
1237 (discussions,)f(advice,)i(and)f(for)g(including)e(the)i(DDDMP)-189
1238 4785 y(package)28 b(into)f(the)h(CUDD)g(distrib)n(ution.)37
1239 b(W)-8 b(e)29 b(also)e(thank)g(all)h(the)g(user)g(of)g(the)f(package)i
1240 (for)f(their)f(useful)h(indi-)-189 4905 y(cation)c(and)h(comments)f(on)
1241 g(the)h(it.)1794 5800 y(9)p eop
1243 10 9 bop -189 218 a Fo(7)143 b(FTP)35 b(Site)-189 441
1244 y Fl(The)25 b(package)g(is)f(singularly)g(a)n(v)n(ailable)g(from:)-189
1245 645 y Fg(site:)59 b(ftp.polito.it)-189 765 y(user:)g(anonymous)-189
1246 885 y(directory:)f(/pub/research/dddmp)-189 1089 y Fl(or)25
1247 b(directly)f(from)h(the)f(author)h(WEB)g(pages:)-189
1248 1292 y Fg(WWW:)59 b(http://www.polito.it/\230{cabodi)o(,quer)o(})-189
1249 1632 y Fo(8)143 b(F)l(eedback)-189 1855 y Fl(Send)25
1250 b(feedback)h(to:)-189 2059 y Fg(Gianpiero)58 b(Cabodi)g(&)i(Stefano)e
1251 (Quer)-189 2179 y(Politecnico)f(di)j(Torino)-189 2300
1252 y(Dipartimento)d(di)i(Automatica)f(e)i(Informatica)-189
1253 2420 y(Corso)f(Duca)g(degli)f(Abruzzi,)g(24)-189 2540
1254 y(I-10129)g(Torino)-189 2661 y(Italy)-189 2781 y(E-mail:)g
1255 ({cabodi,quer}@polito.it)-189 2901 y(WWW:)h
1256 (http://www.polito.it/\230{cabodi)o(,quer)o(})1769 5800
1260 userdict /end-hook known{end-hook}if