CAS Program

%% Encoding TS Problem road(Y,X):-road(X,Y). cost(Y,X,C):-cost(X,Y,C). 1{route(X,Y): road(X,Y)}1:-city(X). 1{route(X,Y): road(X,Y)}1:-city(Y). reached(X):-initial(X). reached(Y):-reached(X), route(X,Y). :-city(X), not reached(X). &dom {0..C} = c(X,Y) :- cost(X,Y,C). &sum {c(X,Y)} =0 :-cost(X,Y,C), not route(X,Y). &sum {c(X,Y)} =C :-cost(X,Y,C), route(X,Y). :- &sum {c(X,Y):cost(X,Y,C)} > W, maxCost(W). %% Instance TS Problem city(a). city(b). city(c). city(d). initial(a). road(a,b). road(b,c). road(c,d). cost(a,b,1). cost(b,c,1). cost(c,d,1). road(d,a). road(a,c). road(b,d). cost(d,a,1). cost(a,c,2). cost(b,d,2). maxCost(4).

EZSMT Output