Q. I think my program is correct but it takes minutes to solve N-queens for N=8 and hours when N=10. I am sure that your automatic testing will not wait hours for my solution. What should I do?

A. We will test your sat solver on a variety of small and large CNF formula. We will test your N-Queens CNF on our sat solver which works fast enough to check its correctness also for larger N. We expect your sat solver to manage to solve the CNF for N-queens for at least N=8 in less than 10 seconds. We might decide to test it even for larger values of N.

The bonus tests will be on much larger values of N.

The forum is full of technical answers. But try to think of it this way:

• You have a set of propositional variables (represented by an array of integers). Lets call these variables v1,v2,…,vn. Each variable can be either "true" or "false".

• Your task7 is to express as a CNF formula the statement: at least one of v1,v2,…,vn is true. Try to think which formula (in CNF) makes this statement.

• Your task8 is to express a CNF formula which says that not more than 1 of the variables v1,v2,…,vn is true. Or in other words that it is not possible for two of them to be true. It means that for every two variables and at least one of them is not true. This is a conjunction on all pairs (i != j) where for each pair we say that either is false or is false (otherwise there would be two variables true).

• Note that if phi1 expresses that at least one of the variables v1,…,vn is true and phi2 expresses that at most one of them is true then the conjunction of phi1 and phi2 expresses that "exactly one of the variables is true". Use this idea to solve task 9.

No. Please use only one return at the end of a function.

You did not mention which function (task) you are inquiring about, but phi should not be changed in any task. Notice that a new "phi", let's call it phi2, that is also an array of arrays, can hold references to the clauses in the original phi, in a different order. Thus you did not change phi, and did not copy it all.

For example:

As you can see above, if you want to change the order of the clauses in phi, you do not need to copy all the literals in the clause, you can just copy the reference to the clause.

In tasks 7 and 8 you should return a legal CNF, according to the task description.
Yes, task 7 is quite simple, and task 8 is slightly more complicated. The "Coaching" part of the tasks is very detailed, and the example is pretty clear, so it should not be very difficult to understand and implement them.
Giving another example is giving away the whole task. You should understand from the task description.

Generally, we ask you not to use Java elements not taught in classes or practical sessions. In some cases, we may not take points off for doing this (like if you use "i++" instead of "i=i+1" command).
It is very good you are reading through Java's API, and it is ok to use some functions we did not teach, like ; but you are not allowed to use the functions that create/copy arrays, or use Objects like Array or Vector.

Q:

Can we assume that a variable will not appear more than once in any single clause? Can we assume that a variable and it's opposite (e.g. x1 and ~x1) will not appear in the same clause?

A:

We will not test your program for examples that have twice x1 or both x1 and -x1. So if you like to make this assumption, you may.

Q:

in Task 4 (substitute): can we assume that there are no empty clauses? if not, what does the function return in that case?

A:

No, you may not make this assumption. You are free to return any CNF representing the formula

Q:

in Task 4: what does it return in case phi itself is empty?

A:

Think about it.

Yes.

No.