2

What I'm really trying to do is to convert boolean expressions to integer linear programming constraints. I'm trying to first convert the expressions into a CNF (using pyeda) and then from the CNF form the constraints (since this is pretty straight forward). However, I'm having trouble to understand the abstract syntax tree which the .to_ast() function is outputting. As an example, when running .to_ast() on the expression (~C1 | ~P1 | ~O1) & (~C1 | ~P1 | ~O2) the output is

('and', ('or', ('lit', -1), ('lit', -2), ('lit', -3)), ('or', ('lit', -1), ('lit', -2), ('lit', -4)))

It is pretty obvious that the - is the negation and the integer is representing one of the variables. Does anyone know if there is a mapping from the integer to the variable? Long description for short question...

Rikard Olsson
  • 841
  • 1
  • 7
  • 28

1 Answers1

3

Yes, the integer you are looking at is the 'uniqid' attribute on literals.

>>> from pyeda.inter import *
>>> C1, P1, O1, O2 = map(exprvar, "C1 P1 O1 O2".split())
>>> f = (~C1 | ~P1 | ~O1) & (~C1 | ~P1 | ~O2)
>>> f.to_ast()
('and',
 ('or', ('or', ('lit', -1), ('lit', -2)), ('lit', -3)),
 ('or', ('or', ('lit', -1), ('lit', -2)), ('lit', -4)))
>>> C1.uniqid, P1.uniqid, O1.uniqid, O2.uniqid
(1, 2, 3, 4)
>>> (~C1).uniqid, (~P1).uniqid, (~O1).uniqid, (~O2).uniqid
(-1, -2, -3, -4)

You can access the internal mapping directly if you want, but it requires some special knowledge:

>>> from pyeda.boolalg.expr import _LITS
>>> _LITS
{1: C1, 2: P1, 3: O1, 4: O2, -1: ~C1, -2: ~P1, -3: ~O1, -4: ~O2}
Chris Drake
  • 353
  • 1
  • 7
  • would it make sense to give documented access to this mapping? In my case I am parsing an expression from a string so I don't have access to the variables since I haven't defined them. – Leevi L Jan 06 '21 at 11:28