          The French Toast Problem, Solutions, Part 1

==== Solution 1, by Julian Michael, for clingo ====

%% domain predicates

bread(a;b;c).
pan(p).

#const n = 3.
time(0..n).

%% positional constraints

% a pan fits two breads
:- 3 { on(B, P, T) : bread(B) }, pan(P), time(T).
% a bread can only be on one pan
:- 2 { on(B, P, T) : pan(P) }, bread(B), time(T).
:- face_up(B, T), face_down(B, T).

%% physics of toasting

bot_toasted(B, T) :- face_up(B, T), on(B, P, T).
top_toasted(B, T) :- face_down(B, T), on(B, P, T).

%% auxiliary predicates

top_toasted(B, T+1) :- top_toasted(B, T), time(T+1).
bot_toasted(B, T+1) :- bot_toasted(B, T), time(T+1).
toasted(B, T) :- top_toasted(B, T), bot_toasted(B, T).

%% inertia

face_up(B, T+1) :- face_up(B, T), not not face_up(B, T+1), time(T+1).
face_down(B, T+1) :- face_down(B, T), not not face_down(B, T+1), time(T+1).
on(B, P, T+1) :- on(B, P, T), not not on(B, P, T+1), time(T+1).

%% effects of actions

on(B, P, T) :- place(B, P, T).
:- remove(B, P, T), on(B, P, T).
face_down(B, T) :- flip(B, T), face_up(B, T-1).
face_up(B, T) :- flip(B, T), face_down(B, T-1).

%% nonexecutability or necessary execution conditions

:- remove(B, P, T), place(B, P, T).
:- place(B, P, T+1), on(B, P, T).
:- remove(B, P, T+1), not on(B, P, T).

:- not remove(B, P, T), on(B, P, T-1), not on(B, P, T), time(T+1).

%% actions can be chosen

{ place(B, P, T) } :- bread(B), pan(P), time(T), T > 0.
{ remove(B, P, T) } :- bread(B), pan(P), time(T), T > 0.
{ flip(B, T) } :- bread(B), time(T), T > 0.

%% initial conditions

:- on(B, P, 0).
face_up(B, 0) :- bread(B).

%% goal conditions

:- not toasted(B, n), bread(B).

%% extra constraints so we show the best plan

% don't bother flipping when not on a pan.
:- flip(B, T), not on(B, P, T), pan(P).
% shouldn't need more than 3 flips
:- 4 { flip(B, T) : bread(B), time(T) }.

#show place/3.
#show remove/3.
#show flip/2.

==== Solution 2, by Jorge Fandino, for clingo ====

% I will use variable F for freach toast
% S for side and T for time.

pan_size(2).

toast(a).
toast(b).
toast(c).

side(1..2).

% time that takes to cook each toast side
time_to_cook(F,S,1) :- toast(F), side(S).

time(0..10).

% a toast is cooked after enough time on the pan
% once cooked can not be uncooked
cooked(F,S,T+CT) :- on_pan(F,S,T), time_to_cook(F,S,CT).
cooked(F,S,T+1)  :- cooked(F,S,T), time(T).

% a toast can not be on both sides at time
:- on_pan(F,S,T), on_pan(F,S2,T), S != S2.

% a toast must remain on the pan until is cooked
on_pan(F,S,T+1)  :- on_pan(F,S,T), not cooked(F,S,T+1), time(T).

uncooked(F,S,T)  :- toast(F), side(S), time(T),
					not cooked(F,S,T).

% you finish when there is no uncooked toast
some_uncooked(T) :- uncooked(F,S,T).
finish(T)	:- time(T), not some_uncooked(T).
finish 		:- finish(T).
:- not finish.

% actions
{ on_pan(F,S,T) : toast(F), side(S) }N :- pan_size(N), time(T).

#minimize{ 1@T : some_uncooked(T) }.
#minimize{ 1@on_pan(F,S,T)    : toast(F), side(S), time(T) }.

total_time(T) :- T = #min{ TT : finish(TT) }.

#show on_pan/3.
#show total_time/1.

==== Solution 3, by Adam Smith, for clingo ====

(See http://nbviewer.ipython.org/urls/dl.dropbox.com/s/nv3wbxy5j4lo228/The%20French%20Toast%20Problem.ipynb
for discussion and an alternatice formulation)

#const p = 3.
#const c = 2.
#const t = 4.

state(cooked;uncooked).
face(front;back).
loc(counter;pan).

piece(1..p).
time(1..t).

% Initially, every face of every piece is uncooked.
status((P,F),uncooked,1) :- piece(P); face(F).

% At every time, each piece has a unique location and orientation.
1 { location(P,L,T):loc(L) } 1 :- piece(P); time(T).
1 { orientation(P,F,T):face(F) } 1 :- piece(P); time(T).
    
% But there aren't too many pieces in the pan!
:- time(T); c + 1 { location(P,pan,T):piece(P) }.
    
% Simple cooking dynamics:
heated((P,F),T) :- location(P,pan,T); orientation(P,F,T).
status(Pair,cooked,T+1) :- heated(Pair,T).
status(Pair,S,T+1) :- time(T); status(Pair,S,T), not heated(Pair,T).

% Job completion
more_work(T) :- status(Pair,uncooked,T+1).
finished :- time(T); not more_work(T).
:- not finished.
#minimize { 1,T: more_work(T) }.

% Display
cook(Pair,T) :- status(Pair,uncooked,T); heated(Pair,T).
#show cook/2.

==== Solution 4, by Bart Bogaerts, for IDP ====

(See http://dtai.cs.kuleuven.be/krr/idp-ide/?src=54d24a20645472118790
for an alternative formulation)

vocabulary toastVoc{
    /*
     *  TYPES
     */
    
    //French toasts to be baked
    type toast
    
    //sides of toasts
    type side 
    
    //time
    type time
    
    //Whether or not some side of some toast is baking at a certain time
    isBaking(toast,side,time)
    
}

//NOTE: I sometimes omitted type information in my theory. f always refers to a french toast,  s to a side and t to a time

theory combinatorial: toastVoc{
	//Pan only has size 2, thus maximally two toastsides can bake at the same time
    !t[time]: #{f[toast] s[side] : isBaking(f,s,t)} =< 2.
    
    //A toast cannot    
    !t[time] f[toast]: #{s[side] : isBaking(f,s,t)} =< 1.

    //Every side of every toast should be baked:
    ! f[toast] s[side] : ?t[time]: isBaking(f,s,t).
    
}

//We minimize the number of time points that some toast is baking
//NOTE: lots of liberty here, we could also minimize, e.g., the largest time at which some toast is baking
term optimalitycriterion: toastVoc{
    #{t: ?f s: isBaking(f,s,t)}
}

//Vladimir's instance
structure vl: toastVoc{
    toast = { toast_1; toast_2; toast_3} //three toasts
    side = {side_1; side_2} //2 sides
    time = {0..6} //some time points
}

procedure main(){
    
    //We want one model
    stdoptions.nbmodels = 1
    
    //We do optimization
    sol, optimal, value = minimize(combinatorial, vl, optimalitycriterion)
    
    print(">>>>We found a model.")
    if optimal then
    	print(">>>>this model is optimal")
    else
    	print(">>>>we did not prove optimality")
    end
    print(">>>>The value of the optimisation term in this model is "..value)
    print(">>>>The model is:\n")
    print(sol[1])
}

==== Solution 5, by Martin Gebser, for clingo ====

#const pieces=3.
#const capacity=2.

% guess and check

piece(1..pieces).
time(1..((pieces+capacity-1)/capacity)*2).

2 { cook(P,T) : time(T) } 2 :- piece(P).
:- time(T), capacity+1 #count{ P : cook(P,T) }.

% optimize

cook(T) :- cook(P,T).
:- cook(T), 1 < T, not cook(T-1). % use consecutive times starting from 1
:~ cook(T). [1,T]

% symmetry breaking

fill(P,T-1,-1) :- cook(P,T), 2 < T.
fill(P,T+1, 1) :- cook(P,T), time(T+2).
fill(P,T+D, D) :- fill(P,T,D), time(T+2*D).
:- fill(P+1,T, 1), piece(P), not fill(P,T, 1). % pieces start cooking in order
:- fill(P-1,T,-1), piece(P), not fill(P,T,-1). % pieces finish cooking in order

% display

#show cook/2.

==== Solution 6, by Peter Schueller, for clingo ====

% input: how many toasts do we want to toast?
% in this case 3 slices {a, b, c}
toast(a). toast(b). toast(c).
% end of input

% every slice has two sides
toastside(side1(T)) :- toast(T).
toastside(side2(T)) :- toast(T).

% time starts at 0
time(0).
% create the maximum time we need: naively toast each toast side separately
time(T+1) :- time(T), T <= #count { TS : toastside(TS) }.

% at each step roast or not roast a toast side
{ roast(TS,Step) } :- toastside(TS), time(Step).

% if we roast, it is roasted in the next step
roasted(TS,Step+1) :- roast(TS,Step), time(Step+1).
% roasted remains roasted
roasted(TS,Step+1) :- roasted(TS,Step), time(Step+1).

% do not re-roast
:- roast(TS,Step), roasted(TS,Step).

% do not roast more than 2 toast sides at once
:- 2 < #count { TS : roast(TS,Step) }, time(Step).

% do not roast both sides of the same toast at once
:- roast(side1(T),Step), roast(side2(T),Step), time(Step).

% if one toastside is not roasted we are notfinished in this step
notfinished(Step) :- toastside(TS), not roasted(TS,Step), time(Step).

% we are finished if we are not notfinished
finished(Step) :- not notfinished(Step), time(Step).

% forbid to be notfinished at a cost
% the cost is the required number of steps
:~ time(Step), not finished(Step). [ 1,Step ]

% this makes us obtain cost 0 = "we need 0 steps" if there is no toast
% (otherwise optimization does not kick in because
% the previous weak constraint yields no ground instances)
:~. [0,0]

% output: roast(<which slice>,<rost at which step>)
#show roast/2.

==== Solution 7, by Amelia Harrison, for clingo ====

bread(a;b;c). 
bread_side(B, 0..1) :- bread(B). 

#const n=2. 
time(0..n).

{place(B, S, T)} :- not side_done(B, S, T), time(T), bread_side(B, S).
{flip(B, T)} :- on_pan(B, S, T-1), not side_done(B, S^1, T-1), bread_side(B, S),
time(T).
{remove(B, T)} :- on_pan(B, S, T-1), bread(B). 

% effects of actions
on_pan(B, S, T) :- place(B, S, T). 
side_done(B, S, T) :- on_pan(B, S, T-1). 
ready(B, T) :- remove(B, T), side_done(B, S1, T1), side_done(B, S2, T2), S1 != S2, T >= T1, T >= T2.
on_pan(B, S^1, T) :- on_pan(B, S, T-1), flip(B, T), T <= n. 
 
% cannot perform 2 actions at once 
:- place(B, S, T), flip(B, T), bread_side(B,S). 
:- place(B, S, T), remove(B, T), bread_side(B,S). 
:- flip(B, T), remove(B, T).

% physical constraints
:- #count{S : on_pan(B,S,T)} > 1, time(T), bread(B).  
:- #count{B,T : on_pan(B,S,T)} > 2, time(T).  
 
% inertia
on_pan(B, S, T) :- on_pan(B, S, T-1), T <= n, not flip(B, T), not remove(B,T).
side_done(B, S, T) :- side_done(B, S, T-1), T <=n.  

% symmetry breaking constraint --- we don't really want to distinguish sides 
% always place side 0 first
:- place(B, 0, T1), place(B, 1, T2), T2 < T1.
% only place 1 if you already placed 0 
:- place(B, 1, T1), not place(B, 0, _).  

% what's a solution
:- not ready(B, _), bread(B). 

#show place/3. 
#show flip/2.
#show remove/2. 
#show ready/2.

==== Solution 8, by Shahab Tasharrofi, for clingo ====

#const n = 3.
timestep(0..n).
toast(1..3).
side(1..2).

0{fryAt(T,S,Time)}1 :- toast(T), side(S), timestep(Time).
:- fryAt(T, 1, Time), fryAt(T, 2, Time).
:- 3{fryAt(T, S, Time)}, timestep(Time).

friedAt(T, S, Time + 1) :- fryAt(T, S, Time).
friedAt(T, S, Time + 1) :- friedAt(T, S, Time), timestep(Time + 1).
:- not friedAt(T, S, n), toast(T), side(S).
:- fryAt(T, S, Time), friedAt(T, S, Time).

#show fryAt/3.

==== Solution 9, by Joshua Irvin and Yuliya Lierler, for clingo ====

#const maxt=3.
time(0..maxt).

toast(t1;t2;t3).
side(s1;s2).

%action of cooking a toast side on a pan *may* happen in case when a toast
was not previously cooked
{actionCookToastSide(To,S,T)}:- time(T),toast(To),side(S), not
cooked(To,S,T) .

% effect of actionCookToastSide is cooked Toast Side at the next
minute
cooked(To,S,T+1):-actionCookToastSide(To,S,T), time(T).

% if actionCookToastSide(To,S,T) occurs then toast To is being cooked at
time T
toastBeingCooked(To,T):-actionCookToastSide(To,S,T),time(T),toast(To),side(S).

%We cannot fry more than two toasts at a time
:-toastBeingCooked(To1,T),toastBeingCooked(To2,T),toastBeingCooked(To3,T),
To1!=To2,To2!=To3,To1!=To3.

%we cannot fry two sides of the same toast at the same time
:-actionCookToastSide(To,S1,T), actionCookToastSide(To,S2,T), S1!=S2,
      time(T),toast(To),side(S1;S2).

%Once cooked toast-side stays cooked
cooked(To,S,T+1):-cooked(To,S,T), time(T).

% Six constraints below require that by maxt every toast-side  is cooked
:- not  cooked(t1,s1,maxt).
:- not  cooked(t1,s2,maxt).
:- not  cooked(t2,s1,maxt).
:- not  cooked(t2,s2,maxt).
:- not  cooked(t3,s1,maxt).
:- not  cooked(t3,s2,maxt).

#hide.
#show actionCookToastSide(To,S,T).

==== Solution 10, by Ben Susman, for clingcon  ====

#hide bread/1.
#hide side/1.
#hide toast/2.

#const numBread=3.

$domain(1..numBread):- numBread > 1.
$domain(1..2):- numBread == 1.

bread(1..numBread).
side(1..2).

% Toasting consists of a piece of bread with two sides
toast(B,S):-bread(B),side(S).

% Without loss of generality, we toast the first side before the second and cannot be done simultaneously
toast(B,S1) $< toast(B,S2):-toast(B,S1),toast(B,S2),S1 < S2.

% Without lost of generality, we toast the first piece before the next
toast(B1,S) $<= toast(B2,S):-toast(B1,S),toast(B2,S),B1 < B2.

% If there are two pieces of bread being toasted, then all other pieces must be toasted at a different time.
toast(B3,S3) $!= toast(B1,S1) :- toast(B1,S1) $== toast(B2,S2), toast(B1,S1), toast(B2,S2), toast(B3,S3), B3 != B1, B3 != B2, B1 != B2.

totalMinutes $== toast(numBread,2).

==== Solution 11, by Maurice Bruynooghe, for IDP  ====

vocabulary V {
    type time isa nat
    type toast 
    type side  isa nat
    type toastside constructed from {ts(toast,side)}
    bake(toastside):time // 
}

theory Baking : V{ 
!t[time]: #{ts:bake(ts)=t} =< 2.  //pan capacity
!t[time] to[toast]: #{s : bake(ts(to,s))=t} =<1. //at most one side at a time
}

structure Input : V { 
    toast = {a;b;c}
    side = {1;2}
    time = {1 .. 6}
}

term M : V{ 
max {t:  true: bake(t)}
}

procedure main(){
    stdoptions.cpsupport=true
    printmodels(minimize(Baking, Input, M))
    
}

==== Solution 12, by Joshua Irvin, for clingo ====

#const t = 2.
time(0..t).
toast(1). toast(2). toast(3).
side(1). side(2).

%both sides of each toast must be cooked
aCook(To, S) :- toast(To), side(S).

%at most 2 toasts can be cooked at a time
{occurs(aCook(To, S), T) : aCook(To, S)}2 :- time(T).

%constraint that prevents a toast side from being cooked more than once
:- occurs(aCook(To,S),T1),occurs(aCook(To,S),T2),T1!=T2.

%when an action occurs the toast's side is then cooked
cooked(To, S, T+1) :- occurs(aCook(To, S), T).

%goal is reached when both sides of a toast are cooked
%the T != T1 condition prevents both sides of a toast
%from being cooked simultaneously
goal(To) :- cooked(To, 1, T), cooked(To, 2, T1), T != T1.

%success is achieved when all goals are met
%in other words when all toasts are cooked on both sides
success :- goal(To) : toast(To).

%ensures success must be reached
:- not success.

==== Solution 13, by Michael Gelfond, for Sparc  ====

% This is just a planning version of the program.
% No optimization. Shortest plan is achieved by selecting the right n.

#const n = 3.  % number of steps
#const m = 6.  % number of sides

sorts 

#step = 0..n.
 
#side = 1..m.

% Sides of the first toast are 1,2, second 3,4, etc.

#action = toast(#side).

#fluent = toasted(#side).

predicates

holds(#fluent,#step).

occurs(#action,#step).

o(#action,#step).

same_toast(#side,#side).

all_toasted(#step). 

success().

rules

% toast causes toasted

holds(toasted(S),I1) :-
                 occurs(toast(S),I),
                 I1 = I+1.

% impossible to toast more then two sides at the same time:

:- #step(I),
   #count{A:occurs(A,I)} > 2.

% impossible to toast two sides of the same toast at the same time

same_toast(1,2).
same_toast(X+2,Y+2) :- same_toast(X,Y).
same_toast(X,Y) :- same_toast(Y,X).

-occurs(toast(S2),I) :-
        occurs(toast(S1),I),
        same_toast(S1,S2). 

% inertia

holds(F,I+1) :- 
         holds(F,I),
         not -holds(F,I+1).

-holds(F,I+1) :- 
         -holds(F,I),
         not holds(F,I+1).


%goal

all_toasted(I) :-
        #count{S : holds(toasted(S),I)} = m.

success :- all_toasted(I).

:- not success. 

% initially

-holds(toasted(S),0). 

% generate

occurs(A,I) | -occurs(A,I) :-
                     not all_toasted(I).

o(A,I) :- occurs(A,I). % Use for display


%sparc  toast-plan.lp -A -solveropts "-pfilter=o,all_toasted"

==== Solution 14, by Mario Alviano, for dlv  ====

#const toasts = 3.
#const pan_size = 2.

toast(1..toasts).
side(1..2).
time(T) :- T = toasts * 2.
time(T1) :- time(T), T1 = T-1, T1 > 0.

% guess when each toast side is cooked
in(X,S,T) | out(X,S,T) :- toast(X), side(S), time(T).

% at most pan_size toasts at the same time
:- time(T), #count{X,S : in(X,S,T)} > pan_size.

% at most one side of each toast at each time step
:- time(T), toast(X), #count{S : in(X,S,T)} > 1.

% all coocked
:- toast(X), side(S), not #count{T : in(X,S,T)} = 1.

% compute cost
used(T) :- in(_,_,T).
:~ used(T). [T:1]

% as an alternative to the previous weak constraint (in case the cost
% must coincide with the time required to cook all toasts):
% :- used(T), T > 1, T1 = T-1, not used(T1).
% :~ used(T). [1:1]

