ちょっと難しい数独を解くNuSMVソースコード

sudoku_mid.smv

MODULE main

DEFINE
  A0 := 3;
  A2 := 2;
  A5 := 5;
  A6 := 7;
  A7 := 4;
  A8 := 9;
  B2 := 6;
  B5 := 9;
  B7 := 1;
  B8 := 2;
  C2 := 4;
  C3 := 3;
  C5 := 2;
  D3 := 9;
  D7 := 3;
  E0 := 4;
  E2 := 7;
  E4 := 3;
  E6 := 6;
  E8 := 8;
  F1 := 3;
  F5 := 6;
  G3 := 1;
  G5 := 3;
  G6 := 8;
  H0 := 8;
  H1 := 6;
  H3 := 4;
  H6 := 1;
  I0 := 1;
  I1 := 2;
  I2 := 3;
  I3 := 6;
  I6 := 4;
  I8 := 7;

VAR
  A1 : {0, 1, 8};
  A3 : {0, 8};
  A4 : {0, 1, 6, 8};
  B0 : {0, 5, 7};
  B1 : {0, 5, 7, 8};
  B3 : {0, 7, 8};
  B4 : {0, 4, 7, 8};
  B6 : {0, 3, 5};
  C0 : {0, 5, 7, 9};
  C1 : {0, 1, 5, 7, 8, 9};
  C4 : {0, 1, 6, 7, 8};
  C6 : {0, 5};
  C7 : {0, 5, 6, 8};
  C8 : {0, 5, 6};
  D0 : {0, 2, 5, 6};
  D1 : {0, 1, 5, 8};
  D2 : {0, 1, 5, 8};
  D4 : {0, 1, 2, 4, 5, 7, 8};
  D5 : {0, 1, 4, 7, 8};
  D6 : {0, 2, 5};
  D8 : {0, 1, 4, 5};
  E1 : {0, 1, 5, 9};
  E3 : {0, 2, 5};
  E5 : {0, 1};
  E7 : {0, 2, 5, 9};
  F0 : {0, 2, 5, 9};
  F2 : {0, 1, 5, 8, 9};
  F3 : {0, 2, 5, 7, 8};
  F4 : {0, 1, 2, 4, 5, 7, 8};
  F6 : {0, 2, 5, 9};
  F7 : {0, 2, 5, 7, 9};
  F8 : {0, 1, 4, 5};
  G0 : {0, 5, 7, 9};
  G1 : {0, 4, 5, 7, 9};
  G2 : {0, 5, 9};
  G4 : {0, 2, 5, 7, 9};
  G7 : {0, 2, 5, 6, 9};
  G8 : {0, 5, 6};
  H2 : {0, 5, 9};
  H4 : {0, 2, 5, 7, 9};
  H5 : {0, 7};
  H7 : {0, 2, 5, 9};
  H8 : {0, 3, 5};
  I4 : {0, 5, 8, 9};
  I5 : {0, 8};
  I7 : {0, 5, 9};

ASSIGN
  init(A1) := 0;
  next(A1) := case
    TRUE : {1, 8};
  esac;

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

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

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

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

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

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

  init(B6) := 0;
  next(B6) := case
    TRUE : {3, 5};
  esac;

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

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

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

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

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

  init(C8) := 0;
  next(C8) := case
    TRUE : {5, 6};
  esac;

  init(D0) := 0;
  next(D0) := case
    TRUE : {2, 5, 6};
  esac;

  init(D1) := 0;
  next(D1) := case
    TRUE : {1, 5, 8};
  esac;

  init(D2) := 0;
  next(D2) := case
    TRUE : {1, 5, 8};
  esac;

  init(D4) := 0;
  next(D4) := case
    TRUE : {1, 2, 4, 5, 7, 8};
  esac;

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

  init(D6) := 0;
  next(D6) := case
    TRUE : {2, 5};
  esac;

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

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

  init(E3) := 0;
  next(E3) := case
    TRUE : {2, 5};
  esac;

  init(E5) := 0;
  next(E5) := case
    TRUE : {1};
  esac;

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

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

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

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

  init(F4) := 0;
  next(F4) := case
    TRUE : {1, 2, 4, 5, 7, 8};
  esac;

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

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

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

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

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

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

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

  init(G7) := 0;
  next(G7) := case
    TRUE : {2, 5, 6, 9};
  esac;

  init(G8) := 0;
  next(G8) := case
    TRUE : {5, 6};
  esac;

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

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

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

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

  init(H8) := 0;
  next(H8) := case
    TRUE : {3, 5};
  esac;

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

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

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


SPEC
!EF(
!(A1 = A3) &
!(A1 = A4) &
!(A3 = A4) &
!(B0 = B1) &
!(B0 = B3) &
!(B0 = B4) &
!(B0 = B6) &
!(B1 = B3) &
!(B1 = B4) &
!(B1 = B6) &
!(B3 = B4) &
!(B3 = B6) &
!(B4 = B6) &
!(C0 = C1) &
!(C0 = C4) &
!(C0 = C6) &
!(C0 = C7) &
!(C0 = C8) &
!(C1 = C4) &
!(C1 = C6) &
!(C1 = C7) &
!(C1 = C8) &
!(C4 = C6) &
!(C4 = C7) &
!(C4 = C8) &
!(C6 = C7) &
!(C6 = C8) &
!(C7 = C8) &
!(D0 = D1) &
!(D0 = D2) &
!(D0 = D4) &
!(D0 = D5) &
!(D0 = D6) &
!(D0 = D8) &
!(D1 = D2) &
!(D1 = D4) &
!(D1 = D5) &
!(D1 = D6) &
!(D1 = D8) &
!(D2 = D4) &
!(D2 = D5) &
!(D2 = D6) &
!(D2 = D8) &
!(D4 = D5) &
!(D4 = D6) &
!(D4 = D8) &
!(D5 = D6) &
!(D5 = D8) &
!(D6 = D8) &
!(E1 = E3) &
!(E1 = E5) &
!(E1 = E7) &
!(E3 = E5) &
!(E3 = E7) &
!(E5 = E7) &
!(F0 = F2) &
!(F0 = F3) &
!(F0 = F4) &
!(F0 = F6) &
!(F0 = F7) &
!(F0 = F8) &
!(F2 = F3) &
!(F2 = F4) &
!(F2 = F6) &
!(F2 = F7) &
!(F2 = F8) &
!(F3 = F4) &
!(F3 = F6) &
!(F3 = F7) &
!(F3 = F8) &
!(F4 = F6) &
!(F4 = F7) &
!(F4 = F8) &
!(F6 = F7) &
!(F6 = F8) &
!(F7 = F8) &
!(G0 = G1) &
!(G0 = G2) &
!(G0 = G4) &
!(G0 = G7) &
!(G0 = G8) &
!(G1 = G2) &
!(G1 = G4) &
!(G1 = G7) &
!(G1 = G8) &
!(G2 = G4) &
!(G2 = G7) &
!(G2 = G8) &
!(G4 = G7) &
!(G4 = G8) &
!(G7 = G8) &
!(H2 = H4) &
!(H2 = H5) &
!(H2 = H7) &
!(H2 = H8) &
!(H4 = H5) &
!(H4 = H7) &
!(H4 = H8) &
!(H5 = H7) &
!(H5 = H8) &
!(H7 = H8) &
!(I4 = I5) &
!(I4 = I7) &
!(I5 = I7) &
!(A1 = B1) &
!(A1 = C1) &
!(A1 = D1) &
!(A1 = E1) &
!(A1 = G1) &
!(A3 = B3) &
!(A3 = E3) &
!(A3 = F3) &
!(A4 = B4) &
!(A4 = C4) &
!(A4 = D4) &
!(A4 = F4) &
!(A4 = G4) &
!(A4 = H4) &
!(A4 = I4) &
!(B0 = C0) &
!(B0 = D0) &
!(B0 = F0) &
!(B0 = G0) &
!(B1 = C1) &
!(B1 = D1) &
!(B1 = E1) &
!(B1 = G1) &
!(B3 = E3) &
!(B3 = F3) &
!(B4 = C4) &
!(B4 = D4) &
!(B4 = F4) &
!(B4 = G4) &
!(B4 = H4) &
!(B4 = I4) &
!(B6 = C6) &
!(B6 = D6) &
!(B6 = F6) &
!(C0 = D0) &
!(C0 = F0) &
!(C0 = G0) &
!(C1 = D1) &
!(C1 = E1) &
!(C1 = G1) &
!(C4 = D4) &
!(C4 = F4) &
!(C4 = G4) &
!(C4 = H4) &
!(C4 = I4) &
!(C6 = D6) &
!(C6 = F6) &
!(C7 = E7) &
!(C7 = F7) &
!(C7 = G7) &
!(C7 = H7) &
!(C7 = I7) &
!(C8 = D8) &
!(C8 = F8) &
!(C8 = G8) &
!(C8 = H8) &
!(D0 = F0) &
!(D0 = G0) &
!(D1 = E1) &
!(D1 = G1) &
!(D2 = F2) &
!(D2 = G2) &
!(D2 = H2) &
!(D4 = F4) &
!(D4 = G4) &
!(D4 = H4) &
!(D4 = I4) &
!(D5 = E5) &
!(D5 = H5) &
!(D5 = I5) &
!(D6 = F6) &
!(D8 = F8) &
!(D8 = G8) &
!(D8 = H8) &
!(E1 = G1) &
!(E3 = F3) &
!(E5 = H5) &
!(E5 = I5) &
!(E7 = F7) &
!(E7 = G7) &
!(E7 = H7) &
!(E7 = I7) &
!(F0 = G0) &
!(F2 = G2) &
!(F2 = H2) &
!(F4 = G4) &
!(F4 = H4) &
!(F4 = I4) &
!(F7 = G7) &
!(F7 = H7) &
!(F7 = I7) &
!(F8 = G8) &
!(F8 = H8) &
!(G2 = H2) &
!(G4 = H4) &
!(G4 = I4) &
!(G7 = H7) &
!(G7 = I7) &
!(G8 = H8) &
!(H4 = I4) &
!(H5 = I5) &
!(H7 = I7) &
!(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)
)