%PDF-1.3
%
149 0 obj
<>/OCGs[152 0 R]>>/OutputIntents[146 0 R]/PageLabels 144 0 R/Pages 15 0 R/Type/Catalog>>
endobj
151 0 obj
<>/Font<>>>/Fields 156 0 R>>
endobj
148 0 obj
<>stream
2016-01-23T19:16:36-08:00
TeX
2016-01-31T20:16:26-08:00
2016-01-31T20:16:26-08:00
This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015) kpathsea version 6.2.1
PDF/X-1a:2001
PDF/X-1:2001
Acrobat Distiller 15.0 (Macintosh)
False
Technical Papers: Knowledge Representation and Reasoning
PDF/X-1a:2001
PDF/X-1:2001
application/pdf
Tomi Janhunen, Shahab Tasharrofi, Eugenia Ternovska
SAT-to-SAT: Declarative Extension of SAT Solvers with New Propagators
Copyright(C) 2016, Association for the Advancement of Artificial Intelligence
Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence (AAAI-16)
Technical Papers: Knowledge Representation and Reasoning
True
http://www.aaai.org
uuid:ac0f130f-c3c4-2042-8f34-c3b8ad0055ff
uuid:081ae066-5c95-9747-ac75-8e0e2b2d1cf0
1
PDF/X-1:2001
endstream
endobj
144 0 obj
<>
endobj
15 0 obj
<>
endobj
2 0 obj
<>/Font<>/ProcSet[/PDF/Text]/XObject<>>>/TrimBox[0 0 612 792]/Type/Page>>
endobj
16 0 obj
<>/Font<>/ProcSet[/PDF/Text]/XObject<>>>/TrimBox[0 0 612 792]/Type/Page>>
endobj
29 0 obj
<>/Font<>/ProcSet[/PDF/Text]/XObject<>>>/TrimBox[0 0 612 792]/Type/Page>>
endobj
33 0 obj
<>/Font<>/ProcSet[/PDF/Text]/XObject<>>>/TrimBox[0 0 612 792]/Type/Page>>
endobj
36 0 obj
<>/Font<>/ProcSet[/PDF/Text]/XObject<>>>/TrimBox[0 0 612 792]/Type/Page>>
endobj
44 0 obj
<>/Font<>/ProcSet[/PDF/Text]/XObject<>>>/TrimBox[0 0 612 792]/Type/Page>>
endobj
47 0 obj
<>/Font<>/ProcSet[/PDF/Text]/XObject<>>>/TrimBox[0 0 612 792]/Type/Page>>
endobj
175 0 obj
<>stream
HWMsHWܲ8l~s%˚؎x-mM!$_@S%gjJ w?9U3ЃNB781ێ
wumf
/Q39jdZ-UCw`
";ͫ1m/WTw~];-ͻYEֹw775_Xؤ\U7Op06Gȷj-3kآXCj@M&+"-/np_X6"%ڱ'`2b&Q"'eOUMV&p~`Evf@5ԊyhVstR^D%mm,+*|~RO*
l`xMQ(ѻW'8iFY7/ע*SPUEHyh(A7l
y.*sl;>5 yÞdX5v#-"GJkdŃ l?v9fX LnXDj!$_dӪ8#DjdBB>[LcV`N&0~PqkI,L.[#D/l{q'f&aǖ1$*QM$@Y쾴.Jx EMP茾$ѶB 2k^`3Y x3v28uHYHL~HFG=n賫`3 TrGļQe ~z];c'6sH֡K'`6u%PBTv`;n=2{XaVȎv$^/3PkB "F]COE?E<$V9]]OֆY|ێe!
!O T$*kRQyY$5a9&{tqgβrL쩱m| w Ym_ᮡY&
7ZVޫUK[f C.\c"ఐz="e^;>D! }Ԭ'ffm)3O^OyS/4 TPIDU7cS -:O,{nSaԃ=~#hhID|Y CDRJ BF{Vۖ#mZsmeJ\n<Ѡy'f.zecN
<xt˒$@
9Jub:ǘF 2PŴ+1ވ.r5i%&O+y_קiҽu_D.F^/ĄgٚwFM%W?!FuNS6|"տ0fKlO3>1 Ԑ{xRC8XT;XN<9-D݃"'3;"9JGS;.]4vL6_@| zx!OZ=m;le]k]^fk\F>nYpJ;KLž-SnBAnӨ0ˌNi{<ȠY4>Ӽ[Kb#L?A lE+A|:]6:ĥbL&Mq̜$'pѧ0Ri# #5.?8!"ǀƌ)r&(1;3m3ӆ1KWl.}? .}mb7-prj[|sJsؽo1!m4"';(ѤZ0#D.ROc5jB0b:z䯥tMgLmڼnA7~#E<..({Үh)C0ՒfPƪ nDC.1C̰*̣8n*6054UNiOZG]l(>tGS.H5/hsRpqy&I_<2w}({7f0 %0 4Y @ 8kڧL&yMЉF;|u#ou5
ؼ
^]16yΡQr\S}ӂiCY0oKPLaJ>EwmCb2-jMCOsK{T.Liє;#]#XM@3Cc[Vm2/՝ad'͏^H%>3GWA \,^]ظP.lf*r~ZoʊD)('GJD.Sx?mTRtҨgږƱQh^d&䅖Tds.A >}TS0M=_N7+ZCW%eUr"v(3̬yVdgDX.ȕ)e^OȪZ5P?JW0V\Ut&2%P3L^73_&mgcS@#B]i}_A,m\#"WEiGÂ+dq>J]M:}m~DDY}vNG9n
t\7Cz#WeTb"fu 9ͻ,Z{ X(r`=HybpSOb+K#hȧVؚsF@T!Kb#T BJ<_7y[pȿ ג
]}`Nchr Ub^M;]5fpjZVki[H=I'u>%=b}E˒g+@!'nR_^ևtvw)1>N&Ǟ@HZ;]/u?7oI]5Sh7?
/Ƨl}R|vAWԟ$.v@e}$R/cK.\rZ
9fT:߿1ILg"\.r-TI[iׂ^(:Cfs]|JLlN
>4%և,vs~vڬi@93ē;Ύ~'*Ƴr-t_FC߸_{4
Ī4KiyI"A@֦EBDM#qe5K(Tfzukw![؍|G97(NS7v}4jcːRGn4{%GR/S6wعlq^zKq%TSA%]j=Y,D6_:żqlV:?vϚ]?#OLW1:gbJL#d%Ćɤ
)>@ jQ1 u:4TvUH6gP^vsrj$,tTJ2gt{vм\zYWqhq
$O:+6JXrxFՑ.3DEϔ H}f\+p-hp 1(9[MƂ⧩d+W;B8auRړ-
BP"C/]7?"2X%
LjdHXk~"2Ng.*f2{?$\Yᥪ~6l79Pʍy N})ۃA)2H}5n\퐑ki_
"B顫
l&܍T-l0@`(-w;^eksiCGOC(@esW2;A1yLt;v\LrlFğHwn?EnN;\ Iy:"[ݸ<$.wkduA^<>6`cjE$_I#m-YB*6:C,}2xKqҎdzƞǝ1bAkxm^u ӻRj ~j}Z킮p1εj]sSgAPB:: jأ\QDz^O$9}% Z~UF8xE4nR}|j@(_uk7?"W:|)\dc&:*Y+mK*IYF =å{1
{~J&8!`y["\~'TcJ~KF|:\Xxȳ*IaN|gd "]cI i7io\HETtpײZ4ucO^Qvyw>#59|G;hFp1ooMpxLYR1
<Ш/X#I|k\5sS.VUQM\BT]$lj= Ôx{Q4VgP٩V48WLflѐ7ʇ#2Ewrj*OcY'; t0ٲW#V<7&^]{Zkk%oe +Xtx3]C>˶{{I
UYcx|*gq{$?zW$==
FMdw6$J@p]Od `U^uC?K.OAѣO)VGDMqlkV
/3U/QW-4|s&?%ZAVB?&RU+c@s÷BE(HAeaQZgUφ=H؟CD!oFd|@pTH#-?PX]8^Et)ߓ AJuOPg:#yxp?l}qǼJux:;=|Z)BA1W{/v
{~gPt^$p# F二 ~mS˓oȠ|;P"C}cwEѶ/.k[fD(*p,*w*?!*0I|"s{D$m^6_\Aza3;֙]\v(W7ʳ a+~ Q\|i;MoP~_mqd4][Ԟۘ2W"\OIb9nF3_O#HVZA%j
]Dt'L2 3:GJfФox8
Ϯ(=LyՌCF؝nBJA} Z[JO87Ʒ Uf@ܲ#Kv% >
endstream
endobj
177 0 obj
<>>>/Resources 180 0 R/Subtype/Form>>stream
H2PHW0PpL R5PH
|d*Db..}̼|ݠҜ"K4.t 5351VIҰ0Tr
0 j
endstream
endobj
178 0 obj
<>
endobj
180 0 obj
<>
endobj
181 0 obj
<>
endobj
150 0 obj
<>
endobj
182 0 obj
<>
endobj
183 0 obj
<>
endobj
184 0 obj
<>stream
H twoQk̄fb$Kb07CD6$&CP1Z Z3TU(mX:cPC-I\9{y'yԨd``2ڠ,c āa
b. zX-!mHRO<> ꤔ䴵֔ ~`uqRnKס ]["Z0(T9σbCdeN~uxnB9%JSOS ̐Ofd VMCX6!?P蒡 X䬢⢂B$$椲|0,)x3
mBܢY3ߨm_}Eb'R~M,m˿I跠BqT::; C0lP`1,Oa
.p(4)8
g{7'xCHQ7zX&LrQ24E"T}h7GatCWP3z~A/1X;EbbTlasj
ǎbc7+