(benchmark job_shop_scheduling_4_2.smt
:source {
Job_Shop_Scheduling Problem from Papadimitriou-Steiglitz is translated by Hyondeuk Kim in SMT-LIB format benchmark
}
:status sat
:category { crafted }
:difficulty { 0 }
:logic QF_IDL
:extrafuns ((s1_1 Int))
:extrafuns ((s1_2 Int))
:extrafuns ((s2_1 Int))
:extrafuns ((s2_2 Int))
:extrafuns ((s3_1 Int))
:extrafuns ((s3_2 Int))
:extrafuns ((s4_1 Int))
:extrafuns ((s4_2 Int))
:extrafuns ((m1_1 Int))
:extrafuns ((m2_1 Int))
:extrafuns ((m3_1 Int))
:extrafuns ((m4_1 Int))
:extrafuns ((m1_2 Int))
:extrafuns ((m2_2 Int))
:extrafuns ((m3_2 Int))
:extrafuns ((m4_2 Int))
:extrafuns ((ref Int))
:formula
( and
(<= (- m1_1 ref ) 1 )
(<= (- m2_1 ref ) 1 )
(<= (- m3_1 ref ) 1 )
(<= (- m4_1 ref ) 1 )
(<= (- m1_2 ref ) 1 )
(<= (- m2_2 ref ) 1 )
(<= (- m3_2 ref ) 1 )
(<= (- m4_2 ref ) 1 )
(>= (- m1_1 ref) 0 )
(>= (- m2_1 ref) 0 )
(>= (- m3_1 ref) 0 )
(>= (- m4_1 ref) 0 )
(>= (- m1_2 ref) 0 )
(>= (- m2_2 ref) 0 )
(>= (- m3_2 ref) 0 )
(>= (- m4_2 ref) 0 )
( or (not ( = (- m1_1 m2_1 ) 0 )) (>= (- s1_1 s2_1 ) 4 ) (>= (- s2_1 s1_1 ) 4 ))
( or (not ( = (- m1_1 m3_1 ) 0 )) (>= (- s1_1 s3_1 ) 4 ) (>= (- s3_1 s1_1 ) 4 ))
( or (not ( = (- m1_1 m4_1 ) 0 )) (>= (- s1_1 s4_1 ) 4 ) (>= (- s4_1 s1_1 ) 4 ))
( or (not ( = (- m2_1 m3_1 ) 0 )) (>= (- s2_1 s3_1 ) 4 ) (>= (- s3_1 s2_1 ) 4 ))
( or (not ( = (- m2_1 m4_1 ) 0 )) (>= (- s2_1 s4_1 ) 4 ) (>= (- s4_1 s2_1 ) 4 ))
( or (not ( = (- m3_1 m4_1 ) 0 )) (>= (- s3_1 s4_1 ) 4 ) (>= (- s4_1 s3_1 ) 4 ))
( or (not ( = (- m1_2 m2_2 ) 0 )) (>= (- s1_2 s2_2 ) 4 ) (>= (- s2_2 s1_2 ) 4 ))
( or (not ( = (- m1_2 m3_2 ) 0 )) (>= (- s1_2 s3_2 ) 4 ) (>= (- s3_2 s1_2 ) 4 ))
( or (not ( = (- m1_2 m4_2 ) 0 )) (>= (- s1_2 s4_2 ) 4 ) (>= (- s4_2 s1_2 ) 4 ))
( or (not ( = (- m2_2 m3_2 ) 0 )) (>= (- s2_2 s3_2 ) 4 ) (>= (- s3_2 s2_2 ) 4 ))
( or (not ( = (- m2_2 m4_2 ) 0 )) (>= (- s2_2 s4_2 ) 4 ) (>= (- s4_2 s2_2 ) 4 ))
( or (not ( = (- m3_2 m4_2 ) 0 )) (>= (- s3_2 s4_2 ) 4 ) (>= (- s4_2 s3_2 ) 4 ))
(>= (- s1_2 s1_1 ) 4 )
(>= (- s2_2 s2_1 ) 4 )
(>= (- s3_2 s3_1 ) 4 )
(>= (- s4_2 s4_1 ) 4 )
(<= (- s1_2 ref ) 8 )
(<= (- s2_2 ref ) 8 )
(<= (- s3_2 ref ) 8 )
(<= (- s4_2 ref ) 8 )
(>= (- s1_1 ref) 0 )
(>= (- s2_1 ref) 0 )
(>= (- s3_1 ref) 0 )
(>= (- s4_1 ref) 0 )
))