Alexander Smith
2004-02-23 00:08:59 UTC
Hi everyone,
It looks like there's still some confusion about how the algorithm works.
I'll try to see if I can clear things up in this message. If you're still
confused after reading this message, then go to your lab session on Tues.
or Wed. In the last week before reading week, we ran special tutorials on
this assignment for the first hour or so of the labs, but attendance was
very low. If enough people show up and request it, we will re-run the
tutorials this week. See the TA in GB243 at the start of your lab session
- that's me on Tuesday, or Frank on Wednesday.
When you're reading through the lab handout, one thing to keep in mind is
that Figures 1-3 are separate from Figures 4 and 5. The latter two figures
are the ones you want to look at when you're going to implement the lab.
Figure 4 shows the decision tree for the DLL algorithm, which is what you
are going to implement. Figures 1-3 show a simplified SAT-solving
procedure *without* the two deduction rules. Those appear first to
introduce you to how the overall concept works before complicating matters
by adding heuristics.
In Figures 1-3, it is true that at each level, you will only make an
assignment to one variable. But that is NOT what you are implementing. You
have to implement the Unit Literal Rule and the Conflict Rule. This means
that there are now two places you might make an assignment. The first is
still in the solve() procedure - where you pick one unassigned variable,
and then arbitrarily assign a value to it. (This is shown with circle
nodes in Figure 4.) The second place an assignment might happen is in the
deduction procedure. These assignments come from applications of the Unit
Literal rule, and they all go into the *same* decision level.
Here is what assignStack would look like after Figure 4:
assignStack[0] -> NULL (empty list)
assignStack[1] -> x1=0
assignStack[2] -> x3=1 -> x2=1
assignStack[3] -> x4=0
The reason x3=1 appears before x2=1 is that we insert assignments at the
head of the list. x2=1 occurred first. Then, when deduce() encountered the
clause (x1 + x2' + x3), it applied the Unit Literal Rule resulting in the
assignment x3=1 (because the assignments x1=0 and x2=1 had been made
previously, causing the first two literals to become UNSAT.) At this
point, there were no more deductions to be made. So, in the next recursive
call, we picked the unassigned variable x4 and assigned it the value 0.
This did not result in any conflicts, and there were no more variables
left unassigned, so we would return SAT at this point.
assignStack[0] is an empty list in this case. This is going to happen
unless your formula has clauses with only one literal in them. If you do,
then the Unit Literal Rule automatically applies, so you will get
assignments happening from deductions right from the start. But if all of
the clauses in your formula have two or more variables, then the first
non-empty list in your assignment stack will be assignStack[1].
Follow through this example yourself to make sure you understand what is
going on. The above "picture" of assignStack shows what it looks like at
the end of the algorithm. While you're running the algorithm yourself, you
will have to step through a backtracking procedure: you will initially
assign x2=0 in level 2. This will lead to the deduced assignment x4=1, but
this in turn will lead to a conflict, so you'll have to backtrack. That
means undoing all the assignments in level 2. Since x2=0 caused the
problem, you'll instead try x2=1, and continue as shown above.
Alexander
It looks like there's still some confusion about how the algorithm works.
I'll try to see if I can clear things up in this message. If you're still
confused after reading this message, then go to your lab session on Tues.
or Wed. In the last week before reading week, we ran special tutorials on
this assignment for the first hour or so of the labs, but attendance was
very low. If enough people show up and request it, we will re-run the
tutorials this week. See the TA in GB243 at the start of your lab session
- that's me on Tuesday, or Frank on Wednesday.
When you're reading through the lab handout, one thing to keep in mind is
that Figures 1-3 are separate from Figures 4 and 5. The latter two figures
are the ones you want to look at when you're going to implement the lab.
Figure 4 shows the decision tree for the DLL algorithm, which is what you
are going to implement. Figures 1-3 show a simplified SAT-solving
procedure *without* the two deduction rules. Those appear first to
introduce you to how the overall concept works before complicating matters
by adding heuristics.
In Figures 1-3, it is true that at each level, you will only make an
assignment to one variable. But that is NOT what you are implementing. You
have to implement the Unit Literal Rule and the Conflict Rule. This means
that there are now two places you might make an assignment. The first is
still in the solve() procedure - where you pick one unassigned variable,
and then arbitrarily assign a value to it. (This is shown with circle
nodes in Figure 4.) The second place an assignment might happen is in the
deduction procedure. These assignments come from applications of the Unit
Literal rule, and they all go into the *same* decision level.
Here is what assignStack would look like after Figure 4:
assignStack[0] -> NULL (empty list)
assignStack[1] -> x1=0
assignStack[2] -> x3=1 -> x2=1
assignStack[3] -> x4=0
The reason x3=1 appears before x2=1 is that we insert assignments at the
head of the list. x2=1 occurred first. Then, when deduce() encountered the
clause (x1 + x2' + x3), it applied the Unit Literal Rule resulting in the
assignment x3=1 (because the assignments x1=0 and x2=1 had been made
previously, causing the first two literals to become UNSAT.) At this
point, there were no more deductions to be made. So, in the next recursive
call, we picked the unassigned variable x4 and assigned it the value 0.
This did not result in any conflicts, and there were no more variables
left unassigned, so we would return SAT at this point.
assignStack[0] is an empty list in this case. This is going to happen
unless your formula has clauses with only one literal in them. If you do,
then the Unit Literal Rule automatically applies, so you will get
assignments happening from deductions right from the start. But if all of
the clauses in your formula have two or more variables, then the first
non-empty list in your assignment stack will be assignStack[1].
Follow through this example yourself to make sure you understand what is
going on. The above "picture" of assignStack shows what it looks like at
the end of the algorithm. While you're running the algorithm yourself, you
will have to step through a backtracking procedure: you will initially
assign x2=0 in level 2. This will lead to the deduced assignment x4=1, but
this in turn will lead to a conflict, so you'll have to backtrack. That
means undoing all the assignments in level 2. Since x2=0 caused the
problem, you'll instead try x2=1, and continue as shown above.
Alexander