Opened 10 years ago

Last modified 7 years ago

#13558 new enhancement

Add Philipp Jovanovic ANF to CNF converter

Reported by: malb Owned by: jason
Priority: major Milestone: sage-duplicate/invalid/wontfix
Component: misc Keywords: SAT
Cc: Merged in:
Authors: Reviewers: Martin Albrecht
Report Upstream: N/A Work issues:
Branch: Commit:
Dependencies: Stopgaps:

Status badges

Description (last modified by 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

Change History (15)

comment:1 Changed 10 years ago by malb

  • Component changed from PLEASE CHANGE to misc
  • Owner changed from tbd to jason

comment:2 Changed 10 years ago by malb

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

comment:3 Changed 10 years ago by boothby

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".

comment:4 follow-up: Changed 10 years ago by cosh

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?

comment:5 in reply to: ↑ 4 ; follow-up: Changed 10 years ago by malb

Replying to cosh:

  • 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.

comment:6 in reply to: ↑ 5 Changed 10 years ago by cosh

Replying to malb:

Replying to cosh :

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 ...

comment:7 Changed 10 years ago by nthiery

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!

comment:8 Changed 10 years ago by cosh

  • Description modified (diff)

comment:9 Changed 10 years ago by malb

  • Description modified (diff)

comment:10 Changed 10 years ago by cosh

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...

comment:11 Changed 9 years ago by jdemeyer

  • Milestone changed from sage-5.11 to sage-5.12

comment:12 Changed 8 years ago by vbraun_spam

  • Milestone changed from sage-6.1 to sage-6.2

comment:13 Changed 8 years ago by vbraun_spam

  • Milestone changed from sage-6.2 to sage-6.3

comment:14 Changed 8 years ago by vbraun_spam

  • Milestone changed from sage-6.3 to sage-6.4

comment:15 Changed 7 years ago by malb

  • Milestone changed from sage-6.4 to sage-duplicate/invalid/wontfix
  • Reviewers set to Martin Albrecht

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

Note: See TracTickets for help on using tickets.