APPLICATION FOR N -QUEEN PROBLEM Faculty of Mathematics and Computer Science West University of Timisoara, Romania Master program: Artificial… [610333]

TERM REWRIT E SYSTEM
APPLICATION FOR N -QUEEN PROBLEM
Faculty of Mathematics and Computer Science West University of Timisoara, Romania
Master program: Artificial Intelligence and Distributed Computing, year I.
Course: TERM REWRITING
Student: [anonimizat], rewrite engines for term rewriting
systems compute a normal set of terms that respect the rules from a specification . Trying to
overcome the problems of non -terminating and non -confluence sometime le ads to the need of
additional rewriting rules.
A Term Rewrite System (TSR) should be able to answer from confluence point of view to not
changing the outcome in case multiple rules match a term and one input could have more possible
outputs without it. Fr om termination point of view, a term rewriting system will always terminate
as normal form, for which no rewrite rule will match and when the normal form is unique it is
taken as the value of the initial expression.
TSR serve as general purpose nondetermi nistic programing possessing convenient mathematical
properties (Burstall , 1977) that serve as decision procedures for equational theories and
interpreting logic programing (Kowalski, 1974) .
The Term Rewrite Systems have an important role in abstract data type specifications,
implementation of functional programing languages and automated deduction. The aim of this
paper is to demonstrate the utility of term rewriting systems by proving termination utility.

DEFINITION OF TERMS

A Term Rewrite application have a se t of rewrite rules for transforming expression in other
expressions that match source expression and could replace it.
A term rewriting system R over a set of terms T is a finite set of rewrite rules, each of where l and
r are terms in T containing variables , such a rule may be applied to a term t in T if a sub term s of
t matches the left -hand side with some substitution of terms for the variables appearing .
Proof of properties of programs, in the case the proof is given to a computer this proof is fully
automated and is needed to give to the computer auxiliary lemmas, invariants.
Term rewriting is an attractive paradigm for program transformation. This programs must be
rewrite terminating, but mostly turn to be non -terminating or non -confluent and the most used
solution is to implement additional constructors to obtain a normalization for the rules According
to C.Elliott (2000), in functional programing this king of constructors (functions) are known by
smart constructors.

A terminatio n function takes a term as an argument and a rewriting system is terminating when
are no infinite derivations t1 ->t2->t3… A rewrite system is confluent when two terms can join if
they are or not result of the rewriting in one step from the same term.

TEST S AND COMPARATIONS
Program proposal using ADA to place N queens on 4 × 4 chess board so that no queen can capture
another one with a legal move.
Predicates:
– Queen( , )
• Constants:
– 1, 2, 3, 4 (column and row numbers)
• Column constraints:
– ∀i,j1,j2 Queen(i,j1) ∧ j1 ≠ j2 ⇒ ¬Queen(i,j2)
– ∀i ∃j Queen(i,j)

Constraints that no two queens should be:
▪ in the same row,
▪ same column,
▪ or in same diagonal.

Termination program p roperties: The post -condition need to establish that when the algorithm
returns a placement, it is legal, and if it returns an empty board, there is no solution. With N = 2,
the result should be empty and with N = 4, there need to be a legal placement.

➢ The board is a term
➢ Each move is a rewr ite
➢ The if multiple rules (constraints) need to have probability and select best move
➢ Multiple rewrites can take place
➢ Is needed to automate the process
➢ The final board is a term for which no rewrite rule will match

Exactly one queen in each row:
((x0⇒(¬x1∧¬x2∧¬x3∧¬x4))∧(¬x0⇒((x1⇒¬x2)∧(¬x1⇒x2)))) ∧
((x3⇒(¬x4∧¬x5))∧(¬x3⇒((x4⇒¬x5)∧(¬x4⇒x5)))) ∧
((x6⇒(¬x7∧¬x8))∧(¬x6⇒((x7⇒¬x8)∧(¬x7⇒x8)))) ∧
Exactly one queen in each column:
((x0⇒(¬x3∧¬x6))∧(¬x0⇒((x3⇒¬x6)∧(¬x3⇒x6)))) ∧
((x1⇒(¬x4∧¬x7))∧(¬x1⇒((x4⇒¬x7)∧(¬x4⇒x7)))) ∧
((x2⇒(¬x5∧¬x8))∧(¬x2⇒((x5⇒¬x8)∧(¬x5⇒x8)))) ∧
at most one queen in each diagonal:
((x0⇒(¬x4∧¬x8))∧(¬x0⇒(x4⇒¬x8))) ∧
(x1⇒¬x5) ∧
(x3⇒¬x7) ∧
((x2⇒(¬x4∧¬x6))∧(¬x2⇒(x4⇒¬x6))) ∧
(x1⇒¬x3) ∧
(x5⇒¬x7)

Search trees for all solutions to the 4 queens

ADA CODE for 4 x 4 queens’ chessboard
–GNAT 4.9.3

with Ada.Text_IO; use Ada.Text_IO;
procedure Queens is
Board : array (1..4, 1..4) of Boolean := (others
=> (others => False));
function Test (Row, Column : Integer) return
Boolean is
begin
for J in 1..Column – 1 loop
if ( Board (Row, J)
or else
(Row > J and then Board (Row – J,
Column – J))
or else
(Row + J <= 4 and then Board (Row +
J, Column – J))
) then
return False;
end if;
end loop;
return True;
end Test; function Fill (Column : Integer) return Boolean
is
begin
for Row in Board'Range (1) loop
if Test (Row, Column) then
Board (Row, Column) := True;
if Column = 4 or else Fill (Column + 1) then
return True;
end if;
Board (Row, Column) := False;
end if;
end loop;
return False;
end Fill;
begin
if not Fill (1) then
raise Program_Error;
end if;
for I in Board'Range (1) loop
Put (Integer'Image (9 – I));
for J in Board'Range (2) loop
if Board (I, J) then
Put ("|Q");
elsif (I + J) mod 2 = 1 then

Put ("|/");
else
Put ("| ");
end if;
end loop;
Put_Line ("|"); end loop;
Put_Line (" A B C D ");
end Queens;

OUTPUT

ADA CODE for 4 x 4 queens’ chessboard Term Rewriting terminating
–GNAT 4.9.3

with Ada.Text_IO; use Ada.Text_IO;
with Queens; use Queens;

procedure Main is
Success : Boolean;
Queens_2 : Board (1..2);
Queens_4 : Board (1 .. 4);

procedure Print_Board (B : Board) is
J : Index;
begin
J := 1;
while J <= B'Last loop
Put_Line ("|" & Index'Image (B(J)));
J := J + 1;
end loop;
end Print_Board;

begin
– 2-Queens
Search (Queens_2, 2, Success);
if (Success) then
Put_Line ("The legal placement in Queens _2
is : ");
Print_Board (Queens_2);
else
Put_Line ("No solution found in Queens_2");
end if;

New_Line;

– 4-Queens
Search (Queens_4, 4, Success);

if (Success) then
Put_Line ("The legal placement in Queens_4
is : " );
Print_Board (Queens_4);
else
Put_Line ("No solution found in Queens_4");
end if;
end Main;

package body Queens is

Compilation time: 0.38 sec, absolute service time: 0,55 sec

function Is_Consistent (B : Board; Pos : Index)
return Boolean is
Cons : Boolean;
begin
Cons := True;
for J in Index range 1 .. Pos – 1 loop
if not ((B(J) /= B(Pos))
and then (B(J) – B(Pos) /= Pos – J)
and then (B(Pos) – B(J) /= Pos – J))
then
Cons := False;
exit;
end if;
–# assert Cons = True and Pos = Pos% and
–# (for all K in Index range 1 .. J =>
–# (B(K) /= B(Pos) and
–# B(K) – B(Pos) /= Pos – K and
–# B(Pos) – B(K) /= Pos – K));
end loop;
return Cons;
end Is_Consistent;

procedure Search (B : out Board; N : in Size;
Success : out Boolean) is
Pos : Index := 1;
J : Extended_Index := 1;
begin
Success := False;
B := (others => 1);

loop
–# assert not Success and B'First = 1 and
B'Last = N and
–# Pos >= 1 and Pos <= N;

while J <= N loop
–# assert not Success and J <= N and
B'First = 1 and B'Last = N and
–# Pos >= 1 and Pos <= N;
B(Pos) := J;

if Is_Consistent (B, Pos) then
if Pos = N then
Success := True;
else
Pos : = Pos + 1;
J := 1;
end if;
exit;
end if;

J := J + 1;
end loop;

exit when Success;

– backtrack if no solution found
if J /= 1 then
while Pos > 1 and then B(Pos) = N loop
Pos := Pos – 1;
–# assert not Success and Pos >= 1 and
Pos < N;
end loop;
end if;

– no solution found, exit
exit when J /= 1 and then B(Pos) = N;

if J /= 1 then
J := B(Pos) + 1;
end if;
end loop;
end Search;

end Queens;

OUTPUT
No solution found in Queens_2
The legal placement in Queens_4 is :
| 2
| 4

| 1
| 3

CONCLUSION

The rewriting rules facilitate extension in computational domain. Solving constraint problems with
rewrite of rules will support that program run faster by eliminating all the overhead because of the
modular style. Rewrite rules can be used for general pu rpose computation where the result is an
nondeterministic programing with advantage incorporation of rules for equalities between terms.
The procedure is used as a theorem proving to search for solutions.
The difference between the two compared source code s demonstrated that using rewriting system
with termination is more efficient in terms of compilation time result.

Compilation time: 0.13 sec, absolute service time: 0,21 sec

REFERENCE S

Articles:
Burstall, R. M., And Darlington, J. (1977), A transformation system for developing recursive
programs .
EelcoVisser , A Survey of Rewriting Strategies in Program Transformation Systems, Electronic
Notes in Theoretical Computer Science Volume 57, December 2001 , Pages 109 -143
François Fages , A Generic Graphical User Interface for Constraint Logic Programming, 2004.
Nachum Dershowitz. Termination of rewriting. J. Symbolic Computation, 3(1&2):69{115,
February/April 1987. Corrigendum: 4, 3 (December 1987), 409{410 .
Pierre -Etienne Moreau, A choice -point library for backtrack programming, 54506 Vandœuvre –
l`es-Nancy Cedex, France

Web Sites:
http://why3.lri.fr/