Majority Logic Representation and Satisfiability

Majority logic is a powerful generalization of common AND/OR logic. Original two-level and multi-level logic networks can use majority operators as primitive connective, in place of AND/ORs. In such a way, Boolean functions have novel means for compact representation and efficient manipulation. In this paper, we focus on two-level logic representation. We define a Majority Normal Form (MNF), as an alternative to traditional <em>Disjunctive Normal Form</em> (DNF) and <em>Conjunctive Normal Form</em> (CNF). After a brief investigation on the MNF expressive power, we study the problem of MNF-<em>SATisfiability</em> (MNF-SAT). We prove that MNF-SAT is NP-complete, as its CNF-SAT counterpart. However, we show practical restrictions on MNF formula whose satisfiability can be decided in polynomial time. We finally propose a simple algorithm to solve MNF- SAT, based on the intrinsic functionality of two-level majority logic. Although an automated MNF-SAT solver is still under construction, manual examples already demonstrate promising opportunities.

Presented at:
23rd International Workshop on Logic & Synthesis (IWLS), San Francisco, California, USA, May 30 - June 1, 2014

 Record created 2014-05-06, last modified 2018-03-17

Download fulltextPDF
External link:
Download fulltextURL
Rate this document:

Rate this document:
(Not yet reviewed)