How is lab 3 going to be marked?

[Diego Huang]

Hi,

I was wondering how the automarker is going to mark lab 3? Is it going to
expect a specific satisfiable vector? Or as long as the vector that's
output by our program satisfies the formula, the marker will mark it as
correct? I'm asking this because there are different orders in which we
can implement the deductions, and that will lead to different satisfiable
vectors...

Thanks,

Diego

[Alexander Smith]

Hi,

You are correct: a formula may have many different satisfying assignments.
If a formula is satisfiable, then your program should find *a* satisfying
assignment - any one is fine. The assignment your program returns will be
checked by running it through another program (like the reference solution
to lab 2). It is also possible to generate formulas that are not
satisfiable. ex3.cnf from lab2 is one example of such a formula. In this
case, obviously your program should not return an assignment; it should
say "UNSAT".

Alexander

Post by Diego Huang
Hi,
I was wondering how the automarker is going to mark lab 3? Is it going to
expect a specific satisfiable vector? Or as long as the vector that's
output by our program satisfies the formula, the marker will mark it as
correct? I'm asking this because there are different orders in which we
can implement the deductions, and that will lead to different satisfiable
vectors...
Thanks,
Diego

[Xing Katharine He]

Hi,

Is it acceptable if the program provides a satisfying assignment of the form:
001XX1
or should the program provide a specific assignment such as:
001001

Thanks!

Katharine Xing

Post by Alexander Smith
Hi,
You are correct: a formula may have many different satisfying assignments.
If a formula is satisfiable, then your program should find *a* satisfying
assignment - any one is fine. The assignment your program returns will be
checked by running it through another program (like the reference solution
to lab 2). It is also possible to generate formulas that are not
satisfiable. ex3.cnf from lab2 is one example of such a formula. In this
case, obviously your program should not return an assignment; it should
say "UNSAT".
Alexander

Post by Diego Huang
Hi,
I was wondering how the automarker is going to mark lab 3? Is it going to
expect a specific satisfiable vector? Or as long as the vector that's
output by our program satisfies the formula, the marker will mark it as
correct? I'm asking this because there are different orders in which we
can implement the deductions, and that will lead to different satisfiable
vectors...
Thanks,
Diego

[Alexander Smith]

That would be acceptable, since it is possible to find satisfying
assignments that do not assign a value to every variable. (In lab 2,
ex1.vec and ex2.vec are both examples of this.) However, the algorithm as
described in the handout will keep going until it has assigned a value to
every variable. This is easier to implement, since it means you don't
actually need to check to see if each clause is satisfied; you can just
keep going until you run out of variables. getNextVar() will return 0 to
tell you that there are no more unassigned variables. When this happens,
you can just return SAT.

Alexander

Post by Xing Katharine He
Hi,
001XX1
001001
Thanks!
Katharine Xing

Post by Alexander Smith
Hi,
You are correct: a formula may have many different satisfying assignments.
If a formula is satisfiable, then your program should find *a* satisfying
assignment - any one is fine. The assignment your program returns will be
checked by running it through another program (like the reference solution
to lab 2). It is also possible to generate formulas that are not
satisfiable. ex3.cnf from lab2 is one example of such a formula. In this
case, obviously your program should not return an assignment; it should
say "UNSAT".
Alexander

Post by Diego Huang
Hi,
I was wondering how the automarker is going to mark lab 3? Is it going to
expect a specific satisfiable vector? Or as long as the vector that's
output by our program satisfies the formula, the marker will mark it as
correct? I'm asking this because there are different orders in which we
can implement the deductions, and that will lead to different satisfiable
vectors...
Thanks,
Diego