Last change
on this file since 56 was
12,
checked in by cecile, 13 years ago
|
cusp added
|
-
Property svn:executable set to
*
|
File size:
2.2 KB
|
Rev | Line | |
---|
[12] | 1 | (benchmark job_shop_scheduling_4_2.smt |
---|
| 2 | :source { |
---|
| 3 | Job_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.