2. Check consistency

The AML Consistency Checker shows:

  • a summary of duples grouped by region,

  • the result of the consistency analysis,

  • if the embedding is inconsistent, it displays the potential source.

Here we use the embedding described in Create an AML Embedding as an example.

2.1. Consistent embedding

An embedding is consistent if no rules enter in contradiction. This contradiction can be difficult to spot when it happens with implicit rules. For instance, \(A < B\) and \(A \nless B\), produce an explicit contradiction. However, \(A < B\), \(B < C\), (implicitly produce \(A < C\), which is not one of the original rules). In this case, a sentence such as \(A \nless C\) would give raise to a contradiction.

If we run the analysis on the N-Queens embedding we obtain that the result is consistent.

python AMLConsistencyChecker.py queens_embedding.py

It also displays a summary of the number of duples generated by the embedding in each region.

Positive duples:

+ region  1 > 64
+ region  5 > 128
+ region  6 > 128
+ region  7 > 124
+ region  9 > 1
+ region  12 > 2

Negative duples:

- region  1 > 8
- region  2 > 8
- region  11 > 64

2.2. Inconsistent embedding

The embedding can be turned inconsistent by adding the following duple

theEmbedding.REGION = 14
ADD(INC(F("Q", 4), F("E", 4)))

If we run the analysis on this modified embedding we obtain that the result is inconsistent this time.

python AMLConsistencyChecker.py queens_embedding.py

First it displays a summary of the duples in the embedding. Notice that there is an additional region with a positive duple:

+ region  14 > 1

This follows with information about the inconsistency. Which negative duple is producing the problem:

Failure in region 1 at:

R[4] !< Q[0]...Q[3] * Q[5]...Q[11] * Q[13]...Q[19] *
        Q[21]...Q[27] * Q[29]...Q[35] * Q[37]...Q[43] *
        Q[45]...Q[51] * Q[53]...Q[59] * Q[61]...Q[63] *
        E[0]...E[63]

This rule indicates that anything besides the Queens at the forth row (\(Q[4]\), \(Q[12]\), …) produce the property \(R[4]\). That constant indicates having a Queen on the forth row.

This output is followed by the positive duples that might be causing the inconsistency:

Potential conflict with:
  in region 1 at:
    R[0]*C[0] < Q[0]
    R[0]*C[1] < Q[8]
    R[0]*C[2] < Q[16]
    R[0]*C[3] < Q[24]
    R[0]*C[4] < Q[32]
    R[0]*C[5] < Q[40]
    R[0]*C[6] < Q[48]
    R[0]*C[7] < Q[56]
    R[1]*C[0] < Q[1]
    R[2]*C[0] < Q[2]
    R[3]*C[0] < Q[3]
    R[5]*C[0] < Q[5]
    R[6]*C[0] < Q[6]
    R[7]*C[0] < Q[7]
    R[4]*C[0] < Q[4]
  in region 14 at:
    Q[4] < E[4]

The inconsistency comes from \(Q[4] < E[4]\) that together with \({R[4],C[0]} < Q[4]\) produces \(R[4] < E[4]\). This duple is inconsistent with the negative duple in region 1, \(R[4] \nless E[4]\).