feat: finish A&B&C
This commit is contained in:
parent
c0b878e8ef
commit
5433ee3959
30
A/queens.P
Normal file
30
A/queens.P
Normal file
|
@ -0,0 +1,30 @@
|
|||
legal_queens(N, Row, []) :- N =:= Row - 1.
|
||||
legal_queens(N, Row1, [(Row1, Col1)|Queens]) :-
|
||||
Row1 < N + 1,
|
||||
Row2 is Row1 + 1,
|
||||
legal_queens(N, Row2, Queens),
|
||||
between(1,N,Col1),
|
||||
no_attacks((Row1, Col1), Queens).
|
||||
|
||||
no_attacks(_, []).
|
||||
no_attacks((Row1, Col1), [(Row2, Col2)|OtherQueens]) :-
|
||||
Row1 \= Row2,
|
||||
Col1 \= Col2,
|
||||
abs(Row1 - Row2) =\= abs(Col1 - Col2),
|
||||
no_attacks((Row1, Col1), OtherQueens).
|
||||
|
||||
n_queens(N, Solution) :-
|
||||
legal_queens(N, 1, Solution).
|
||||
|
||||
one_queens(N, Solution) :-
|
||||
legal_queens(N, 1, Solution), !.
|
||||
|
||||
printNQueen(N) :- n_queens(N, Solution), write(Solution), write('\n'), fail.
|
||||
printNQueen(_).
|
||||
|
||||
printOneQueen(N) :- one_queens(N, Solution), write(Solution), write('\n'), fail.
|
||||
printOneQueen(_).
|
||||
|
||||
timeNQueen(N) :- cputime(X), printNQueen(N), cputime(Y), T is Y-X, write(T).
|
||||
|
||||
timeOneQueen(N) :- cputime(X), printOneQueen(N), cputime(Y), T is Y-X, write(T).
|
|
@ -1,5 +0,0 @@
|
|||
import random
|
||||
for i in range(10000):
|
||||
j = random.randint(1,1000)
|
||||
k = random.randint(1,1000)
|
||||
print("edge(", j, ",", k, ").")
|
12
A/reach.P
12
A/reach.P
|
@ -1,13 +1,5 @@
|
|||
source(3).
|
||||
edge(0,1).
|
||||
edge(1,2).
|
||||
edge(1,5).
|
||||
edge(2,5).
|
||||
edge(3,5).
|
||||
edge(3,5).
|
||||
|
||||
%input :- [reachin1000]. % one way of reading input facts
|
||||
%:- include(reachin1000). % 2nd way of reading input facts
|
||||
:- include(reachin1000). % 2nd way of reading input facts
|
||||
|
||||
reach(X) :- source(X).
|
||||
reach(Y) :- reach(X), edge(X,Y).
|
||||
|
@ -20,3 +12,5 @@ printReach.
|
|||
%timeReach :- cputime(X), input, printReach, cputime(Y), T is Y-X, write(T).
|
||||
%timeReach :- input, cputime(X), printReach, cputime(Y), T is Y-X, write(T).
|
||||
timeReach :- cputime(X), printReach, cputime(Y), T is Y-X, write(T).
|
||||
|
||||
source(3).
|
||||
|
|
8
B/nqueens.lp
Normal file
8
B/nqueens.lp
Normal file
|
@ -0,0 +1,8 @@
|
|||
#const n = 8.
|
||||
|
||||
% n-Queens encoding
|
||||
|
||||
{ q(I,1..n) } == 1 :- I = 1..n.
|
||||
{ q(1..n,J) } == 1 :- J = 1..n.
|
||||
:- { q(D-J,J) } >= 2, D = 2..2*n.
|
||||
:- { q(D+J,J) } >= 2, D = 1-n..n-1.
|
5
B/reach.lp
Normal file
5
B/reach.lp
Normal file
|
@ -0,0 +1,5 @@
|
|||
#include "reachin1000".
|
||||
|
||||
source(3).
|
||||
reach(Y) :- edge(X,Y), reach(X).
|
||||
reach(X) :- source(X).
|
53
C/nqueens.idp
Normal file
53
C/nqueens.idp
Normal file
|
@ -0,0 +1,53 @@
|
|||
vocabulary V {
|
||||
type index isa int
|
||||
queen(index, index)
|
||||
n : index
|
||||
type diag isa int
|
||||
diag1(index, index) : diag
|
||||
diag2(index, index) : diag
|
||||
type dist isa int
|
||||
k: dist
|
||||
}
|
||||
|
||||
structure S : V {
|
||||
index = {1..4}
|
||||
diag = {1..7}
|
||||
n = 4
|
||||
k = 2
|
||||
}
|
||||
|
||||
theory T : V {
|
||||
{ diag1(x, y) = x - y + n. }
|
||||
{ diag2(x, y) = x + y - 1. }
|
||||
!x : ?=1y : queen(x, y). //(1)
|
||||
!y : ?=1x : queen(x, y). //(2)
|
||||
!d : #{x y : queen(x, y) & diag1(x, y) = d} < 2. //(3)
|
||||
!d : #{x y : queen(x, y) & diag2(x, y) = d} < 2. //(4)
|
||||
~? x1 y1 x2 y2: queen(x1, y1) & queen(x2, y2) & ~x1 = x2 & abs(x1-x2) + abs(y1-y2) =< k.
|
||||
//~? x1 y1 x2 y2: queen(x1, y1) & queen(x2, y2) & abs(x1-y1) = 3.
|
||||
}
|
||||
|
||||
procedure main() {
|
||||
/* Important: the option xsb is not present in every installation, in order to obtain
|
||||
* efficient definition evaluation with XSB, you should compile IDP yourself
|
||||
* (as XSB cannot be distributed with dynamically linked binaries
|
||||
*/
|
||||
stdoptions.xsb=true // use XSB to calculate definitions that can be
|
||||
// calculated in advance
|
||||
diags = calculatedefinitions(T,S) // calculate the definitions for symbols diag1 and diag2
|
||||
// The resulting variable (diags) contains a single structure
|
||||
// in which the defined symbols are two-valued
|
||||
print("Definitions calculated:\n"..tostring(diags))
|
||||
|
||||
stdoptions.nbmodels=0 // search for all models
|
||||
solutions = modelexpand(T,diags) // solutions is now a (Lua) table with all models
|
||||
// Note that instead of diags, we could also do modelexpand on S,
|
||||
// since the standard modelexpand workflow contains a call to
|
||||
// calculatedefinitions
|
||||
print(#solutions.." models found") // "#" retrieves table size, .. is the lua concatenation
|
||||
for i,sol in ipairs(solutions) do // A for-loop to iterate over all solutions.
|
||||
print("model "..i..":") // ipairs is a builtin Lua procedure which allows you
|
||||
// to loop over the index and table elements of a table
|
||||
print(sol)
|
||||
end
|
||||
}
|
5
randomgen.py
Normal file
5
randomgen.py
Normal file
|
@ -0,0 +1,5 @@
|
|||
import random
|
||||
for i in range(100000):
|
||||
j = random.randint(1,10000)
|
||||
k = random.randint(1,10000)
|
||||
print("edge(", j, ",", k, ").")
|
50000
reachin1000
Normal file
50000
reachin1000
Normal file
File diff suppressed because it is too large
Load Diff
Loading…
Reference in New Issue
Block a user