=Paper= {{Paper |id=None |storemode=property |title=Job Shop Scheduling via Disjunctive Boolean Formulas |pdfUrl=https://ceur-ws.org/Vol-911/03_LANMR12.pdf |volume=Vol-911 |dblpUrl=https://dblp.org/rec/conf/lanmr/ItaMPP12 }} ==Job Shop Scheduling via Disjunctive Boolean Formulas== https://ceur-ws.org/Vol-911/03_LANMR12.pdf
  0123415364789  9 67117
               19
      !"#$%#&'#()#$*#&+#,-./$*,.-./
                  012345627879:;< =1=>874?:4@A8BC<4D2E=
    FGHIJKLLLMHNJOGPMQRSTQOTJOKLUMVWJPMQRSXGJNLJYZOP[K\OIQJHZMLOQS
                           FMXOUWGMPZK]QJHZMLOQ
     ^_`abcdaef23418g5=h4E;i=5>47@j864524=i;86k6Bl4g54641;8
     >4;m=7lm2Em8AA=l:6;=@:2A7;m4l=5k21n;48>6;=g45i=5>;m4g5=h4E;o
     pm4;48>6854i=5>47@j4>gA=j4468178EE=5721n;=;m48@2A2;j=i;m4>
     i=568;26ij21n;m4A=n2E8A54q:254>41;6=i;m4;86k6opm4A48745=i;m4
     g5=h4E;74;45>2146i=548Em;86kBA=n2E8AE=1;5821;62172E8;21n;m472r45s
     41;4>gA=j446lm=E81g45i=5>;m4;86kot8Em4>gA=j44m86866=E28;478
     E=6;i=5g85;2E2g8;21n218;86kB6=;m8;l4m83472r4541;l8j6;=g45i=5>
     ;m4;=;8Ag5=h4E;817l2;m72r4541;E=6;6o
     u4g54641;8>4;m=7i=5g5=E46621n;m4A=n2E8AE=16;5821;6866=E28;47;=
     48Em;86kov:5>4;m=7@:2A768AA;m4g=662@A4l=5k21n;48>68178A6=
     2;6m=l6;m4E=6;866=E28;47l2;m48Eml=5k21n;48>opm4>4;m=78A6=
     w176;m4l=5k21n;48>l2;m>212>:>E=6;i=57=21n;m4;=;8Ag5=h4E;o
     xyz{|b}`~8;26w8@2A2;j?5=@A4>B=@m=g?5=@A4>Bu=5k21np48>6B
     26h:1E;234=5>6
 18961
  & ",&",$",&",",','",'& #,#"
& "#&",),","$,'& 
,#&&,"#"'#&'#,,'",""""#"&#
") & "#,")#,$&#&'&","& ,&,,'&
,#&#"'&&&"&"#&#"& #&'
,#,
    '& ,"##"& "',,""#,,#"",
"'& ,#,&,''#,#',&#& ,,"#"#,
#,# #""/#"&&",
    &),'+"#-#"("'+-($#,,,"#"&"'
,,####$#&'"#"#"",& #&,#&
#'"&##"&",,#"'#&'#"
,#''& "#&""$"&#&"#&","
##"&",,#,,"& #"",&'"&/
#"'#"&
    $&,',&#,#,""#,,#'",
#/'&"),#/'), &,'&",
#/',&&,#,"&,,",'&'"#
,""

                                    ¡¢
    012345672489 8154723 379 42327527482415 23
24 41 52655 6122 5839 652  2655 61 37 23
26555367 8 175785412345865 67578  61561 9 3
5267248462 416 7412677741 68326531 4712525
 814824126567 7 41648699688741 42323 77 7741
 23 74526556123 9 57741235 2655
    3457541 23 379 812415416 !36779
5418 23  554494245 7262415 8148241 9 5774123
265501234589655 4152618523 "954 17 72624157 "
824123 26551 123 17 526541941 683265#
751237 619 23 75941234589655 5379 7
 23 45654123 5874241  683265237345$1824 75
    # 67 41275241824169923 4712 7412652362861
7 2 967$8241967 87 7624 861453 967 23
7$822741523 9486981527641257 6832654123 7$8283
812764152567 276159622 45$1824 7535 23 8152764125761
2654123 7$82 499 6558462 423645$1824 7
    414169945$1824 75 23 26554123 7$8261 81$1824
 961796% 457 &1412345865 23 52'()*%+*23 52 
56245,65541 125 %+2741523 4712 7412652362861
 7 2 923 7$82 8249#349 -'()*%+*23 17 
56245,65541 125+4 53 614712265861 7 2 9
23 7$82
    # 36 5416 23 2 4923 52'()*%+35 ,123
   741265 34838617723 7$8261695 2741 23 741
26 423414 85265541236223 6724846241  683 9 41
62653656,"85234541 62624.6241 499392 23 86145
2 56  16124 64123 74126 5982417855 7
 /8412276156712611648
0 1234352646789:;5<56495:=
> 2? @ ABCDEEEDBFG 652 H7$825I1 7$82JBK @ *LKCDEEEDLKMN+
7 652  2655O6837$82BKP?4577416 741
26 61 683 7412645652  9 5
   O6837$82BKP?8154525 65745 815824 614127112
2655J*LKCDEEEDLKMN+37 4561 776 123 2655 67$824123
4127118 23 415836 62362872641265586112411249699
23 2655231 167 892
   &118763 77818 763*Q&R+SK@*TDU*SK++45492
77751241 6837$82BKP?3 1 541SK77512265561
$4123 9652265 23 7$82 4236584691  96965BKO683 
*VDW+PU*SK+ 6141236223 265W1547829 123 265V3
7818 81527641252 1265567 77512 12345Q&R237323
 531 61  77512567818 7962415342 14252655

                              XY
                                 3

                   2      01          6
                                 4

                                      5


                         78898
                                               7

                       

     !"#$ %&'() $* +,$*$-./01#2 $* 31#45$6(78.9-::&;<"-=>?
$*1 "#!.-1 5#22#";$* <"<$<-:$-./@#1.#2 $<2 .$* <"<$<-:$-./.A;-"#!
131."$<"BC*"-" 11#1*-.% "30#12 !@$* D11#1"#!A;-"!$* E"-:
$-./;<"#91EB91;<$<.131."$!%&$* FGH:-%:"#!7I* !91-$<#"#0
 -5*$-./<./"#C";-"!$* $-./1J9<1.-.$#0 23:#& .$*1#9B*#9$<$.
310#12-"57
    K $LMNOPQORQSSSQOTU% -.$#0G%##:-"V-1<-%:.;-5*V-1<-%:O(WL
131."$.-" 23:#& 01#2-5#23-"&7>XYZ[\]X<. <$*1-V-1<-%:#1-"B-$!
V-1<-%:7I* %-1#V1$* V-1<-%:;O0#1<".$-"5;C<::!"#$ -"B-$!V-1<-%:7
^#2 $<2 .;C -:.#9. _-.$* "B-$!#31-$#17K $`MNOPQ_OPQSSSQOTQ_OTU
% $* .$#0:<$1-:.#V1-.$#0V-1<-%:.L;-"!:$a-"!b% $C#5#".$-"$.
$*-$131."$$* c]Xd[-"!Z\e[V-:9.;1.35$V-1<-%: OWL -33-1.<"-5:-9. #1-3*1-. k<0O#1O<.-"
 :2 "$#0k7K $h@kAMNOWLxOlppolrnwGkU7
    >5#"49"5$+,{s<.-yz5#",
$-<"<"B#":&+,5:-9..7>!<.49"5$
+,=s<.-|z5#"$-<"<"B#":&+,3*1-..7
    >"-.."]ddY[Z5-"% 5#"...92<"B-:.#-3*1-. p-.-.$#0:<$1-:.;p<..-$<.E!%&-"-..?@./69 937324909 0318
-./ 603198026963138)109604 67>?@./3 A= 9BC./3
D>?@./D 9 082610469537>?@./ >?@834 316961298E
616167 00324 B>?@3)1961834 3169373)1961
9 1)83732437 212318-./ C834 60406
FGE349 834
H IJKLMLNOPQRSTQUVQWJX
 Y3E32)461834 01 738)409200937Z[3.)496E
83[9/\34\78]]]8\^:93 2)4231_ 061385_ 435 
`0[3.3883[9/\a6738 25Za31)961 90b\a3.ca78]]]8ca^d/3
98 60e)1960438280319 90b619 0 83[9 90b.caf/
88199 gE990b379 [3\a
   `090bcah00360920836196 iah012 083[9\a)9
 0612738 02) 96 jca= 9ah  9 908996 7382)4619
90bcah+38k3l8]]]8Z9 9390496 909083[9\a1 273834961
0446990b66934963196 012696213920@a'64@$a2139
9 93904908261195?a61382893061 9 40990b\a mno
   = 9pqr  9 0b01.9390434963196 379 )496E83[95E
9/012@$  9 93904908261379 59 )496E3[961 396E
6s09631834 316983)4561126102)4 379 Z83[9909
6166s9 0b010129 93904908261 mtou393[96101
738)409206166s619 734430617)19631v
   w73pqr 3x!     64a^ yiap Dk ml]]]Zo:
   w93@$3z^ m_!6.d|8ap dyiap }jca/o
              a{7         d     d

   *383809 301621436183[901 9349610251060059
26~819038b619093341 9 8e)68 1937083[9 3016
01 0169 90~738 25Z 435 060 06442139 59 9v
34678]]]86^:
   (1809604186083[9\a 3)42 034626126~819
0059096 090b619 83[901 8046s2526~819 435 
.038b6190/1226~8193908 0443092038261939 0896609631
37 435 738873861029861290b

                               
   0123452678396962 269 5692 352819 8262259223
 96 29 9 22682 39 98 964 83 33982
92138 8231225922319435688521943
9568852  1983962279568852 96526968123
     692 2635695932123322899 9696823!32 9
1262368893872 962134162368893 62962 968912
5!888239 259223  1262"486223143!2 958312 812
5692#962$52 8 9 623688994 !21925922317212
32 !8882396193528%259223996899526872 
812191262&226  98 964 8323!8312 96 22688
1262 893185 9259223 98 22682 3
   0125692 26 2%2334162368893'5!888239662"486223(96
2138125692#962$52282812 9983231
9 293683!222 5869 259223
)*+,-.'/(0&8 8231883  9611225922/568852
81246623
)*+,1.'/2/3(0012 432834383%!212/45  /3458 88
1281269 12259223/96/3435688528122961!91
!2912322
)*+,6.'/27/3(0012 432834383%!212/458/349&8 823
18/383912212/3194 !2912322&1232 
8/839812212/3439!288
)*+,:.'7/27/3(0012 432834383%!28/498/3 498 88
128126/96/32592233194 95688528122!919 12
3194 90143243 798 178!91259223812322
;,<<*-=>?@A?BCDECEFG@GEHBIJEDKLIB@M?HNBHA?@DBHFIB@?OGHBIEPGNBI
?QLGRBI?H@JEDKLIB?SCD?FF?OGHOGFTLHN@GR?JEDKUVWX
   Y968912562789432 1298 93683872!122 26
9 125692!262682 3 834872 9630122 3398281
2139 5692 83487296Z'(181 292312 8262
9682318152696123
   [ 1 83487296Z'(!29 8%2 78 72969 \59388939 95
  ]9 9689125938899 212592212 281265688529
568852961243956885281246629682
   012329 7296392 9621 83489 69 Z'(996 12693
9  68$^014321313 33982  68$^98812
 826234!2318152696129662359 83
   & 298'81129489952696(12_ 834872 96312
2569593889 964 `4Z'a(8Z'b(80008Z'c(83 962`
8 !2 94899 834872 963#46126962  33821
383%23`62562323  9 96 569526968218 2$24212
9 5692

                                de
   0123452446718928891 28 2855217 3511246812785 157
282492421 548289128582354845712 5858915
81279 9 21135 89185823 518
   91151 !" 5824233891 54431812748928 2157185
 7 31718891 5181#181301 1418 891533541859585
63891418 !"2234595851817 189175135!897 767
 548
$ % &'()*+,-.'*/01./2'3'.4 5'.6)7(8/+49
: 28 632 127 315;916335 891587 <28551456 144857 =
 7 <1 5484> 164851 518?@ ABCDDDCAE"911129824AFGH924
2445 2812418555312 5482841 26325531257632!9541
75134 1 1418891812749 9 21135 89185823 518I295
8127 4 1 14181275135!
   J89541751345!89135 232361K  281489282 28 632 17 3511
764812 57 5185891581278912361L1 144148928891 5=
 14517 3511725812 28589158127012345641891
2361=K85  2818928891 1418117 3511764858 28 281 8928
58127
   91 548284 289 917 351145631135 2824AFGH21
8243281 2468157MN AF";69MN AF"1 14414891#11824
85 157891824AF4589157632 3614891#1184681274 9 2
 157891824I29468157 MN AF"4151895692 552
7285 548284158124OP
   Q51 14182718958563891751349 94284233891 5=
48284855891 518R 481 14188231K8917638 3281 28814
6419185 5416818244AF2AFSB 21 5411851 1571
891427117 3511
   91488911 5458918231K 5891 14638582191891 2=
8 2855217 3511 411442 2824289191 411442 891
85823 518;7 323217 3511764858 28 2812824 2361=K"
 541T618391U4913358 28 281891 51828233 54VW2X 
8918231K"Y8915891 928914753Z 46419185 548284 2
58158942841191217 35117648 28 281 28246891
92458 28 28189153358244
   [\]^_`a\_bcade`dfgh]`_eij]\kdilaf^mdn_o]\piq
   rm_stbu18OF12728 58289168157485 157891
824AFu18vwxAxyPz@{FCP@KCDDDC|12185 51984129198{F
 1 14184891 5485891 28 285589117 3511}F 891 518
   rm_s~b012 3241 237287638 32855891728=824424
                    OH@OB O" DDD OE"                   K"

                              
                    0123456789 9   
                            
                            
                            
                            
                           
                           
                           
                           

  !""#$!%&!'#"()&'*$#&+,!-!.&/-'$'#"(
'-/"%/.#"&$ !0&$1"'-/"%/.#",%#""$!&$"#2/3##%%/0*
   456789:'#"('-/"%/.#"&$ $;-#"&$<3=!0&$ $ "#",+#>
#$0"&+!.&$"#$$?"!>'2&/@#'&,0 $#.!-/"$?!-2'#"(*
A$.!-.&+!%!$"-$!#"!B#2/.&$!"#$"!*
   4567C9D)"&2"#$$?"B$#/'#"(E +"&-"-$!#"!B#2/&+!1
+#!!&.#""&#.&+ $E #.&!"+.%!$"".#?"#""
.&!%&$0$?+&F$?"#' ;-!"!"&%)&' &$""&"#/%&G."*H)#&+
IJ KE !%!$"02>#2$#>,."&L&-"""&"#/%&G."*
   D!'%/(#'%///-!"#"!"+#> $+.&-'"&0+&F!*
defghijklm"VNOVP#$0Vn2""#!F!)&' $?#%&G."E*:.&$!"#$"!
+.0"' $&+"0o$"'%/&>!&)".&'%#$>.#$%)&'#.
"#!F#L
              VNW&)#.'%/&>L
                            wpN pP pn ps pv}
                    STUVUW xyz{zzyyz|xzyzz
   ~>"#$!/#"$?".&$!"#$"!0B$02>"/#0&)"%&G."#!0!G-$.
",)&'!1+&2"#$")&//&+$?0!G-$.",.&$!"#$"!L

                               
   01234156475489 3415647549 348564 549 364854 549
                       082364154 5479 341548549
                       0 2348547549 364154 5479
  1 8  
!
                                "%%&'%&(
                            12# %&%'%&
                                $&%%&'%)
                                #            )
                                             *
                                 &'%%&'%
                                  +         ,
                             82 '%&%%&
                                    %%&&%
                                  +&%&%%,
                              2 '%&%%&
    -./0/01/%21
/.13845
                                          " 67           (
               " 1         ( " 84( #    #
                                          # 8 9 99 9)
                                            %   %  &'%%   )
                                                          )
               ##% % &'%&)     #
                               #'%   % )
                                       )  #
                                          # 8   9  99   9 )
                                                          )
                ##% & %'%&) )3 #
                               # &   % )
                                       )2 #
                                          # %   %  %'%%   )
                                                          )
                            )  #
                               # %   & )
                                       )  #
                 $& % %&'%* $% & * #'% % %%'%)
                                          #               )
                  &'%%&'% & % #% 8 99 9)  #               )
                                          $'%'%%% %)      *
                                            % 8 99 9
    :;1/<=>002111;%&
?>2/121/5
    @2A0./;2?;?0B2
?2/0/1; 45
                                           " 6           (
            " 67             ( "  4( #   #
                                           # % % &8 9)
                                             %  8  9  9  9)
                                                          )
            ##% % &'%%)          #
                                 #&'%  )
                                       )   #
                                           # %  %  %8    9)
                                                          )
             ##% % %'%%)      )3 #
                                 #%  & )
                                       ) 2 #
                                           #'%  %  8'%%   )
                                                          )
              $'% % %%'%* #   )  #&  % )
                                       )   #
                                           #'%  %  %  %'% )
                                                          )
                 '%'%%% % % & #  $%  % *   #
                                           #'%  8  9  9  9)
                                                          )
                                           $'%'% % % %)   *
                                             % 8 99 9

                                 CD
   012345678139 35 4515153114354872 47 727567
8139 35 5
                          
                          
                          
   012813997 5756745434435725567 4 321!
556745!"71#567353517367 9771567$75%
                     &'&(&)&* &+ 
                       ,-./
                        ,0./
   1719275635567$7531#73 725# 7314567991!
21!573 
                   34(54)54*631234)54*54+6%
   01256721!573 56 1  45434(54)54*6%
   714 56747267 4545354#49"1!567#97 7351!
567573 4563531 775399567$7553424 47361! 5671756567
  1 3945%8643365567#97 4"74 93 5567145315
4354351#97 4 90:662456!364312155624$15"7
 492756717763"7$45472%
; <=>?@ABC=>B
D323 45 317463"75 21!573 4127 57E75"792
3$75%86753423$75 313!7 451492357567453E31257357
573 4563531367"71757 74954127 7531574745514%16
 745514371711!567 35633#95743#957431221972!7
3 1!5677 9774663"753 946567$75%86747 793514
 74551437571 97  567$75 313!7 31267 455327567
#7452741%
   F 439  1!56721!573 44#347217441!24$15"7
 4471!5677 97746923535731256476 4515
 7 1!47853424%867435483#95344!1 7154 74951! 567
#9731 93 7747155672E77153457 5675539$75%
   G7747153 7562 7441!56724$15"7 4912725736
5342%F 7562313942757 176621!573 434435725567
   1  455321!1514273515635567353517367 977
 17365342634347845%
HIJIKI>?IB
 LMNOPQRSOTMUVWXYZ[\]^_`\_ab]cXdeUfgOhijSOklSOmnjUoppqM

                                   rs
 01234567189 6 63  36  6 5532333 
   338!"#$"%"&'$&&"( )*'++,-81./01..08000.1
 /176 321318)4("54#64789$#:"82 ;3 <= 8>?@A1
 .176B C18=6B C186D318EF3GH1C18I 9#"!$"J $K4!54#:4&"(
   L4MN:K48:K9&"(O#4M&7!8P0000Q8R533315113BS.00A?>15
 T12  D6UR6B8>??/8J$7V   $"!W"!#$!8XB56 935R336 1.56
   3BRF 1
 Y1H36DZ18H3G6GH18[6DX11718966 3 R 365\3356135R 53
   R565 6 B1CR635B ]53D1D^3R5\3 _1= D38:"
   W"#$O#&&&64789$"(/08P000YQ81Y./1YT?
 A196553 2131CR6 3`6R566R3 \5353R 1
   563B3R3^3R5R3BD38J(7 $:"8a 1/08
   P>?@.Q81@T.1@YA1
 @13B=1U D358b#8KcK4#d'$!88&"$"4!$4O#4M&7!45:4"$d8XB51
   =4CH  3R5 8>?A@1
 ?1736e1C183633B=1e18f  3B658 3BRR36 B533338
   88&"J$K7$"&:"!8a 1.]PA0Q800>081/.TT1/.YY1
>01e 5691=18=D66 6H1=18Z 53 65 3B68*4$!4*97M#
   cK4#dW"!#$ J$K7$"!>T]P.Q8000?81>1Y
>>1U 58218f 536B 3 6`65336 8#$"%"&'$&&"( gh8
   0A/1/008>??Y1
>01a6B6 8=1918[3R3`5   5 =638U3686 B96 6768
   :'J L49#&464789$"(81/?@1.0A8a/>8Z08000>1
>/126\B9 38C6 H6Ri_ 58U6 B 7 3D38 565 64533R3CE 1
   R6 C6R8jk54#l"#!"$dO#!!8>.A1>T01




                                 mn