StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>The most well-known algorithm for Boolean formula minimisation is the Quine-McCluskey algorithm, which yields the smallest DNF formula, but is computational expensive (necessarily, since the problem is outside PTIME, cf. <a href="http://www.cs.caltech.edu/~umans/papers/BU07.pdf" rel="nofollow noreferrer">The complexity of Boolean formula minimization, 2007</a>). There's <a href="http://archive.is/z73yL" rel="nofollow noreferrer">a literate Java implementation</a>; the basic concept is crucial to Prolog, so if you have any experience with Prolog, the idea should come easily enough.</p> <p><strong>Postscript</strong> There's an IEEE-paywalled article, <a href="http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=485236" rel="nofollow noreferrer">Extending Quine-McCluskey for exclusive-or logic synthesis</a>, abstract:</p> <blockquote> <p>Various forms of Boolean minimization have been used within electronic engineering degrees as a key part of the syllabus. Typically, Karnaugh maps and Quine-McCluskey methods are the principal exhaustive search techniques for digital minimization at the undergraduate level as they are easy to use and simple to understand. Despite the popularity of these methods, they are not well suited to typical digital circuits. Simple examples of such circuits are parity, adders, gray code generators, and so on. The common factor among these is the Exclusive-Or logic gate. This problem is exacerbated by the increasing importance of Exclusive-Or in modern design. This paper proposes an extension to the Quine-McCluskey method which successfully incorporates Exclusive-Or gates within the minimization process. A number of examples are given to demonstrate the effectiveness of this approach. This technique is easy to master as it can be considered to be an extension to the Quine-McCluskey method.</p> </blockquote> <p>I had been thinking of how to extend the method before I looked this up: you should be able to synthesise applications of XOR by using an alternate version of resolution that corresponds to them. For example, for a disjunctive clause <code>F</code> in a CNF, which does not contain either of the atoms <code>A</code>, or <code>B</code>, from the clauses <code>F | A | ~B</code> and <code>F | ~A | B</code>, then you can replace them by <code>F | XOR(A,B)</code>.</p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload