source: vis_dev/cusp-1.1/examples/jobshop4-2-2-2-4-4-12/jobshop4-2-2-2-4-4-12.smt @ 20

Last change on this file since 20 was 12, checked in by cecile, 13 years ago

cusp added
  • Property svn:executable set to *
File size: 2.2 KB
Line 
1(benchmark job_shop_scheduling_4_2.smt
2:source {
3Job_Shop_Scheduling Problem from Papadimitriou-Steiglitz is translated by Hyondeuk Kim in SMT-LIB format benchmark
4}
5:status sat
6:category { crafted }
7:difficulty { 0 }
8:logic QF_IDL
9:extrafuns ((s1_1 Int))
10:extrafuns ((s1_2 Int))
11:extrafuns ((s2_1 Int))
12:extrafuns ((s2_2 Int))
13:extrafuns ((s3_1 Int))
14:extrafuns ((s3_2 Int))
15:extrafuns ((s4_1 Int))
16:extrafuns ((s4_2 Int))
17:extrafuns ((m1_1 Int))
18:extrafuns ((m2_1 Int))
19:extrafuns ((m3_1 Int))
20:extrafuns ((m4_1 Int))
21:extrafuns ((m1_2 Int))
22:extrafuns ((m2_2 Int))
23:extrafuns ((m3_2 Int))
24:extrafuns ((m4_2 Int))
25:extrafuns ((ref Int))
26:formula
27( and
28(<= (- m1_1 ref ) 1 )
29(<= (- m2_1 ref ) 1 )
30(<= (- m3_1 ref ) 1 )
31(<= (- m4_1 ref ) 1 )
32(<= (- m1_2 ref ) 1 )
33(<= (- m2_2 ref ) 1 )
34(<= (- m3_2 ref ) 1 )
35(<= (- m4_2 ref ) 1 )
36(>= (- m1_1 ref) 0 )
37(>= (- m2_1 ref) 0 )
38(>= (- m3_1 ref) 0 )
39(>= (- m4_1 ref) 0 )
40(>= (- m1_2 ref) 0 )
41(>= (- m2_2 ref) 0 )
42(>= (- m3_2 ref) 0 )
43(>= (- m4_2 ref) 0 )
44( or (not ( = (- m1_1 m2_1 ) 0 )) (>= (- s1_1 s2_1 ) 4 ) (>= (- s2_1 s1_1 ) 4 ))
45( or (not ( = (- m1_1 m3_1 ) 0 )) (>= (- s1_1 s3_1 ) 4 ) (>= (- s3_1 s1_1 ) 4 ))
46( or (not ( = (- m1_1 m4_1 ) 0 )) (>= (- s1_1 s4_1 ) 4 ) (>= (- s4_1 s1_1 ) 4 ))
47( or (not ( = (- m2_1 m3_1 ) 0 )) (>= (- s2_1 s3_1 ) 4 ) (>= (- s3_1 s2_1 ) 4 ))
48( or (not ( = (- m2_1 m4_1 ) 0 )) (>= (- s2_1 s4_1 ) 4 ) (>= (- s4_1 s2_1 ) 4 ))
49( or (not ( = (- m3_1 m4_1 ) 0 )) (>= (- s3_1 s4_1 ) 4 ) (>= (- s4_1 s3_1 ) 4 ))
50( or (not ( = (- m1_2 m2_2 ) 0 )) (>= (- s1_2 s2_2 ) 4 ) (>= (- s2_2 s1_2 ) 4 ))
51( or (not ( = (- m1_2 m3_2 ) 0 )) (>= (- s1_2 s3_2 ) 4 ) (>= (- s3_2 s1_2 ) 4 ))
52( or (not ( = (- m1_2 m4_2 ) 0 )) (>= (- s1_2 s4_2 ) 4 ) (>= (- s4_2 s1_2 ) 4 ))
53( or (not ( = (- m2_2 m3_2 ) 0 )) (>= (- s2_2 s3_2 ) 4 ) (>= (- s3_2 s2_2 ) 4 ))
54( or (not ( = (- m2_2 m4_2 ) 0 )) (>= (- s2_2 s4_2 ) 4 ) (>= (- s4_2 s2_2 ) 4 ))
55( or (not ( = (- m3_2 m4_2 ) 0 )) (>= (- s3_2 s4_2 ) 4 ) (>= (- s4_2 s3_2 ) 4 ))
56(>= (- s1_2 s1_1 ) 4 )
57(>= (- s2_2 s2_1 ) 4 )
58(>= (- s3_2 s3_1 ) 4 )
59(>= (- s4_2 s4_1 ) 4 )
60(<= (- s1_2 ref ) 8 )
61(<= (- s2_2 ref ) 8 )
62(<= (- s3_2 ref ) 8 )
63(<= (- s4_2 ref ) 8 )
64(>= (- s1_1 ref) 0 )
65(>= (- s2_1 ref) 0 )
66(>= (- s3_1 ref) 0 )
67(>= (- s4_1 ref) 0 )
68))
Note: See TracBrowser for help on using the repository browser.