Incorrect unsat for nqueens implementation
FOLASP returns unsat for the below nqueens implementation, whereas IDP3 is able to (correctly) find two models.
// Alternate version of nqueens
// Author: Simon Vandevelde (s.vandevelde@kuleuven.be)
vocabulary V {
type Val isa int
queen(Val): Val
// Basically: queen (row -> col)
}
structure S: V{
Val = {1..4}
}
theory T:V{
// Column constraint
!v1[Val]: !v2[Val]: v1 < v2 => queen(v1) ~= queen(v2).
// Diagonal constraints
!v1[Val]: !v2[Val]: queen(v1) + v2 ~= queen(v1+v2).
!v1[Val]: !v2[Val]: queen(v1) - v2 ~= queen(v1-v2).
!v1[Val]: !v2[Val]: queen(v1) + v2 ~= queen(v1-v2).
!v1[Val]: !v2[Val]: queen(v1) - v2 ~= queen(v1+v2).
}
procedure main() {
stdoptions.nbmodels = 10
printmodels(modelexpand(T, S))
}