-
Title:
13ps-08 Reduced Satisfaction Solution
-
Description:
-
Let's take a look at the code.
-
Now the first thing we do is we set a variable called rules affable to be true.
-
And this is so that we know when we can continue applying to the given rules
-
and that way we know when we can simply be done with the function.
-
We also get a temporary assignment to all of the variables of none
-
since we haven't assigned that neither true or false values yet.
-
Now in this loop, well, we can still apply rules.
-
We first set rules affable to false and let's say that unless we come into a situation
-
where we might be able to apply the rules again,
-
we just assume that this is the last time we'll be able to do this.
-
We first deal with single occurrence variables,
-
so we set a counter to be zero for each of the variables here
-
and we'll also set the variable setting to none for each of the variables.
-
And then, for each of the clauses and each variable in each clause,
-
we set the absolute value of the variable and then we increment variable counter of that variable
-
by 1 since we've seen that variable now and we set this variable to 1
-
if it does greater than 0 or 0, otherwise.
-
Or we set it to 1 is 0 to represent true or false if it is positive or negative.
-
Now, we enumerate all of the variable counters with i and var,
-
and if var is not equal to 1 then we go ahead and just continue.
-
And if our temporary assignment is not none, that is it's already going to assign to something,
-
we also continue, otherwise, we fall through
-
and we set the contemporary assignment to the current setting available.
-
In here, we try to deal with single variable clauses.
-
Now, for each clause in the list of clauses, we first check that the length of the clause is not zero.
-
If the length of the clause is greater than 1, we go ahead and just continue to do it.
-
We don't need to check any further; otherwise, we set the variable
-
equal to the only element in the list in the clause
-
and we set a var to the absolute value of that variable.
-
Now if the temporary assignment of avar is not none,
-
if it's already assigned something, then if the temporary assignment of avar is not equal to 1,
-
if the variable is greater than 0 else 0, then we return 1, -1
-
and this is because that means that the variable cannot be satisfied.
-
This clause and that cannot be satisfied, and if not, then we go ahead and fall through
-
and we set the temporary assignment of this variable to 1
-
if the variable is greater than 0 and else 0.
-
Now, we need to go ahead and clean up all of these clauses.
-
In order to do this, we are going to accumulate all of the current clauses into a new list of clauses,
-
so that we can remove the ones that we don't need to worry about anymore.
-
And we enumerate all the current clauses and we also enumerate all the variables in each clause
-
and we set the assignment equal to the temporary assignment for each of these variables.
-
If the assignment is none, then we go ahead and append that variable to the new clause
-
because it's still haven't determined what it should be, otherwise,
-
we said that, well, we might be able to continue applying rules here
-
because we're about to remove some clauses.
-
Now, if the current variable is assigned true, 1 and the variable is greater than 0
-
or the assignment is false, 0 and the variable is less than 0,
-
that is it's negated then we can go ahead and remove the entire clause.
-
So we set this new clause equal to none and we continue on.
-
Otherwise, well, then we just have to remove the variable and we pass through.
-
Now, if clause could not be satisfied then if the new clause is the empty set
-
then we go ahead and return 1, -1 to indicate they cannot be satisfied.
-
Now if the clause instead is greater than 0 then we go ahead
-
and append this clause to the new list of clauses and at the end of this double for loop,
-
we set the current list of clauses to the new list of clauses and if we have set rules applicable to true,
-
then we go ahead and loop that through until that is not true.
-
At the end of all this, we go ahead and return the list of clauses and that's it.
