English subtitles

← 13ps-08 Reduced Satisfaction Solution

Get Embed Code
1 Language

Showing Revision 1 created 10/24/2012 by Amara Bot.

  1. Let's take a look at the code.
  2. Now the first thing we do is we set a variable called rules affable to be true.
  3. And this is so that we know when we can continue applying to the given rules
  4. and that way we know when we can simply be done with the function.
  5. We also get a temporary assignment to all of the variables of none
  6. since we haven't assigned that neither true or false values yet.
  7. Now in this loop, well, we can still apply rules.
  8. We first set rules affable to false and let's say that unless we come into a situation
  9. where we might be able to apply the rules again,
  10. we just assume that this is the last time we'll be able to do this.
  11. We first deal with single occurrence variables,
  12. so we set a counter to be zero for each of the variables here
  13. and we'll also set the variable setting to none for each of the variables.
  14. And then, for each of the clauses and each variable in each clause,
  15. we set the absolute value of the variable and then we increment variable counter of that variable
  16. by 1 since we've seen that variable now and we set this variable to 1
  17. if it does greater than 0 or 0, otherwise.
  18. Or we set it to 1 is 0 to represent true or false if it is positive or negative.
  19. Now, we enumerate all of the variable counters with i and var,
  20. and if var is not equal to 1 then we go ahead and just continue.
  21. And if our temporary assignment is not none, that is it's already going to assign to something,
  22. we also continue, otherwise, we fall through
  23. and we set the contemporary assignment to the current setting available.
  24. In here, we try to deal with single variable clauses.
  25. Now, for each clause in the list of clauses, we first check that the length of the clause is not zero.
  26. If the length of the clause is greater than 1, we go ahead and just continue to do it.
  27. We don't need to check any further; otherwise, we set the variable
  28. equal to the only element in the list in the clause
  29. and we set a var to the absolute value of that variable.
  30. Now if the temporary assignment of avar is not none,
  31. if it's already assigned something, then if the temporary assignment of avar is not equal to 1,
  32. if the variable is greater than 0 else 0, then we return 1, -1
  33. and this is because that means that the variable cannot be satisfied.
  34. This clause and that cannot be satisfied, and if not, then we go ahead and fall through
  35. and we set the temporary assignment of this variable to 1
  36. if the variable is greater than 0 and else 0.
  37. Now, we need to go ahead and clean up all of these clauses.
  38. In order to do this, we are going to accumulate all of the current clauses into a new list of clauses,
  39. so that we can remove the ones that we don't need to worry about anymore.
  40. And we enumerate all the current clauses and we also enumerate all the variables in each clause
  41. and we set the assignment equal to the temporary assignment for each of these variables.
  42. If the assignment is none, then we go ahead and append that variable to the new clause
  43. because it's still haven't determined what it should be, otherwise,
  44. we said that, well, we might be able to continue applying rules here
  45. because we're about to remove some clauses.
  46. Now, if the current variable is assigned true, 1 and the variable is greater than 0
  47. or the assignment is false, 0 and the variable is less than 0,
  48. that is it's negated then we can go ahead and remove the entire clause.
  49. So we set this new clause equal to none and we continue on.
  50. Otherwise, well, then we just have to remove the variable and we pass through.
  51. Now, if clause could not be satisfied then if the new clause is the empty set
  52. then we go ahead and return 1, -1 to indicate they cannot be satisfied.
  53. Now if the clause instead is greater than 0 then we go ahead
  54. and append this clause to the new list of clauses and at the end of this double for loop,
  55. we set the current list of clauses to the new list of clauses and if we have set rules applicable to true,
  56. then we go ahead and loop that through until that is not true.
  57. At the end of all this, we go ahead and return the list of clauses and that's it.