On 05Aug2014 07:03, varun...@gmail.com <varun...@gmail.com> wrote:
Thank you Cameron. Your post was very helpful. If you don't mind I'd like to
ask you the purpose of the final list in the very beginning of the code. It is
being updated and then checked for the presence of a literal. If a literal is
found it returns not equivalent. Could you brief me the use of a final list?
Not entirely, no. The python code is not very good, so the subtleties of the
algorithm are harder to see on inspection. We can talk about those issues later
if you like.
It looks to me as though this is a truncated version of the full algorithm. It
is currently written to abort the whole program if it decides that the cnf is
not satisfiable. Maybe.
In the (I am guessing hacked) code in your email, any single element sub-cnf
has its components appended to the final_list and then the list is scanned for
nonempty items; if one is found the whole program aborts. Otherwise the list
itself is returned (and universally ignored, which is why I think this code is
modified from a more complete original).
I think in the original the final_list is supposed to be a list of things to
examine later, possibly a list of subexpressions not yet determined to be
satisfiable. In this code it is never examined and you could possibly get away
with a direct examination of cnf[0][0] at that point, ignoring final_list. The
only reason I have any uncertainty is that the cnf trees get modified by the
del_sat() function, and so I'm not sure that the stuff put on final_list is
unchanged later.
So the short answer is: final_list is almost unused in this version of the code
and could possibly be removed, but the code is sufficiently uncommented and
clearly not the original algorithm, and the cnf structured modified in place,
that I am not entirely sure.
It is further complicated by the fact that this is not just the davis-putnam
algorithm on its own, it is that algorithm being used (I think) to compare two
boolean logic circuits for equivalence, possibly by assembling a cnf
representing circuit1 xor circuit2: if they are equivalent then I would expect
that to be not satisfiable but I have not thought it through completely.
You'd better hope those two circuits have no loops; I would not expect the
algorithm to be sufficient in the face of a loop.
Cheers,
Cameron Simpson <c...@zip.com.au>
If I had thought about it, I wouldn't have done the experiment.
The literature was full of examples that said you can't do this.
--Spencer Silver on the work that led to the unique adhesives
for 3-M "Post-It" Notepads.
--
https://mail.python.org/mailman/listinfo/python-list
