多數函數可以經由積項和式(sum-of-product) 或和項積式(product-of-sum)表示。然而，在布林表示式中引入多數函數(Majority function) 能夠使得函數表達上，相較於使用積項和式或和項積式更為簡潔。因此，多數邏輯對於在操作布林邏輯上提供了新的觀點。相較於從前，近期多數邏輯吸引了較多的注目，一些根據多數邏輯而產生的邏輯合成演算法以及公理系統已被提出。另一方面，可滿足性問題求解器(SAT solver) 在過去數十年間，在求解速度有很大的進展。對這些求解器而言，輸入的格式為合取範式(CNF)。對於不是使用合取範式來表達的實例，我們必須將其轉換成合取範式後再經由可滿足性問題求解器求解。然而，對於包含多數函數在內的實例，轉換成合取範式是非常耗時的，原因來自將多數函數展開成合取範式會導致呈指數成長的子句(clause) 數量。因此，這篇論文提出了新的可滿足性問題求解器|MajorSat，能夠直接處理含有多數函數在內的可滿足性問題實例，而一些用來加速MajorSat求解的技巧也一併被提出。除此之外，我們提出一種以多數函數形式呈現的特徵函數來表達多數邏輯閘的功能。實驗結果展現出MajorSat能夠有效率的解出包含多數函數的隨機實例，而這是如MiniSat或Lingeling這類運作在合取範式上的可滿足性問題求解器所做不到的。

A majority function can be represented as sum-of-product (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 new SAT solver, MajorSat, which is for solving a SAT instance containing majority functions without any transformation. Some techniques for speeding up the solver are also proposed. Besides, we also propose a transformation method that can generate the characteristic function of a majority logic gate. The experimental results show that the MajorSat solver can efficiently solve random instances containing majority functions that CNF SAT solvers, like MiniSat or Lingeling, cannot.

[1] L. Amar'u, P.-E. Gaillardon, and G. De. Micheli, "Majority Logic Representation and Satisfiability," in Proc. International Workshop on Logic & Synthesis,
2014.
[2] L. Amar'u, P.-E. Gaillardon, and G. De. Micheli, "Majority-Inverter Graph: A Novel Data-Structure and Algorithms for Efficient Logic Optimization," in Proc. Design Automation Conference, pp. 1-6, 2014.
[3] G. Audemard and L. Simon, "Predicting Learnt Clauses Quality in Modern SAT Solvers," in Proc. International Joint Conference on Artificial Intelligence, pp. 399-404, 2009.
[4] A. Biere, "Lingeling, Plingeling and Treengeling Entering the SAT Competition 2013," SAT Competition, 2013.
[5] M. Davis and H. Putnam, "A Computing Procedure for Quantification Theory," Journal of the ACM, 7:201-215, July 1960.
[6] N. Een and N. Sorensson, "An Extensible SAT-Solver," in Proc. International Conference on Theory and Applications of Satisfiability Testing, pp 502-518,
2003.
[7] N. Een and N. Sorensson, "MiniSat v1.13 | A SAT Solver with Conflict-Clause Minimization," SAT Competition, 2005.
[8] E. Goldberg and Y. Novikov. BerkMin, "A Fast and Robust SAT Solver," in Proc. Design, Automation and Test in Europe, pp. 142-149, 2002.
[9] M. Luby, A. Sinclair, and David Zuckerman, "Optimal speedup of Las Vegas algorithms," Information Processing Letters, pp. 173-180, 1993.
[10] J. P. Marques-Silva and K. A. Sakallah, "GRASP: A Search Algorithm for Propositional Satisfiability," IEEE Transaction on Computers, vol. 48, pp. 506-521, 1999.
[11] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik, "Engineering an Efficient SAT Solver," in Proc. Design Automation Conference, pp. 530-535,
June 2001.
[12] R. E. Tarjan, "Depth-first search and linear graph algorithms," SIAM Journal on Computing, pp. 146-160, 1972.
[13] G. Tseitin, "On the complexity of derivation in propositional calculus," Studies in Constr. Math. and Math. Logic, 1968.
[14] R. Zabih and D. A. McAllester, "A Rearrangement Search Strategy for Determining Propositional Satisfiability," in Proc. National Conference on Artificial
Intelligence, pp. 155-160, 1988.
[15] R. Zhang, K. Walus, W. Wang, and G.A. Jullien, "A Method of Majority Logic Reduction for Quantum Cellular Automata," IEEE Transaction on Nanotechnology, vol. 3, no. 4, pp. 443-450, Dec. 2004.
[16] L. Zhang, C.F Madigan, M.H Moskewicz, and S. Malik, "Efficient Conflict Driven Learning in a Boolean Satisfiability Solver," in Proc. International Conference on Computer Aided Design, pp. 279-285, 2001.
[17] http://minisat.se/
[18] http://www.labri.fr/perso/lsimon/glucose/
[19] http://fmv.jku.at/lingeling/
[20] http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html