If Only Carl Friedrich Gauss had IntelliGen in 1850

18 Aug 2011 • 5 minute read

The N-queens issue is a challenging but standard puzzle when it comes to the world of constraint solving. It's a generalization of the 8-queens puzzle, whose description can be found in detail in Wikipedia (http://en.wikipedia.org/wiki/Eight_queens_puzzle.) The challenge is to place N queens on an NxN chessboard in such a way that no pair of queens can attack each other. For those unfamiliar with chess rules, this means that no two queens can ever be found in the same column, row or diagonal.

Many mathematicians, including the mighty Carl Friedrich Gauss, have tried, and failed, to find algorithms to solve this challenge. Even today we do not know if the problem can be solved by an efficient algorithm (This is a so-called NP-hard problem in the Theory of Computation)

The solutions of N-queens are rare and irregularly placed in the hyperspace of possible placements. For instance, the case of 8 queens has 92 non-symmetric solutions out of more than 4 billion possible placements. So, the ability of a solver to solve N-queens demonstrates the effectiveness of its search mechanisms.

The Specman IntelliGen solving engine is based on what's called a finite-domain solver. This has many advantages over other BDD or SAT-based solvers used by our competition. Without getting too deep into details, there are some inherent problems of the BDD/SAT technologies that cause BDD solvers to explode for even small values of N (resources max out at N>=10) and SAT solvers suffer from poor performance (10X slower than IntelliGen for N=40 and simply does not finish for N=100). In contrast, solving a 100 Queens problem takes only seconds in IntelliGen using the following simple nested for each constraint solution:

<'
#define N 20;
extend sys {
    rows[N] : list of uint[0..N-1];
    keep for each (item_i) using index (i) in rows {
       for each (item_j) using index (j) in rows { 
          i<j => (item_i != item_j and abs(item_j-item_i) != j-i);
        };
    };
    
    run() is also {
        for each (pos) in rows {
            for i from 0 to N-1 {
                if (i==pos) { outf(" Q"); }
                else        { outf(" ."); };
            };
            out("");
        };
    };
};
'>

What are we doing in the above example? We have chosen to model the problem with a list of N integers in the range [0..N-1]. Each element represents a row. Each value is a column position of a queen in that row. So, the constraints used are:

No queens reside in the same column
- keep i<j => item_i != item_j
No two queens are ever on the same diagonal. Here we use the abs() built in e method to grab the absolute value of the difference between the column position of each queen.
- keep i<j => abs(item_j-item_i) != j-i)
It is sufficient to constraint only the cases i<j; otherwise we would double the constraints.

The run() method is just the pretty-printing. We go over all cells of the chessboard and print "Q" if the cell is occupied and "." otherwise. Here is an example of the printout:

Starting the test ...

Running the test ...

. . . . . . . . . . . . Q . . . . . . .

. Q . . . . . . . . . . . . . . . . . .

. . . Q . . . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . . Q

. . . . . . . . . . . . . Q . . . . . .

. . . . . . . . . . Q . . . . . . . . .

Q . . . . . . . . . . . . . . . . . . .

. . . . . . . . . . . Q . . . . . . . .

. . . . . Q . . . . . . . . . . . . . .

. . . . . . . . . . . . . . . Q . . . .

. . . . . . Q . . . . . . . . . . . . .

. . . . . . . . . . . . . . . . . . Q .

. . . . . . . . . . . . . . Q . . . . .

. . . . . . . . Q . . . . . . . . . . .

. . . . . . . . . . . . . . . . . Q . .

. . . . Q . . . . . . . . . . . . . . .

. . . . . . . Q . . . . . . . . . . . .

. . . . . . . . . . . . . . . . Q . . .

. . Q . . . . . . . . . . . . . . . . .

. . . . . . . . . Q . . . . . . . . . .

No actual running requested.

Checking the test ...

Checking is complete - 0 DUT errors, 0 DUT warnings.

You might ask yourself, why is this important for verification? Well, the faster IntelliGen can solve a very challenging problem like N Queens, the faster it can solve the complex generation constraints of today's largest devices.

How fast is your constraint solving engine? Challenge your vendors' tools in this complex generation puzzle and post your results if you can.

Vitaly Lagoon

Vitaly Lagoon is an Architect working on the IntelliGen Generation Engine. Vitaly is a principal designer of IntelliGen's constraint solver and an expert on constraint solving techniques and tools. He is also a prolific researcher with more than 20 academic publications on constraint solving and program analysis in the leading international conferences and journals.