更好的 Alloy n 皇后模型？

Question

下面是 n 皇后问题（好吧，实际上是 4 皇后问题）的 Alloy 模型。我想知道是否有更好的解决方案？请注意，在我的解决方案中，我反复使用 next 和 prev 来消除对角线上的皇后；这看起来很笨拙。

open util/ordering[Row]

sig Row {}

one sig Column0 {
    row: Row
}

one sig Column1 {
    row: Row
}

one sig Column2 {
    row: Row
}

one sig Column3 {
    row: Row
}

fact {
   #Row = 4
}

fact {
    Column0.row != Column1.row
    Column0.row != Column2.row
    Column0.row != Column3.row
    Column1.row != next.(Column0.row)
    Column2.row != next.next.(Column0.row)
    Column3.row != next.next.next.(Column0.row)
    Column1.row != prev.(Column0.row)
    Column2.row != prev.prev.(Column0.row)
    Column3.row != prev.prev.(Column0.row)

    Column1.row != Column2.row
    Column1.row != Column3.row
    Column2.row != next.(Column1.row)
    Column3.row != next.next.(Column1.row)
    Column2.row != prev.(Column1.row)
    Column3.row != prev.prev.(Column1.row)

    Column2.row != Column3.row
    Column3.row != next.(Column2.row)
    Column3.row != prev.(Column2.row)
}

pred Show {}

run Show for 4

Answer 1

这完全取决于您所说的更好的意思。您的解决方案有一些优点：针对 4 queens/4x4 个板进行了优化，概念数量最少，实例生成的默认图形可视化很好，但也有缺点。（不适用于不同数量的 queens/rows/columns 和 "klunky constraints"）

我向您展示了我提出的一个替代解决方案，它有其缺点（更多概念+约束中的量化可能会减慢分析速度）但也有其优点：简洁和恕我直言，更具可读性的约束和灵活性（适用于任何cols/rows/queens)

的数量

one sig Board{
    cols: seq Column,
    rows: seq Row,
    q: set Queen
}
sig Row {
  id:Int
}{
   id=Board.rows.idxOf[this]
   this in Board.rows.elems
}

sig Column {
  id:Int
}{
  id=Board.cols.idxOf[this]
  this in Board.cols.elems
}
sig Queen{
    x:Column,
    y:Row
}
pred aligned[q1,q2:Queen]{
   q1.y=q2.y 
   or 
   q1.x=q2.x  
   or some a,b:Int{
       add[q1.x.id,a]= q2.x.id 
       add[q1.y.id,b]= q2.y.id
       a=b or a=sub[0,b]
    } 
}
pred Show {
   no disj q1,q2:Queen| aligned[q1,q2]
}
run Show for exactly 4 Row, exactly 4 Column, exactly 4 Queen

请注意，如果没有适当的主题，通过分析获得的实例将很难形象化。这是您可以导入的一个，它会产生漂亮的可视化效果：https://pastebin.com/wwKP6g9h

注意2：您需要禁止整数溢出或将整数的带宽设置得足够大以使对齐谓词中的添加行为符合预期

注意 3：添加了 id 字段，以便在主题中显示 row/column 作为属性（序列不支持）的 id。

编辑必须手动分配 seq 的范围才能使该模型与 n > 4 一起使用。

以下是一个没有顺序的替代实现（对于那些不想为分配额外范围而烦恼的人）

one sig Board{
    cols: set Column,
    rows: set Row,
    q: set Queen
}
sig Row {
  id: disj Int
}{
   this in Board.rows
}

fact id{
    all r:Row| (sub[r.id,1] in Row.id or r.id=1) and r.id>0
    all c:Column| (sub[c.id,1] in Column.id or c.id=1) and c.id>0
}

sig Column {
  id: disj Int
}{
  this in Board.cols
}
sig Queen{
    x:Column,
    y:Row
}
pred aligned[q1,q2:Queen]{
   q1.y=q2.y 
   or 
   q1.x=q2.x  
   or some a,b:Int{
       add[q1.x.id,a]= q2.x.id 
       add[q1.y.id,b]= q2.y.id
       a=b or a=sub[0,b]
    } 
}
pred Show {
   no disj q1,q2:Queen| aligned[q1,q2]
}
run Show for exactly 4 Row, exactly 4 Column, exactly 4 Queen

更好的 Alloy n 皇后模型？

Better Alloy model of n-queens?

alloy