I tried adding
def _pure_literal(self):
#return False
added = False
for i in self.occurrence_count:
if self.occurrence_count[i] and not self.occurrence_count[-i]:
self._unit_prop_queue.append(abs(i))
self.occurrence_count[i] -= 1
added = True
if added: # remove any 0 entries
+self.occurrence_count
return added
to dpll2, but this truncates solutions instead of returning all expected
solutions. Does anyone see the problem with what I have added?
Here is a signed int cnf that should have 36 solutions but with the code
above, only two solutions are returned.
[{3, -4, 5}, {-4, -3, 6}, {-6, -5, -2}, {-6, -5, -1}]
/c
--
You received this message because you are subscribed to the Google Groups
"sympy" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/sympy/14b38743-c58c-4d62-9982-ff50175450c4n%40googlegroups.com.
