Alexander Smith
2004-02-03 17:35:57 UTC
Hi everyone,
There has been an update to lab 2. Figure 1 has also been corrected. (The
literals are in the correct order now.) Two changes have been made to
section 3.4 of the handout. Related changes have been made to the comment
blocks at the tops of two functions in SAT.c.
If you don't want to re-download SAT.c because you've already started
working on it, you can bring your copy up-to-date by replacing the comment
blocks in front of clauseStatus() and checkAssignment() with the
following:
At the top of clauseStatus():
/*
* Determine whether the specified clause is SAT, UNSAT, or not yet determined.
* A clause is SAT if at least one literal is satisfied, or it is an empty
* clause. (An empty clause is one with no literals.)
* A clause is UNSAT if all of its literals are unsatisfied.
* Otherwise it is UNDETERMINED.
*/
At the top of checkAssignment():
/*
* Check the current assignment of variables in the boolean formula
* stored in 'solver'.
* The formula stored in 'solver' is SAT if all its clauses are SAT, or it
* is an empty formula (having no clauses).
* It is UNSAT if any one of its clauses is UNSAT.
* Otherwise it is UNDETERMINED.
*/
(These changes take into account the ambiguities pointed out by Diego
Huang in his recent post "Case of 0 clauses or variables?".)
Alexander
There has been an update to lab 2. Figure 1 has also been corrected. (The
literals are in the correct order now.) Two changes have been made to
section 3.4 of the handout. Related changes have been made to the comment
blocks at the tops of two functions in SAT.c.
If you don't want to re-download SAT.c because you've already started
working on it, you can bring your copy up-to-date by replacing the comment
blocks in front of clauseStatus() and checkAssignment() with the
following:
At the top of clauseStatus():
/*
* Determine whether the specified clause is SAT, UNSAT, or not yet determined.
* A clause is SAT if at least one literal is satisfied, or it is an empty
* clause. (An empty clause is one with no literals.)
* A clause is UNSAT if all of its literals are unsatisfied.
* Otherwise it is UNDETERMINED.
*/
At the top of checkAssignment():
/*
* Check the current assignment of variables in the boolean formula
* stored in 'solver'.
* The formula stored in 'solver' is SAT if all its clauses are SAT, or it
* is an empty formula (having no clauses).
* It is UNSAT if any one of its clauses is UNSAT.
* Otherwise it is UNDETERMINED.
*/
(These changes take into account the ambiguities pointed out by Diego
Huang in his recent post "Case of 0 clauses or variables?".)
Alexander