n皇后的更好的合金模型？

Question

下面是n皇后问题的合金模型（实际上，4皇后问题）。我想知道是否有更好的解决方案？注意在我的解决方案中，我使用next和prev反复消除对角线上的皇后;这似乎很klunky。

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板卡进行了优化，概念数量最少，实例生成的图形可视化效果良好，但带来了其缺点。 （不适用于不同数量的皇后/行/列，以及“klunky约束”）

我向您展示了我提出的替代解决方案，它有其不足之处（更多概念+约束中的量化可能会减慢向下的分析），但也它的优点：简洁和IMHO更可读的约束和灵活性（将用于任何数目的cols /行/王后工作）

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作为属性（不支持序列）。

编辑序列的范围将不得不手动分配该模型与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