Abstract
The equivalence problem for monotone formulae in normal form Monet is in coNP, is probably not coNP-complete [1], and is solvable in quasi-polynomial time n o(logn) [2].
We show that the straightforward reduction from Monet to UnSat yields instances, on which actual Sat-solvers (SAT4J) are slower than current implementations of Monet-algorithms [3]. We then improve these implementations of Monet-algorithms notably, and we investigate which techniques from Sat-solving are useful for Monet. Finally, we give an advanced reduction from Monet to UnSat that yields instances, on which the Sat-solvers reach running times, that seem to be magnitudes better than what is reachable with the current implementations of Monet-algorithms.
This work was supported by the DFG under grant MU 1226/8-1 (SPP 1307/2).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Kavvadias, D.J., Stavropoulos, E.C.: Checking monotone Boolean duality with limited nondeterminism. Technical Report TR2003/07/02, Univ. of Patras (2003)
Fredman, M.L., Khachiyan, L.: On the complexity of dualization of monotone disjunctive normal forms. Journal of Algorithms 21(3), 618–628 (1996)
Hagen, M., Horatschek, P., Mundhenk, M.: Experimental comparison of the two Fredman-Khachiyan-algorithms. In: Proc. ALENEX, pp. 154–161 (2009)
Reith, S.: On the complexity of some equivalence problems for propositional calculi. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 632–641. Springer, Heidelberg (2003)
Eiter, T., Gottlob, G.: Hypergraph transversal computation and related problems in logic and AI. In: Flesca, S., Greco, S., Leone, N., Ianni, G. (eds.) JELIA 2002. LNCS (LNAI), vol. 2424, pp. 549–564. Springer, Heidelberg (2002)
Eiter, T., Gottlob, G., Makino, K.: New results on monotone dualization and generating hypergraph transversals. SIAM J. on Computing 32(2), 514–537 (2003)
Papadimitriou, C.H.: NP-completeness: A retrospective. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 2–6. Springer, Heidelberg (1997)
Bailey, J., Manoukian, T., Ramamohanarao, K.: A fast algorithm for computing hypergraph transversals and its application in mining emerging patterns. In: Proc. of the 3rd IEEE Intl. Conference on Data Mining (ICDM 2003), pp. 485–488 (2003)
Dong, G., Li, J.: Mining border descriptions of emerging patterns from dataset pairs. Knowledge and Information Systems 8(2), 178–202 (2005)
Khachiyan, L., Boros, E., Elbassioni, K.M., Gurvich, V.: An efficient implementation of a quasi-polynomial algorithm for generating hypergraph transversals. Discrete Applied Mathematics 154(16), 2350–2372 (2006)
Kavvadias, D.J., Stavropoulos, E.C.: An efficient algorithm for the transversal hypergraph generation. J. of Graph Algorithms and Applications 9(2), 239–264 (2005)
Lin, L., Jiang, Y.: The computation of hitting sets: Review and new algorithms. Information Processing Letters 86(4), 177–184 (2003)
Torvik, V.I., Triantaphyllou, E.: Minimizing the average query complexity of learning monotone Boolean functions. INFORMS Journal on Computing 14(2), 144–174 (2002)
Uno, T., Satoh, K.: Detailed description of an algorithm for enumeration of maximal frequent sets with irredundant dualization. In: Proc. FIMI (2003)
Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)
Pretolani, D.: Efficiency and stability of hypergraph sat algorithms. In: Proc. DIMACS Challenge II Workshop (1993)
Buro, M., Büning, H.K.: Report on a SAT competition (1992)
Kullmann, O.: Investigating the behaviour of a sat solver on random formulas. Technical Report CSR 23-2002, University of Wales (2002)
Quine, W.: Two theorems about truth functions. Boletin de la Sociedad Matemática Mexicana 10, 64–70 (1953)
Tamaki, H.: Space-efficient enumeration of minimal transversals of a hypergraph. In: Proc. SIGAL, pp. 29–36 (2000)
Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A. (ed.) Studies in Constructive Mathematics and Mathematical Logics, Part II, pp. 115–125 (1968)
Galesi, N., Kullmann, O.: Polynomial time SAT decision, hypergraph transversals and the hermitian rank. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 89–104. Springer, Heidelberg (2005)
Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation 7, 59–64 (2010)
Repository, UCI (2010), http://www.archive.ics.uci.edu/ml/
Repository, FIMI (2010), http://www.fimi.ua.ac.be/
Murakami, K.: Personal communication (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mundhenk, M., Zeranski, R. (2011). How to Apply SAT-Solving for the Equivalence Test of Monotone Normal Forms. In: Sakallah, K.A., Simon, L. (eds) Theory and Applications of Satisfiability Testing - SAT 2011. SAT 2011. Lecture Notes in Computer Science, vol 6695. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21581-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-21581-0_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21580-3
Online ISBN: 978-3-642-21581-0
eBook Packages: Computer ScienceComputer Science (R0)