% RA: Relación 02
% OTTER: puzle2.in
% Departamento de Ciencias de la Computación e Inteligencia Artificial
%==============================================================================


%==============================================================================
% Enunciado
%==============================================================================

% Un puzle está compuesto por las siguientes cuatro fichas:
%
%         +----+        +----+        +----+        +----+
%         |\  /|        |\  /|        |\  /|        |\  /|
%         |R\/V|        |V\/R|        |A\/V|        |R\/A|
%         |R/\V|        |V/\R|        |A/\V|        |R/\A|
%         |/  \|        |/  \|        |/  \|        |/  \|
%         +----+        +----+        +----+        +----+
%
% Donde R, V y A representan los colores Rojo, Verde y Azul, respectivamente.
%
% Utilizar OTTER para encontrar todas las maneras posibles de colocar estas
% cuatro fichas en línea, sin repetir, de forma lo colores de los lados
% adyacentes coincidan. En este caso las fichas se pueden girar.

%==============================================================================
% Formalización
%==============================================================================

% Configuración del sistema

set(hyper_res).
set(para_from).
set(para_into).
assign(max_proofs,-1).

% Lenguaje del problema

% Constantes:
%  PiezaA, PiezaB, PiezaC, PiezaD : Identificadores de las piezas.
%  Rojo, Verde, Azul : Colores disponibles.

% Propiedades:
%  Ficha(X,Y1,Y2) :
%    La pieza X tiene los colores Y1 e Y2 a la izquierda y a la derecha,
%    respectivamente. 
%  orden(X1,X2,X3,X4) :
%    Las secuencia de piezas [X1,X2,X3,X4] forma una solución al puzle.

formula_list(usable).
% Reflexividad
 all x (x = x).

% Las piezas son distintas
 PiezaA != PiezaB.
 PiezaA != PiezaC.
 PiezaA != PiezaD.
 PiezaB != PiezaC.
 PiezaB != PiezaD.
 PiezaD != PiezaC.

% Descripción de las piezas
 Ficha(PiezaA,0,Rojo,Verde).
 Ficha(PiezaB,0,Verde,Rojo).
 Ficha(PiezaC,0,Azul,Verde).
 Ficha(PiezaD,0,Rojo,Azul).
end_of_list.

formula_list(sos).
% Girar las piezas
 all x y z (Ficha(x,0,y,z) -> Ficha(x,1,z,y)).

% Caracterización de 4 piezas que cumplen las restricciones del puzle.
 all x1 x2 x3 x4 y0 y1 y2 y3 y4 i1 i2 i3 i4
  ((Ficha(x1,i1,y0,y1) & Ficha(x2,i2,y1,y2) & Ficha(x3,i3,y2,y3) & Ficha(x4,i4,y3,y4) &
    (x1 != x2) & (x1 != x3) & (x1 != x4) &
    (x2 != x3) & (x2 != x4) & (x3 != x4)) ->
    orden(x1,i1,x2,i2,x3,i3,x4,i4)).
end_of_list.

formula_list(passive).
 all x1 x2 x3 x4 i1 i2 i3 i4
  (orden(x1,i1,x2,i2,x3,i3,x4,i4) -> $ANS(x1,i1,x2,i2,x3,i3,x4,i4)).
end_of_list.

%==============================================================================
% Soluciones:
%==============================================================================

% Se obtienen las siguientes soluciones:
%
%  $ANS(PiezaA,1,PiezaB,1,PiezaC,1,PiezaD,1).
%  $ANS(PiezaA,1,PiezaD,0,PiezaC,0,PiezaB,0).
%  $ANS(PiezaB,1,PiezaA,1,PiezaD,0,PiezaC,0).
%  $ANS(PiezaB,1,PiezaC,1,PiezaD,1,PiezaA,0).
%  $ANS(PiezaC,1,PiezaD,1,PiezaA,0,PiezaB,0).
%  $ANS(PiezaD,0,PiezaC,0,PiezaA,1,PiezaB,1).
%  $ANS(PiezaD,0,PiezaC,0,PiezaB,0,PiezaA,0).
%  $ANS(PiezaB,0,PiezaD,0,PiezaC,0,PiezaA,1).
%  $ANS(PiezaB,0,PiezaA,0,PiezaC,1,PiezaD,1).
%  $ANS(PiezaA,0,PiezaC,1,PiezaD,1,PiezaB,1).
%  $ANS(PiezaA,0,PiezaB,0,PiezaD,0,PiezaC,0).
%  $ANS(PiezaC,1,PiezaD,1,PiezaB,1,PiezaA,1).

%==============================================================================
