Add Philipp Jovanovic ANF to CNF converter

[malb]

The converter is available here

https://github.com/Daeinar/anf2cnf-sage/blob/master/anf2cnf_sage.py

we should consider it for inclusion as it is more flexible than what we have now.

ANF
Algebraic Normal Form = Boolean polynomials = Square free polynomials over GF(2)

CNF
Conjunctive Normal Form = ANDs of OR clauses = form SAT-solvers understand

Component: misc

Keywords: SAT

Reviewer: Martin Albrecht

Issue created by migration from https://trac.sagemath.org/ticket/13558

[malb]

comment:2

The code is not ready for inclusion in Sage yet:

• there are no doctests
• it seems many local attributes are not marked local (self.one vs. self._one ), note that the current converter has a similar issue though
• phi is a function in this converter, but an attribute in the one currently included in Sage. Also, phi returns a reference to an internal mutable variable, instead of a copy

[boothby]

comment:3

The conversion strategies are poorly documented. At least one docstring should describe all of the strategies, and all of the methods which accept a strategy as an argument should provide the list of strategies and a reference to the docstring that describes them.

Additionally, I'm concerned that c_lin_cnf doesn't do anything for polynomials with length > 6. This doesn't currently seem to cause any bugs, but it might in the future. I'd rather see a generic implementation, or at the very least, raise ValueError, "input polynomials must have length <= 6".

[daeinar]

comment:4

Made some modifications to the code:

• Every function now has at least one doctest
• phi is now a @property
• marked self.one and self.zero as local (although self.zero could be deleted completely as it is never used) 

What I want to do next is adding some error checking mechanisms for user parameters and re-implementing the c_lin_cnf function in a more generic way. Anything else that I forgot?

[malb]

comment:5

Replying to @daeinar:

• Every function now has at least one doctest

Note that you misformated the doctest blocks: There's a :: after the preceding line (e.g. EXAMPLE::) which starts a code block. Also, there's supposed to be an empty line between the EXAMPLE:: and the first line of the code block. Again, this is part of the markup which starts a code block.

• phi is now a @property
• marked self.one and self.zero as local (although self.zero could be deleted completely as it is never used) 

Lets remove it then :)

What I want to do next is adding some error checking mechanisms for user parameters and re-implementing the c_lin_cnf function in a more generic way. Anything else that I forgot?

As far as I can see, no.

[daeinar]

comment:6

Replying to @malb:

Replying to @daeinar :

What I want to do next is adding some error checking mechanisms for user parameters and re-implementing the c_lin_cnf function in a more generic way. Anything else that I forgot?

As far as I can see, no.

Something that I think would be nice to have is some kind of mechanism which automatically selects (per polynomial?!) the "best suited" conversion strategy, as by now the user has to specify how all the polynomials get converted. But first one would have to find out what "best" means in this case before anything in that direction could be done. And even then I guess we would get very fast into NP complete areas. So a heuristic would be fine, too ...

[nthiery]

comment:7

Hi!

Please add in the doc and ticket description what ANF and CNF mean; that will save some time for the non experts, and will help find them through searches.

Thanks!

[daeinar]

comment:10

Today I've added the generic implementation for c_lin_cnf using some combinatorics. By now I've restricted the cutting_number to range(3,8) (see line 58). I don't think greater cutting_numbers are really that useful as the number of clauses grows exponentially. Nevertheless, if required, this restriction can be easily removed. Well now only some further error checking is missing...

[malb]

comment:15

I think it was decided to drop it (I talked to Philipp ages ago)

[malb]

Reviewer: Martin Albrecht