victornicolet

#!/usr/env/bin/python3
from z3 import *
from itertools import combinations


def solve_job_shop(alljobs, optimize=False):
    v = [[(Int("t_%i_%i" % (i, j)), task) 
    		for j, task in enumerate(job)] 
    			for i, job in enumerate(alljobs)]
    clauses = []

victornicolet

#!/usr/bin/env python3

# command,mean,stddev,median,user,system,min,max,nalarm
#    0      1   2       3      4    5     6   7      8
def parseline(line):
    parts = line.strip().split(',')
    name = parts[0].split('>')[0].strip().split(' ')[1]
    time = parts[1]
    nalarm = parts[8]
    nameparts = name.split('-')

victornicolet

for i in range(9):
  for k in range(9):
    clauses += exactly_one([lits[i][j][k] for j in range(9)])

victornicolet

for j in range(9):
  for k in range(9):
    clauses += exactly_one([lits[i][j][k] for i in range(9)])

victornicolet

    for i in range(9):
        for j in range(9):
            clauses += exactly_one(lits[i][j])

victornicolet

;;define the max function
(define-fun max ((x Int) (y Int)) Int (ite (< x y) y x))
;; optimization problem
(minimize (max (+ t02 2) (max (+ t12 4) (+ t21 3))))

victornicolet

import itertools
import os
import sys

def nl(f):
    f.write('\n')


do_maxSAT = True
# Output file

victornicolet

;; Machine 0- only 2 tasks, it's easy
(assert (or
  (and  (<= (+ t00 3) t10))
 (and  (<= (+ t10 2) t00))))

;; Machine 1: three tasks, so 6 possible sequences!
(assert (or
  (and  (<= (+ t01 2) t12) (<= (+ t12 4) t20))
  (and  (<= (+ t01 2) t20) (<= (+ t20 4) t12))
 (and  (<= (+ t12 4) t01) (<= (+ t01 2) t20))

victornicolet

(assert (and (<= (+ t00 3)  t01) (<= (+ t01 2)  t02)))
(assert (and (<= (+ t10 2)  t11) (<= (+ t11 1)  t12)))
(assert (and (<= (+ t20 4)  t21))

victornicolet

(assert (and (>= t00 0) (>= t01 0) (>= t02 0) (>= t10 0) (>= t11 0) (>= t12 0) (>= t20 0) (>= t21 0)))