Davis putnam algorithm for satisfiability...

[Cameron Simpson]

On 05Aug2014 07:03, varun7rs at gmail.com <varun7rs at 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 <cs at 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.