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 NPcomplete problem in itself? Source: http://www.livejournal.com/community/algorithms/49222.html
