Date: 03/04/05 (Algorithms)    Keywords: programming, web

I have been tinkering with Satisfiability solvers of late, but they all take input in CNF format and as my logic is not always of that form, I have a question: do you know of any algorithms to transform an arbitrary AND/OR tree into a set of CNF clauses? Can the result be shown to be minimal (cannot be done with fewer clauses nor fewer variables per clause), or is determining if a boolean logic relation between inputs and an output is minimal an NP-complete problem in itself?

On another note, it seems one can factorize in pseudopolynomial time by dynamic programming. Run the Sieve of Eratosthenes, but for each discovered prime, assign that prime to multiples of it that haven't been assigned to something else already. Then, starting at some number within the sieve, divide by the number assigned to it (which is one of its prime factors) and recurse until a prime is reached.
I don't know if this is common knowledge, though it seems simple in retrospect. It might be interesting as I didn't find any mention of it on the obvious web searches.

Source: http://www.livejournal.com/community/algorithms/49222.html