Skip to content

Instantly share code, notes, and snippets.

@huyen-nguyen
Created November 20, 2020 05:11
Show Gist options
  • Save huyen-nguyen/f497216b6c2601d73fe3ca0f89f5c6d2 to your computer and use it in GitHub Desktop.
Save huyen-nguyen/f497216b6c2601d73fe3ca0f89f5c6d2 to your computer and use it in GitHub Desktop.
Generate DIMACS CNF formula for N-queens problem
// helper functions
// cnf formula exactly one of the variables in the chosen list to be true
function ext_one(list) {
let temp = ""
temp=temp+atl_one(list)
temp=temp+atm_one(list)
return temp
}
// cnf formula for atleast one of the variables in the chosen list to be true
function atl_one(list) {
let temp=""
list.forEach(item => {
temp = temp +" " + item
})
temp=temp+" 0\n"
console.log("at least, ", temp)
return temp
}
// cnf formula for atmost one of the variables in the chosen list to be true
function atm_one(list) {
let temp=""
list.forEach(function (x) {
list.slice(list.indexOf(x) + 1).forEach(y => {
temp = temp +" -"+x+" -"+y+" 0\n"
})
})
return temp
}
// function to map position (r,c) 0 <= r,c < N, in an NxN grid to the integer
// position when the grid is stored linearly by rows.
function varmap(r,c,N) {
return r*N+c+1
}
// range
function range(start, stop, step) {
if (typeof stop == 'undefined') {
// one param defined
stop = start;
start = 0;
}
if (typeof step == 'undefined') {
step = 1;
}
if ((step > 0 && start >= stop) || (step < 0 && start <= stop)) {
return [];
}
var result = [];
for (var i = start; step > 0 ? i < stop : i > stop; i += step) {
result.push(i);
}
return result;
}
/**
* @return {string}
*/
function sat(N){
// Start Solver: Comments
let output="c SAT Expression for N="+N+((N === 1)? " queen\n": " queens\n")
let size = N*N
output = output + "c Chess board has "+size+((N === 1)? " position\n": " positions\n")
// Exactly 1 queen per row
let tempG = ""
range(0,N).forEach(row => {
let A=[]
range(0,N).forEach(column => {
let position = varmap(row,column,N)
A.push(position)
})
tempG = tempG+ext_one(A)
})
// Exactly 1 queen per column
range(0,N).forEach(column => {
let A=[]
range(0,N).forEach(row => {
let position = varmap(row,column,N)
A.push(position)
})
tempG = tempG+ext_one(A)
})
// Atmost 1 queen per negative diagonal from left
range(N-1,-1,-1).forEach(row => {
let A=[]
range(0,N-row).forEach(x => {
A.push(varmap(row+x,x,N))
})
tempG=tempG+atm_one(A)
})
// Atmost 1 queen per negative diagonal from top
range(1,N).forEach(column => {
let A=[]
range(0,N-column).forEach(x => {
A.push(varmap(x,column+x,N))
})
tempG=tempG+atm_one(A)
})
// Atmost 1 queen per positive diagonal from right
range(N-1,-1,-1).forEach(row => {
let A=[]
range(0,N-row).forEach(x => {
A.push(varmap(row+x,N-1-x,N))
})
tempG=tempG+atm_one(A)
})
// Atmost 1 queen per positive diagonal from top
range(N-2,-1,-1).forEach(column => {
let A=[]
range(0,column+1).forEach(x => {
A.push(varmap(x,column-x,N))
})
tempG=tempG+atm_one(A)
})
output = output + 'p cnf ' + (N*N) + ' ' + (tempG.split('\n').length - 1) + '\n' + tempG.trim()
return output
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment