簡単な数独を解くNuSMVソースコード

sudoku_easy.smv

MODULE main

DEFINE
  A1 := 8;
  A2 := 6;
  A3 := 1;
  A7 := 2;
  B0 := 3;
  B1 := 2;
  B2 := 4;
  B6 := 1;
  B8 := 5;
  C0 := 7;
  C1 := 5;
  C2 := 1;
  C3 := 3;
  C4 := 2;
  C6 := 9;
  C7 := 8;
  C8 := 6;
  D0 := 2;
  D1 := 4;
  D2 := 3;
  D3 := 9;
  D4 := 8;
  D5 := 6;
  D8 := 1;
  E3 := 7;
  E5 := 1;
  F0 := 5;
  F3 := 2;
  F4 := 4;
  F5 := 3;
  F6 := 8;
  F7 := 6;
  F8 := 9;
  G0 := 6;
  G1 := 9;
  G2 := 8;
  G4 := 1;
  G5 := 7;
  G6 := 4;
  G7 := 3;
  G8 := 2;
  H0 := 1;
  H2 := 5;
  H6 := 6;
  H7 := 9;
  H8 := 8;
  I1 := 3;
  I5 := 9;
  I6 := 5;
  I7 := 1;

VAR
  A0 : {0, 9};
  A4 : {0, 5, 7, 9};
  A5 : {0, 4, 5};
  A6 : {0, 3, 7};
  A8 : {0, 3, 4, 7};
  B3 : {0, 6, 8};
  B4 : {0, 6, 7, 9};
  B5 : {0, 8};
  B7 : {0, 7};
  C5 : {0, 4};
  D6 : {0, 7};
  D7 : {0, 5, 7};
  E0 : {0, 8, 9};
  E1 : {0, 6};
  E2 : {0, 9};
  E4 : {0, 5};
  E6 : {0, 2, 3};
  E7 : {0, 4, 5};
  E8 : {0, 3, 4};
  F1 : {0, 1, 7};
  F2 : {0, 7};
  G3 : {0, 5};
  H1 : {0, 7};
  H3 : {0, 4};
  H4 : {0, 3};
  H5 : {0, 2, 4};
  I0 : {0, 4};
  I2 : {0, 2, 7};
  I3 : {0, 4, 6, 8};
  I4 : {0, 6};
  I8 : {0, 7};

ASSIGN
  init(A0) := 0;
  next(A0) := case
    TRUE : {9};
  esac;

  init(A4) := 0;
  next(A4) := case
    TRUE : {5, 7, 9};
  esac;

  init(A5) := 0;
  next(A5) := case
    TRUE : {4, 5};
  esac;

  init(A6) := 0;
  next(A6) := case
    TRUE : {3, 7};
  esac;

  init(A8) := 0;
  next(A8) := case
    TRUE : {3, 4, 7};
  esac;

  init(B3) := 0;
  next(B3) := case
    TRUE : {6, 8};
  esac;

  init(B4) := 0;
  next(B4) := case
    TRUE : {6, 7, 9};
  esac;

  init(B5) := 0;
  next(B5) := case
    TRUE : {8};
  esac;

  init(B7) := 0;
  next(B7) := case
    TRUE : {7};
  esac;

  init(C5) := 0;
  next(C5) := case
    TRUE : {4};
  esac;

  init(D6) := 0;
  next(D6) := case
    TRUE : {7};
  esac;

  init(D7) := 0;
  next(D7) := case
    TRUE : {5, 7};
  esac;

  init(E0) := 0;
  next(E0) := case
    TRUE : {8, 9};
  esac;

  init(E1) := 0;
  next(E1) := case
    TRUE : {6};
  esac;

  init(E2) := 0;
  next(E2) := case
    TRUE : {9};
  esac;

  init(E4) := 0;
  next(E4) := case
    TRUE : {5};
  esac;

  init(E6) := 0;
  next(E6) := case
    TRUE : {2, 3};
  esac;

  init(E7) := 0;
  next(E7) := case
    TRUE : {4, 5};
  esac;

  init(E8) := 0;
  next(E8) := case
    TRUE : {3, 4};
  esac;

  init(F1) := 0;
  next(F1) := case
    TRUE : {1, 7};
  esac;

  init(F2) := 0;
  next(F2) := case
    TRUE : {7};
  esac;

  init(G3) := 0;
  next(G3) := case
    TRUE : {5};
  esac;

  init(H1) := 0;
  next(H1) := case
    TRUE : {7};
  esac;

  init(H3) := 0;
  next(H3) := case
    TRUE : {4};
  esac;

  init(H4) := 0;
  next(H4) := case
    TRUE : {3};
  esac;

  init(H5) := 0;
  next(H5) := case
    TRUE : {2, 4};
  esac;

  init(I0) := 0;
  next(I0) := case
    TRUE : {4};
  esac;

  init(I2) := 0;
  next(I2) := case
    TRUE : {2, 7};
  esac;

  init(I3) := 0;
  next(I3) := case
    TRUE : {4, 6, 8};
  esac;

  init(I4) := 0;
  next(I4) := case
    TRUE : {6};
  esac;

  init(I8) := 0;
  next(I8) := case
    TRUE : {7};
  esac;


SPEC
!EF(
!(A0 = A4) &
!(A0 = A5) &
!(A0 = A6) &
!(A0 = A8) &
!(A4 = A5) &
!(A4 = A6) &
!(A4 = A8) &
!(A5 = A6) &
!(A5 = A8) &
!(A6 = A8) &
!(B3 = B4) &
!(B3 = B5) &
!(B3 = B7) &
!(B4 = B5) &
!(B4 = B7) &
!(B5 = B7) &
!(D6 = D7) &
!(E0 = E1) &
!(E0 = E2) &
!(E0 = E4) &
!(E0 = E6) &
!(E0 = E7) &
!(E0 = E8) &
!(E1 = E2) &
!(E1 = E4) &
!(E1 = E6) &
!(E1 = E7) &
!(E1 = E8) &
!(E2 = E4) &
!(E2 = E6) &
!(E2 = E7) &
!(E2 = E8) &
!(E4 = E6) &
!(E4 = E7) &
!(E4 = E8) &
!(E6 = E7) &
!(E6 = E8) &
!(E7 = E8) &
!(F1 = F2) &
!(H1 = H3) &
!(H1 = H4) &
!(H1 = H5) &
!(H3 = H4) &
!(H3 = H5) &
!(H4 = H5) &
!(I0 = I2) &
!(I0 = I3) &
!(I0 = I4) &
!(I0 = I8) &
!(I2 = I3) &
!(I2 = I4) &
!(I2 = I8) &
!(I3 = I4) &
!(I3 = I8) &
!(I4 = I8) &
!(A0 = E0) &
!(A0 = I0) &
!(A4 = B4) &
!(A4 = E4) &
!(A4 = H4) &
!(A4 = I4) &
!(A5 = B5) &
!(A5 = C5) &
!(A5 = H5) &
!(A6 = D6) &
!(A6 = E6) &
!(A8 = E8) &
!(A8 = I8) &
!(B3 = G3) &
!(B3 = H3) &
!(B3 = I3) &
!(B4 = E4) &
!(B4 = H4) &
!(B4 = I4) &
!(B5 = C5) &
!(B5 = H5) &
!(B7 = D7) &
!(B7 = E7) &
!(C5 = H5) &
!(D6 = E6) &
!(D7 = E7) &
!(E0 = I0) &
!(E1 = F1) &
!(E1 = H1) &
!(E2 = F2) &
!(E2 = I2) &
!(E4 = H4) &
!(E4 = I4) &
!(E8 = I8) &
!(F1 = H1) &
!(F2 = I2) &
!(G3 = H3) &
!(G3 = I3) &
!(H3 = I3) &
!(H4 = I4) &
!(A0 = A1) &
!(A0 = A2) &
!(A0 = B0) &
!(A0 = B1) &
!(A0 = B2) &
!(A0 = C0) &
!(A0 = C1) &
!(A0 = C2) &
!(A1 = A2) &
!(A1 = B0) &
!(A1 = B1) &
!(A1 = B2) &
!(A1 = C0) &
!(A1 = C1) &
!(A1 = C2) &
!(A2 = B0) &
!(A2 = B1) &
!(A2 = B2) &
!(A2 = C0) &
!(A2 = C1) &
!(A2 = C2) &
!(B0 = B1) &
!(B0 = B2) &
!(B0 = C0) &
!(B0 = C1) &
!(B0 = C2) &
!(B1 = B2) &
!(B1 = C0) &
!(B1 = C1) &
!(B1 = C2) &
!(B2 = C0) &
!(B2 = C1) &
!(B2 = C2) &
!(C0 = C1) &
!(C0 = C2) &
!(C1 = C2) &
!(A3 = A4) &
!(A3 = A5) &
!(A3 = B3) &
!(A3 = B4) &
!(A3 = B5) &
!(A3 = C3) &
!(A3 = C4) &
!(A3 = C5) &
!(A4 = A5) &
!(A4 = B3) &
!(A4 = B4) &
!(A4 = B5) &
!(A4 = C3) &
!(A4 = C4) &
!(A4 = C5) &
!(A5 = B3) &
!(A5 = B4) &
!(A5 = B5) &
!(A5 = C3) &
!(A5 = C4) &
!(A5 = C5) &
!(B3 = B4) &
!(B3 = B5) &
!(B3 = C3) &
!(B3 = C4) &
!(B3 = C5) &
!(B4 = B5) &
!(B4 = C3) &
!(B4 = C4) &
!(B4 = C5) &
!(B5 = C3) &
!(B5 = C4) &
!(B5 = C5) &
!(C3 = C4) &
!(C3 = C5) &
!(C4 = C5) &
!(A6 = A7) &
!(A6 = A8) &
!(A6 = B6) &
!(A6 = B7) &
!(A6 = B8) &
!(A6 = C6) &
!(A6 = C7) &
!(A6 = C8) &
!(A7 = A8) &
!(A7 = B6) &
!(A7 = B7) &
!(A7 = B8) &
!(A7 = C6) &
!(A7 = C7) &
!(A7 = C8) &
!(A8 = B6) &
!(A8 = B7) &
!(A8 = B8) &
!(A8 = C6) &
!(A8 = C7) &
!(A8 = C8) &
!(B6 = B7) &
!(B6 = B8) &
!(B6 = C6) &
!(B6 = C7) &
!(B6 = C8) &
!(B7 = B8) &
!(B7 = C6) &
!(B7 = C7) &
!(B7 = C8) &
!(B8 = C6) &
!(B8 = C7) &
!(B8 = C8) &
!(C6 = C7) &
!(C6 = C8) &
!(C7 = C8) &
!(D0 = D1) &
!(D0 = D2) &
!(D0 = E0) &
!(D0 = E1) &
!(D0 = E2) &
!(D0 = F0) &
!(D0 = F1) &
!(D0 = F2) &
!(D1 = D2) &
!(D1 = E0) &
!(D1 = E1) &
!(D1 = E2) &
!(D1 = F0) &
!(D1 = F1) &
!(D1 = F2) &
!(D2 = E0) &
!(D2 = E1) &
!(D2 = E2) &
!(D2 = F0) &
!(D2 = F1) &
!(D2 = F2) &
!(E0 = E1) &
!(E0 = E2) &
!(E0 = F0) &
!(E0 = F1) &
!(E0 = F2) &
!(E1 = E2) &
!(E1 = F0) &
!(E1 = F1) &
!(E1 = F2) &
!(E2 = F0) &
!(E2 = F1) &
!(E2 = F2) &
!(F0 = F1) &
!(F0 = F2) &
!(F1 = F2) &
!(D3 = D4) &
!(D3 = D5) &
!(D3 = E3) &
!(D3 = E4) &
!(D3 = E5) &
!(D3 = F3) &
!(D3 = F4) &
!(D3 = F5) &
!(D4 = D5) &
!(D4 = E3) &
!(D4 = E4) &
!(D4 = E5) &
!(D4 = F3) &
!(D4 = F4) &
!(D4 = F5) &
!(D5 = E3) &
!(D5 = E4) &
!(D5 = E5) &
!(D5 = F3) &
!(D5 = F4) &
!(D5 = F5) &
!(E3 = E4) &
!(E3 = E5) &
!(E3 = F3) &
!(E3 = F4) &
!(E3 = F5) &
!(E4 = E5) &
!(E4 = F3) &
!(E4 = F4) &
!(E4 = F5) &
!(E5 = F3) &
!(E5 = F4) &
!(E5 = F5) &
!(F3 = F4) &
!(F3 = F5) &
!(F4 = F5) &
!(D6 = D7) &
!(D6 = D8) &
!(D6 = E6) &
!(D6 = E7) &
!(D6 = E8) &
!(D6 = F6) &
!(D6 = F7) &
!(D6 = F8) &
!(D7 = D8) &
!(D7 = E6) &
!(D7 = E7) &
!(D7 = E8) &
!(D7 = F6) &
!(D7 = F7) &
!(D7 = F8) &
!(D8 = E6) &
!(D8 = E7) &
!(D8 = E8) &
!(D8 = F6) &
!(D8 = F7) &
!(D8 = F8) &
!(E6 = E7) &
!(E6 = E8) &
!(E6 = F6) &
!(E6 = F7) &
!(E6 = F8) &
!(E7 = E8) &
!(E7 = F6) &
!(E7 = F7) &
!(E7 = F8) &
!(E8 = F6) &
!(E8 = F7) &
!(E8 = F8) &
!(F6 = F7) &
!(F6 = F8) &
!(F7 = F8) &
!(G0 = G1) &
!(G0 = G2) &
!(G0 = H0) &
!(G0 = H1) &
!(G0 = H2) &
!(G0 = I0) &
!(G0 = I1) &
!(G0 = I2) &
!(G1 = G2) &
!(G1 = H0) &
!(G1 = H1) &
!(G1 = H2) &
!(G1 = I0) &
!(G1 = I1) &
!(G1 = I2) &
!(G2 = H0) &
!(G2 = H1) &
!(G2 = H2) &
!(G2 = I0) &
!(G2 = I1) &
!(G2 = I2) &
!(H0 = H1) &
!(H0 = H2) &
!(H0 = I0) &
!(H0 = I1) &
!(H0 = I2) &
!(H1 = H2) &
!(H1 = I0) &
!(H1 = I1) &
!(H1 = I2) &
!(H2 = I0) &
!(H2 = I1) &
!(H2 = I2) &
!(I0 = I1) &
!(I0 = I2) &
!(I1 = I2) &
!(G3 = G4) &
!(G3 = G5) &
!(G3 = H3) &
!(G3 = H4) &
!(G3 = H5) &
!(G3 = I3) &
!(G3 = I4) &
!(G3 = I5) &
!(G4 = G5) &
!(G4 = H3) &
!(G4 = H4) &
!(G4 = H5) &
!(G4 = I3) &
!(G4 = I4) &
!(G4 = I5) &
!(G5 = H3) &
!(G5 = H4) &
!(G5 = H5) &
!(G5 = I3) &
!(G5 = I4) &
!(G5 = I5) &
!(H3 = H4) &
!(H3 = H5) &
!(H3 = I3) &
!(H3 = I4) &
!(H3 = I5) &
!(H4 = H5) &
!(H4 = I3) &
!(H4 = I4) &
!(H4 = I5) &
!(H5 = I3) &
!(H5 = I4) &
!(H5 = I5) &
!(I3 = I4) &
!(I3 = I5) &
!(I4 = I5) &
!(G6 = G7) &
!(G6 = G8) &
!(G6 = H6) &
!(G6 = H7) &
!(G6 = H8) &
!(G6 = I6) &
!(G6 = I7) &
!(G6 = I8) &
!(G7 = G8) &
!(G7 = H6) &
!(G7 = H7) &
!(G7 = H8) &
!(G7 = I6) &
!(G7 = I7) &
!(G7 = I8) &
!(G8 = H6) &
!(G8 = H7) &
!(G8 = H8) &
!(G8 = I6) &
!(G8 = I7) &
!(G8 = I8) &
!(H6 = H7) &
!(H6 = H8) &
!(H6 = I6) &
!(H6 = I7) &
!(H6 = I8) &
!(H7 = H8) &
!(H7 = I6) &
!(H7 = I7) &
!(H7 = I8) &
!(H8 = I6) &
!(H8 = I7) &
!(H8 = I8) &
!(I6 = I7) &
!(I6 = I8) &
!(I7 = I8)
)