How to convert boolean polynomials to DIMACS format?

edit

I have very large number of clauses in a list. Is there any other method to add clauses other than repeating the following for each clause? e.clauses_sparse(a*b + a + 1)

From the documentation of CNFEncoder it seems that you can do e(F) where F is an iterable (e.g. list) of boolean polynomials.

This gives a DIMACS file but how can we figure out boolean variables corresponding to the variable numbers in the DIMACS format?

From the same documentation: see e.phi.