n皇后的更好合金模型？

Question

下面是 n-queens 问题（实际上是 4-queens 问题）的合金模型。我想知道是否有更好的解决方案？请注意，在我的解决方案中，我反复使用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 个皇后/4x4 板进行了优化，概念数量最少，生成的实例的默认图形可视化很好，但也有其缺点。 （不适用于不同数量的皇后/行/列，以及“笨拙的约束”）

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

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 字段是为了在主题中将行/列的 id 显示为属性（不支持序列）。

edit必须手动分配 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