%PDF-1.4
%
9 0 obj
<< /S /GoTo /D (Outline0.1) >>
endobj
12 0 obj
(Introduction)
endobj
13 0 obj
<< /S /GoTo /D (Outline0.1.1.2) >>
endobj
16 0 obj
(Motivation)
endobj
17 0 obj
<< /S /GoTo /D (Outline0.1.2.4) >>
endobj
20 0 obj
(Questions)
endobj
21 0 obj
<< /S /GoTo /D (Outline0.2) >>
endobj
24 0 obj
(Finite Model Generation)
endobj
25 0 obj
<< /S /GoTo /D (Outline0.2.1.8) >>
endobj
28 0 obj
(Higher-Order Logic)
endobj
29 0 obj
<< /S /GoTo /D (Outline0.2.2.13) >>
endobj
32 0 obj
(Translation to Propositional Logic)
endobj
33 0 obj
<< /S /GoTo /D (Outline0.2.3.17) >>
endobj
36 0 obj
(Extensions and Optimizations)
endobj
37 0 obj
<< /S /GoTo /D (Outline0.2.4.18) >>
endobj
40 0 obj
(Case Studies)
endobj
41 0 obj
<< /S /GoTo /D (Outline0.3) >>
endobj
44 0 obj
(Proof-Producing SAT Solvers)
endobj
45 0 obj
<< /S /GoTo /D (Outline0.3.1.23) >>
endobj
48 0 obj
(Propositional Logic, Resolution)
endobj
49 0 obj
<< /S /GoTo /D (Outline0.3.2.27) >>
endobj
52 0 obj
(System Overview)
endobj
53 0 obj
<< /S /GoTo /D (Outline0.3.3.28) >>
endobj
56 0 obj
(Representation of SAT Problems)
endobj
57 0 obj
<< /S /GoTo /D (Outline0.3.4.31) >>
endobj
60 0 obj
(Performance)
endobj
61 0 obj
<< /S /GoTo /D (Outline0.4) >>
endobj
64 0 obj
(Satisfiability Modulo Theories)
endobj
65 0 obj
<< /S /GoTo /D (Outline0.4.1.33) >>
endobj
68 0 obj
(Overview)
endobj
69 0 obj
<< /S /GoTo /D (Outline0.4.2.35) >>
endobj
72 0 obj
(Algorithms)
endobj
73 0 obj
<< /S /GoTo /D (Outline0.4.3.36) >>
endobj
76 0 obj
(Community)
endobj
77 0 obj
<< /S /GoTo /D (Outline0.4.4.38) >>
endobj
80 0 obj
(Future Work)
endobj
81 0 obj
<< /S /GoTo /D [82 0 R /Fit ] >>
endobj
99 0 obj <<
/Length 1093
/Filter /FlateDecode
>>
stream
xWn8}Ẉ
,om.`>-;CFYN4)8gH-OĠJl"@[ŝ@Ke*frq+9T~PQǹX~qnUFs)_l
H'9(ǝW!3zb2Bqe-CnƔ.n;c
rC~ڮә#ey-'067 5
_iAlz[)2
7LY-Zf8ӯ{d-ժL8NXH#N('0XNBIvBro6>^hi0Tm,(!49HZ{\}f?@g8)#AF/>/`Qָ:F90^P:YLǬg6[\@/2q#ϋM_TQ/˙.Y 9
Hy~/`6"6
?-TFsS̀Uh8b!Ymgm)j\_eh#AUb}f\E}PN%UeF뜍:;tAcJ$7R..b39*;
jW. |dTꚧNW'S|եWl#RWwm\QN2OSdtp/q=5C%E,^
/|Jժ*z
Q%ə̊P\3j]+C*!t#1TV5vYpT
nW&/)0MO+hVfRZOf^~
*AQ% :pfeEaD9 6Y}$Uu5xy5S6:ݗy~\DC%tŏӯC:$y&[11
endstream
endobj
82 0 obj <<
/Type /Page
/Contents 99 0 R
/Resources 98 0 R
/MediaBox [0 0 362.835 272.126]
/Trans << /S /R >>
/Parent 106 0 R
/Annots [ 93 0 R 94 0 R 95 0 R 96 0 R 97 0 R ]
>> endobj
83 0 obj <<
/Type /XObject
/Subtype /Form
/BBox [0 0 362.835 3.985]
/FormType 1
/Matrix [1 0 0 1 0 0]
/Resources 107 0 R
/Length 15
/Filter /FlateDecode
>>
stream
xP(
endstream
endobj
107 0 obj <<
/Shading << /Sh << /ShadingType 2 /ColorSpace /DeviceRGB /Domain [0 1] /Coords [0 0.0 0 3.9851] /Function << /FunctionType 2 /Domain [0 1] /C0 [1 1 1] /C1 [0.5 0.5 0.5] /N 1 >> /Extend [false false] >> >>
/ProcSet [ /PDF ]
>> endobj
90 0 obj <<
/Type /XObject
/Subtype /Form
/BBox [0 0 8 8]
/FormType 1
/Matrix [1 0 0 1 0 0]
/Resources 108 0 R
/Length 15
/Filter /FlateDecode
>>
stream
xP(
endstream
endobj
108 0 obj <<
/Shading << /Sh << /ShadingType 3 /ColorSpace /DeviceRGB /Domain [0 1] /Coords [4.00005 4.00005 0.0 4.00005 4.00005 4.00005] /Function << /FunctionType 2 /Domain [0 1] /C0 [0.5 0.5 0.5] /C1 [1 1 1] /N 1 >> /Extend [true false] >> >>
/ProcSet [ /PDF ]
>> endobj
91 0 obj <<
/Type /XObject
/Subtype /Form
/BBox [0 0 16 16]
/FormType 1
/Matrix [1 0 0 1 0 0]
/Resources 109 0 R
/Length 15
/Filter /FlateDecode
>>
stream
xP(
endstream
endobj
109 0 obj <<
/Shading << /Sh << /ShadingType 3 /ColorSpace /DeviceRGB /Domain [0.0 8.00009] /Coords [8.00009 8.00009 0.0 8.00009 8.00009 8.00009] /Function << /FunctionType 3 /Domain [0.0 8.00009] /Functions [ << /FunctionType 2 /Domain [0.0 8.00009] /C0 [0.5 0.5 0.5] /C1 [0.5 0.5 0.5] /N 1 >> << /FunctionType 2 /Domain [0.0 8.00009] /C0 [0.5 0.5 0.5] /C1 [1 1 1] /N 1 >> ] /Bounds [ 4.00005] /Encode [0 1 0 1] >> /Extend [true false] >> >>
/ProcSet [ /PDF ]
>> endobj
89 0 obj <<
/Type /XObject
/Subtype /Form
/BBox [0 0 850.394 8]
/FormType 1
/Matrix [1 0 0 1 0 0]
/Resources 110 0 R
/Length 15
/Filter /FlateDecode
>>
stream
xP(
endstream
endobj
110 0 obj <<
/Shading << /Sh << /ShadingType 2 /ColorSpace /DeviceRGB /Domain [0.0 8.00009] /Coords [0 0.0 0 8.00009] /Function << /FunctionType 3 /Domain [0.0 8.00009] /Functions [ << /FunctionType 2 /Domain [0.0 8.00009] /C0 [1 1 1] /C1 [0.5 0.5 0.5] /N 1 >> << /FunctionType 2 /Domain [0.0 8.00009] /C0 [0.5 0.5 0.5] /C1 [0.5 0.5 0.5] /N 1 >> ] /Bounds [ 4.00005] /Encode [0 1 0 1] >> /Extend [false false] >> >>
/ProcSet [ /PDF ]
>> endobj
92 0 obj <<
/Type /XObject
/Subtype /Form
/FormType 1
/PTEX.FileName (./uc-cl.pdf)
/PTEX.PageNumber 1
/PTEX.InfoDict 111 0 R
/BBox [0 0 290 95]
/Resources <<
/ProcSet [ /PDF /ImageC ]
/ExtGState <<
/R7 112 0 R
>>/XObject <<
/R8 113 0 R
>>>>
/Length 114 0 R
/Filter /FlateDecode
>>
stream
x+T03T0 A(˥d^U`daagi42M̍, DK>W Q
endstream
endobj
111 0 obj
<<
/Producer (GPL Ghostscript 8.63)
/CreationDate (D:20090202135259Z00'00')
/ModDate (D:20090202135259Z00'00')
/Creator (GIMP PostScript file plugin V 1.17 by Peter Kirchgessner)
/Title (uc-cl.eps)
>>
endobj
112 0 obj
<<
/Type /ExtGState
/OPM 1
>>
endobj
113 0 obj
<<
/Subtype /Image
/ColorSpace /DeviceRGB
/Width 289
/Height 94
/BitsPerComponent 8
/Filter /FlateDecode
/DecodeParms <<
/Predictor 15
/Columns 289
/Colors 3
>>
/Length 10211
>>
stream
x] xUյMBbf@H @
X)P,5E~OhP2<Z$mP!Z
2XˠJT !3C{}{sod}^g+L.K[lQghjjjJ-tw~l2_sY( rc{k
Jr'fZٮRoǐ`EOv} Jiϙf4G1cƬ]VJw=Z(Tjq fc*EEF窳eaFV\1(*HT_n๘v%pmh3 є8xhr@~6OUl=QPT?FPVK}iɓhO=r3/G?~'u0h'Ś\d@"l{u_衇蹢:e߷o_Jg'