MajorSat: A SAT solver to majority logic

Abstract—A majority function can be represented as sum-ofproduct (SOP) form or product-of-sum (POS) form. However, a Boolean expression including majority functions could be more compact compared to SOP or POS forms. Hence, majority logic provides a new viewpoint for manipulating the Boolean logic. Recently, majority logic attracts more attentions than before and some synthesis algorithms and axiomatic system for majority logic have been proposed. On the other hand, solvers for satisfiability (SAT) problem have a tremendous progress in the past decades. The format of instances for the SAT solvers is the Conjunctive Normal Form (CNF). For the instances that are not expressed as CNF, we have to transform them into CNF before running the SAT-solving process. However, for the instances including majority functions, this transformation might be not scalable and time-consuming due to the exponential growth in the number of clauses in the resultant CNF. As a result, this paper presents a n...

• Type: Journal
• Year: 2016
• Where: ASPDAC
• Authors: Yu-Min Chou, Yung-Chih Chen, Chun-Yao Wang, Ching-Yi Huang
• Keywords: ASPDAC 2016, Hardware