/***************************************************************************** A constraint solver implemented in B-Prolog for CPAI'08 Solver Competition by Neng-Fa Zhou, 2006, 2007, 2008, 2009 Version 7.2 and up To solve a problem instance in Prolog format, say "zebra.pl", use 1. load and run ?- cl(solve). ?- solve(zebra). 2. or run as a command-line bp solve.out -g "solve(zebra),halt" *****************************************************************************/ solve(BaseName):- % solve(BaseName,1800000). solve(BaseName,600000). solve(BaseName,TimeLimit):- statistics(backtracks,Backs0), atom_codes(BaseName,String), append(String,".pl",String2), atom_codes(InFile,String2), (exists(InFile)->true;format("c File not found:~w~n",[InFile]),halt), see(InFile), cputime(Start), read((csp(Vars):-Body)), seen, % append(String,".sol",String3), % atom_codes(SolFile,String3), % SolFile=solution, SolFile=user, tell(SolFile), writeln(user,'c solving'(BaseName,TimeLimit)), writeln('c solving'(BaseName,TimeLimit)), solve_prob(Body,Vars,TimeLimit), cputime(End), statistics(backtracks,Backs1), NBacks is Backs1-Backs0, Time is End-Start, format("~nc Time=~w ms Backtracks=~w~n~n",[Time,NBacks]),!, told. convert_solve(BaseName,TimeLimit):- xcsp2pl(BaseName), solve(BaseName,TimeLimit). t(BaseName):- atom_codes(BaseName,String), append(String,".pl",String2), atom_codes(InFile,String2), (exists(InFile)->true;format("File not found:~w~n",[InFile]),halt), see(InFile), read((csp(Vars):-Body)), seen, cputime(Start), statistics(backtracks,B0), execute_body(Body), (labeling(Vars)->Res=suc(Vars);Res=fail), statistics(backtracks,B1), cputime(End), Time is End-Start, writeln(Res), B is B1-B0, format("~nc Time: ~w ~nBacktracks:~w~n~n",[Time,B]),!. tall(BaseName):- atom_codes(BaseName,String), append(String,".pl",String2), atom_codes(InFile,String2), (exists(InFile)->true;format("File not found:~w~n",[InFile]),halt), see(InFile), read((csp(Vars):-Body)), seen, execute_body(Body), labeling(Vars), writeln(Vars),fail. /****************************************************************/ ec(support1(Tuple),CompVars,_Neqs) => CompVars=Tuple. ec(support(Arity,Mins,Maxs,BigTrie,Tries),CompVars,_Neqs) => constr_scope_tuple(Arity,CompVars), $cfd_var_in(Arity,CompVars,Mins,Maxs,BigTrie,Tries). ec(conflict(_Arity,[],_),_CompVars,_Neqs) => true. ec(conflict(Arity,Tuples),CompVars,Neqs):- Arity=2 ? $eq_rel(Tuples,Min,Max), CompVars=t(V1,V2), domain_min_max(V1,Min1,Max1), domain_min_max(V2,Min2,Max2), Min1>=Min,Min2>=Min,Max1= constr_scope_tuple(Arity,CompVars), $cfd_var_notin(Arity,CompVars,Tuples). $eq_rel([t(E,E)|Tuples],Min,Max) => Min=E, Next is E+1, $eq_rel_aux(Tuples,Next,Max). $eq_rel_aux([t(E,E)],E,Max) => Max=E. $eq_rel_aux([t(E,E)|Tuples],E,Max) => Next is E+1, $eq_rel_aux(Tuples,Next,Max). /****************************************************************/ solve_prob(Body,Vars,TimeLimit):- execute_body(Body),!, (global_get('_$disjunctive_tasks',1)-> Strategies=[ff,ff_min,ff_backward]; Strategies=[ffc,ff,forward,ff_backward]), global_set('_$disjunctive_tasks',0), solve_vars(Vars,TimeLimit,Strategies). solve_prob(_Body,_Vars,_TimeLimit):- writeln('c before_labeling'), writeln('s UNSATISFIABLE'),nl. execute_body(Body):- post_constr(Body,Disjunctions,[],Neqs), closetail(Neqs), % writeln(user,Neqs), post_neqs(Neqs), post_disjunctive_tasks(Disjunctions). post_constr(G,Disjunctions,DisjunctionsR,Neqs), G=((X*Y#<0#\/abs(X-Y)#>=N1), constr_scope([X,Y]), (X*Y#>0 #\/ abs(abs(X)-abs(Y))#>=N2), G1), dvar_excludable(X),dvar_excludable(Y), integer(N1),integer(N2),N1>=N2, b_DM_FALSE_cc(X,0),b_DM_FALSE_cc(Y,0) => constr_scope([X,Y]), (N1==N2-> (N1==0->true;abs(abs(X)-abs(Y)) #>= N1) ; (N2==0->true; abs(X-Y)#>=N2, $comp_prop_fapp2(X,Y,N2,_)), % X*Y#>0 #\/ abs(AbsY(X)-AbsY)#>=N2, $comp_prop_fapp1(X,Y,N1,_)), % X*Y#<0 #\/ abs(X-Y)#>=N1, post_constr(G1,Disjunctions,DisjunctionsR,Neqs). post_constr(((Exp1 #\/ Exp2),G2),Disjunctions,DisjunctionsR,Neqs), Exp1=(abs(P1//N-P2//N)#=1#/\abs(P1 mod N-P2 mod N)#=2), Exp2=(abs(P1//N-P2//N)#=2#/\abs(P1 mod N-P2 mod N)#=1), integer(N),N>0, dvar(P1),dvar(P2),dvar_excludable(P1), dvar_excludable(P2), domain_min_max(P1,Min1,_), domain_min_max(P2,Min2,_), Min1>=0,Min2>=0 => $knightMove(P1,P2,N), post_constr(G2,Disjunctions,DisjunctionsR,Neqs). post_constr(((Exp1 #\/ (Exp2 #\/ Exp3)),G2),Disjunctions,DisjunctionsR,Neqs), Exp1=(P1 mod N#=P2 mod N), Exp2=(P1//N#=P2//N), Exp3=(abs(P1//N-P2//N)#=abs(P1 mod N-P2 mod N)), integer(N),N>0, dvar(P1),dvar(P2),dvar_excludable(P1), dvar_excludable(P2), domain_min_max(P1,Min1,_), domain_min_max(P2,Min2,_), Min1>=0,Min2>=0 => $queenMove(P1,P2,N), post_constr(G2,Disjunctions,DisjunctionsR,Neqs). post_constr((G1,G2),Disjunctions,DisjunctionsR,Neqs) => post_constr(G1,Disjunctions,Disjunctions1,Neqs), post_constr(G2,Disjunctions1,DisjunctionsR,Neqs). post_constr(G,Disjunctions,DisjunctionsR,_Neqs), G=((S1+D1 #=< S2) #\/ (S2 + D2 #=< S1)), dvar_excludable(S1),dvar_excludable(S2),integer(D1),integer(D2),D1>0,D2>0,S1\==S2 => Disjunctions=[disj_tasks(S1,D1,S2,D2)|DisjunctionsR]. post_constr(G,Disjunctions,DisjunctionsR,_Neqs), G=((S2 #>= S1+D1) #\/ (S1 #>= S2 + D2)), dvar_excludable(S1),dvar_excludable(S2),integer(D1),integer(D2),D1>0,D2>0,S1\==S2 => Disjunctions=[disj_tasks(S1,D1,S2,D2)|DisjunctionsR]. post_constr(G,Disjunctions,DisjunctionsR,Neqs), G=(V1#\=V2), dvar_excludable(V1), dvar_excludable(V2), dvar(V1),dvar(V2) => Disjunctions=DisjunctionsR, attach(G,Neqs). post_constr(G,Disjunctions,DisjunctionsR,Neqs), G=ec(Rel,CompVars) => Disjunctions=DisjunctionsR, ec(Rel,CompVars,Neqs). post_constr(G,Disjunctions,DisjunctionsR,_Neqs) => Disjunctions=DisjunctionsR, call(G). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% /* (X*Y#<0) #\/ (abs(X-Y)#>=N), X to Y */ :-determinate $opposite_sign_or_zero/2,$constructive_or_prop1/3. $comp_prop_fapp1(X,Y,_N,Flag),var(Flag),{generated,ins(X),bound(X),ins(Y),bound(Y),ins(Flag)} => b_COMP_PROP_FAPP1. $comp_prop_fapp1(_X,_Y,_N,0) => true. $comp_prop_fapp1(X,Y,N,1) => % X*Y<0 fails $constructive_or_prop1(X,Y,N),$constructive_or_prop1(Y,X,N). $comp_prop_fapp1(X,Y,_N,_) => % (abs(X-Y)#>=N) fails $opposite_sign_or_zero(X,Y). /* (X*Y#>0) #\/ (abs(abs(X)-abs(Y))#>=N), X to Y */ /* Bind Flag to: 0 if either (X*Y#>0) or (abs(abs(X)-abs(Y))#>=N) 01 if (X*Y#>0) fails because X<=0 Y>= 0 10 if (X*Y#>0) fails because X>=0 Y<= 0 2 if (abs(abs(X)-abs(Y))#>=N) fails */ :-determinate fd_new_var/1,$same_sign_or_zero/2,$linear_constr_eq_2_ARC/5. $comp_prop_fapp2(X,Y,_N,Flag),var(Flag),{ins(X),bound(X),ins(Y),bound(Y),ins(Flag)} => b_COMP_PROP_FAPP2. $comp_prop_fapp2(_X,_Y,_N,0) => true. $comp_prop_fapp2(X,Y,N,01) => % X=<0 Y>=0 (integer(X)->MX is -X; fd_new_var(MX), $linear_constr_eq_2_ARC(0,1,1,X,MX)), $constructive_or_prop1(MX,Y,N), $constructive_or_prop1(Y,MX,N). $comp_prop_fapp2(X,Y,N,10) => % X>=0 Y=<0 (integer(Y)->MY is -Y; fd_new_var(MY), $linear_constr_eq_2_ARC(0,1,1,Y,MY)), $constructive_or_prop1(X,MY,N), $constructive_or_prop1(MY,X,N). $comp_prop_fapp2(X,Y,_N,_Flag) => /* Flag=2, abs(abs(X)-abs(Y))#>=N fails */ $same_sign_or_zero(X,Y). %%%%%%%%% solve_vars(Vars,TimeLimit,[Strategy]) => % writeln(user,try(Strategy,TimeLimit)), % solve_vars_aux_nolimit(Vars,Strategy). solve_vars_aux(Vars,Strategy,TimeLimit,_Result). solve_vars(Vars,TimeLimit,[Strategy|_Strategies]):-true ? TimeLimitForThisTry is TimeLimit//2, % writeln(user,try(Strategy,TimeLimitForThisTry)), solve_vars_aux(Vars,Strategy,TimeLimitForThisTry,Result), (Result\=time_out->true; fail). solve_vars(Vars,TimeLimit,[_Strategy|Strategies]) => TimeLimitRest is TimeLimit-TimeLimit//2, solve_vars(Vars,TimeLimitRest,Strategies). solve_vars_aux(Vars,Strategy,TimeLimit,Result):- time_out(solver_labeling(Vars,Strategy),TimeLimit,Result),!, (Result==success-> writeln('c '(Strategy)), write('s SATISFIABLE'),nl, write('v'),write(' '), write_list(Vars),nl; true). solve_vars_aux(_Vars,Strategy,_TimeLimit,Result):- Result=fail, writeln('c '(Strategy)), write('s UNSATISFIABLE'),nl. solve_vars_aux_nolimit(Vars,Strategy):- solver_labeling(Vars,Strategy),!, writeln('c '(Strategy)), write('s SATISFIABLE'),nl, write('v'),write(' '),write_list(Vars),nl. solve_vars_aux_nolimit(_Vars,Strategy):- writeln('c '(Strategy)), write('s UNSATISFIABLE'),nl. solver_labeling([],_Strategy) => true. solver_labeling([V|Vs],Strategy), nonvar(V) => solver_labeling(Vs,Strategy). solver_labeling([V|Vs],Strategy), get_attr(V,scc_num,SccNo) => collect_vars_in_scc(Vs,SccNo,Scc,Rest), labeling([Strategy],[V|Scc]),!, solver_labeling(Rest,Strategy). solver_labeling([V|Vs],Strategy) => indomain(V), solver_labeling(Vs,Strategy). collect_vars_in_scc([],_SccNo,Scc,Rest) => Scc=[],Rest=[]. collect_vars_in_scc([V|Vs],SccNo,Scc,Rest), nonvar(V) => collect_vars_in_scc(Vs,SccNo,Scc,Rest). collect_vars_in_scc([V|Vs],SccNo,Scc,Rest), get_attr(V,scc_num,SccNo) => Scc=[V|SccR], collect_vars_in_scc(Vs,SccNo,SccR,Rest). collect_vars_in_scc([V|Vs],SccNo,Scc,Rest) => Rest=[V|RestR], collect_vars_in_scc(Vs,SccNo,Scc,RestR). % All variables in a strongly-collected-component share the same identity variable SCC constr_scope_tuple(Arity,Vars):- constr_scope_tuple(Arity,Vars,_SCC). constr_scope_tuple(0,_Vect,_SCC) => true. constr_scope_tuple(I,Vect,SCC) => arg(I,Vect,V), (var(V)->put_attr_no_hook(V,scc_num,SCC);true), I1 is I-1, constr_scope_tuple(I1,Vect,SCC). constr_scope(Vars):- constr_scope(Vars,_SCC). constr_scope([],_SCC) => true. constr_scope([V|Vs],SCC) => (var(V)->put_attr_no_hook(V,scc_num,SCC);true), constr_scope(Vs,SCC). %% call_all_distinct(Vs):- constr_scope(Vs,_SCC), all_distinct(Vs). %% call_cumulative(Os,Ds,Es,Hs,Limit):- cumulative_no_dvar(Es),!, constr_scope(Os,SCC), constr_scope(Ds,SCC), constr_scope(Hs,SCC), cumulative(Os,Ds,Hs,Limit). call_cumulative(Os,Ds,Es,Hs,Limit):- constr_scope(Os,SCC), constr_scope(Ds,SCC), constr_scope(Es,SCC), constr_scope(Hs,SCC), relate_os_es(Os,Ds,Es), cumulative(Os,Ds,Hs,Limit). cumulative_no_dvar([]) => true. cumulative_no_dvar([X|_]), dvar_or_int(X) => fail. cumulative_no_dvar([_|Xs]) => cumulative_no_dvar(Xs). relate_os_es([],_Ds,_Es) => true. relate_os_es([O|Os],[D|Ds],[E|Es]) => O+D #= E, relate_os_es(Os,Ds,Es). %% call_element(I,As,V):- constr_scope([I,V|As],_SCC), element(I,As,V). %% call_weightedSum(Coes,Vs,Rel,Rhs):- % constr_scope([Rhs|Vs],_SCC), rel_to_constr(Rel,ConstrRel),!, scalar_product(Coes,Vs,ConstrRel,Rhs). rel_to_constr(eq,'#='). rel_to_constr(ne,'#\\='). rel_to_constr(ge,'#>='). rel_to_constr(gt,'#>'). rel_to_constr(le,'#=<'). rel_to_constr(lt,'#<'). write_list([]) => true. write_list([X|Xs]) => write(X),write(' '), write_list(Xs). /****************************************************************/ %% Let X1 = P1//N, Y1 = P1 mod N, X2 = P2//N, Y2 = P2 mod N %% abs(X1-X2)=1 /\ abs(Y1-Y2)=2 \/ abs(X1-X2)=2 /\ abs(Y1-Y2)=1 $knightMove(P1,P2,N):- CompVars=(P1,P2), domain_min_max(P1,Min1,Max1), $create_knight_moves(P1,Min1,Max1,N,P2,Tuples), CompVars in Tuples. $create_knight_moves(_P1,Max,Max,N,P2,Tuples) => $create_knight_moves_aux(Max,N,P2,Tuples,[]). $create_knight_moves(P1,Cur,Max,N,P2,Tuples) => $create_knight_moves_aux(Cur,N,P2,Tuples,Tuples1), b_DM_NEXT_ccf(P1,Cur,Next), $create_knight_moves(P1,Next,Max,N,P2,Tuples1). $create_knight_moves_aux(Code1,N,P2,Tuples,TuplesR):- X is Code1//N, Y is Code1 mod N, X1 is X+1, Y1 is Y+2, $add_knight_move(Code1,X1,Y1,N,P2,Tuples,Tuples1), X2 is X+1, Y2 is Y-2, $add_knight_move(Code1,X2,Y2,N,P2,Tuples1,Tuples2), X3 is X-1, Y3 is Y+2, $add_knight_move(Code1,X3,Y3,N,P2,Tuples2,Tuples3), X4 is X-1, Y4 is Y-2, $add_knight_move(Code1,X4,Y4,N,P2,Tuples3,Tuples4), X5 is X+2, Y5 is Y+1, $add_knight_move(Code1,X5,Y5,N,P2,Tuples4,Tuples5), X6 is X+2, Y6 is Y-1, $add_knight_move(Code1,X6,Y6,N,P2,Tuples5,Tuples6), X7 is X-2, Y7 is Y+1, $add_knight_move(Code1,X7,Y7,N,P2,Tuples6,Tuples7), X8 is X-2, Y8 is Y-1, $add_knight_move(Code1,X8,Y8,N,P2,Tuples7,TuplesR). $add_knight_move(Code1,X,Y,N,P2,Tuples,TuplesR), X>=0,Y>=0,Y Code2 is X*N+Y, (b_DM_TRUE_cc(P2,Code2)->Tuples=[(Code1,Code2)|TuplesR];Tuples=TuplesR). $add_knight_move(_Code1,_X,_Y,_N,_P2,Tuples,TuplesR) => Tuples=TuplesR. % (P1 mod N#=P2 mod N) or % (P1//N#=P2//N) or % (abs(P1//N-P2//N)#=abs(P1 mod N-P2 mod N)), $queenMove(P1,P2,N):- CompVars=(P1,P2), domain_min_max(P1,Min1,Max1), $create_queen_moves(P1,Min1,Max1,N,P2,Tuples), CompVars in Tuples. $create_queen_moves(_P1,Max,Max,N,P2,Tuples) => $create_queen_moves2(Max,N,P2,Tuples,[]). $create_queen_moves(P1,Cur,Max,N,P2,Tuples) => $create_queen_moves2(Cur,N,P2,Tuples,Tuples1), b_DM_NEXT_ccf(P1,Cur,Next), $create_queen_moves(P1,Next,Max,N,P2,Tuples1). $create_queen_moves2(I1,N,P2,Tuples,TuplesR):- domain_min_max(P2,Min2,Max2), $create_queen_moves2(I1,N,P2,Min2,Max2,Tuples,TuplesR). $create_queen_moves2(I1,N,_P2,I2,Max,Tuples,TuplesR), I2==Max => ($isQueenMove(I1,I2,N)-> Tuples=[(I1,I2)|TuplesR];Tuples=TuplesR). $create_queen_moves2(I1,N,P2,I2,Max,Tuples,TuplesR) => ($isQueenMove(I1,I2,N)-> Tuples=[(I1,I2)|Tuples1];Tuples=Tuples1), b_DM_NEXT_ccf(P2,I2,NextI2), $create_queen_moves2(I1,N,P2,NextI2,Max,Tuples1,TuplesR). $isQueenMove(I1,I2,N),I1 mod N =:= I2 mod N => true. $isQueenMove(I1,I2,N), I1//N =:= I2//N => true. $isQueenMove(I1,I2,N), abs(I1//N-I2//N)=:=abs(I1 mod N-I2 mod N) => true. dump_props:- tell(trace), csp(_), frozen(L), writeln(L), told.