pure_literal addition to dpll2

[Chris Smith]

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

[Donaldson Tan]

are u referring to https://github.com/sympy/sympy/blob/master/sympy/logic/algorithms/dpll2.py ?

[Chris Smith]

yes. The `_pure_literal` there is just a d-onothing stub right now.

[Aaron Meurer]

On Mon, Jul 21, 2025 at 7:58 PM Chris Smith <smi...@gmail.com> wrote:
> +self.occurrence_count

This line is presumably a typo.

I'm not sure what your code is doing but perhaps it's related to the
fact that it causes _unit_prop() to be run multiple times in
_simplify() due to the way the while loop works.

Aaron Meurer

[Tilo RC]

> self._unit_prop_queue.append(abs(i))

The abs in this line is the problem.

Suppose i = -x where x is an atom (a boolean variable). So i is a negative literal. Also assume:
     self.occurrence_count[i] > 0 
     not self.occurrence_count[-i] = 0

Then

> self._unit_prop_queue.append(abs(i))

will schedule x to be set to true instead of doing the correct thing which would be scheduling it to be set to be false. 

Unrelated to the bug you encountered, to get the code working you would also need to update self.occurrence_count elsewhere in the code and deal with backtracking as currently occurance_count is only updated at initialization. 

[Chris Smith]

> +self.occurrence_count

This just clears out zero entries from the defaultdict.

Thanks for the pointers, @TiloRC.

/c