Abstract
We consider the problem of computing tractable approximations to CNF formulas, extending the approach of Selman and Kautz to compute the Horn-LUB to involve renaming of variables. Negative results are given for the quality of approximation in this extended version. On the other hand, experiments for random 3-CNF show that the new algorithms improve both running time and approximation quality. The output sizes and approximation errors exhibit a ‘Horn bump’ phenomenon: unimodal patterns are observed with maxima in some intermediate range of densities. We also present the results of experiments generating pseudo-random satisfying assignments for Horn formulas.
This material is based upon work supported by the National Science Foundation under grant CCF-0431059. A preliminary version of this work appeared in [14].
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
Aspvall, B.: Recognizing disguised NR(1) instances of the satisfiability problem. Journal of Algorithms 1, 97–103 (1980)
Bollobás, B., Kohayakawa, Y., Łuczak, T.: On the evolution of random Boolean functions. In: Frankl, P., et al. (eds.) Extremal Problems for Finite Sets (Visegrád). Bolyai Society Mathematical Studies, vol. 3, pp. 137–156. János Bolyai Mathematical Society, Budapest (1994)
Boros, E.: Maximum renamable Horn sub-CNFs. Discrete Appl. Math. 96-97, 29–40 (1999)
Boufkhad, Y.: Algorithms for propositional KB approximation. In: Proceedings of the 15th National Conference on Artificial Intelligence (AAAI-98) and of the 10th Conference on Innovative Applications of Artificial Intelligence (IAAI-98), pp. 280–285 (1998)
Cadoli, M., Donini, F.M.: A survey on knowledge compilation. AI Communications 10(3–4), 137–150 (1997)
Crama, Y., Ekin, O., Hammer, P.L.: Variable and term removal from Boolean formulae. Discrete Applied Mathematics 75(3), 217–230 (1997)
Darwiche, A., Marquis, P.: A knowledge compilation map. Journal of Artificial Intelligence Research 17, 229–264 (2002)
del Val, A.: First order LUB approximations: characterization and algorithms. Artificial Intelligence 162(1-2), 7–48 (2005)
Erdős, P., Rényi, A.: On the evolution of random graphs. Publ. Math. Inst. Hung. Acad. Sci 5, 17–61 (1960)
Horn, A.: On sentences which are true on direct unions of algebras. J. Symbolic Logic 16, 14–21 (1951)
Jerrum, M.R., Valiant, L.G., Vazirani, V.V.: Random generation of combinatorial structures from a uniform distribution. Theor. Comput. Sci. 43, 169–188 (1986)
Kautz, H., Selman, B.: An empirical evaluation of knowledge compilation by theory approximation. In: Proceedings of the 12th National Conference on Artificial Intelligence, pp. 155–161 (1994)
Kearns, M.J., Vazirani, U.V.: An Introduction to Computational Learning Theory. MIT Press, Cambridge (1994)
Langlois, M., Sloan, R.H., Turán, G.: Horn upper bounds of random 3-CNF: A computational study. In: Ninth Int. Symp. Artificial Intelligence and Mathematics (2006), Available on-line from URL http://anytime.cs.umass.edu/aimath06/
Levin, A.A.: Comparative complexity of disjunctive normal forms (in Russian). Metody Discret. Analiz. 36, 23–38 (1981)
Lewis, H.R.: Renaming a set of clauses as a Horn set. J. ACM 25, 134–135 (1978)
McKinsey, J.C.C.: The decision problem for some classes without quantifiers. J. Symbolic Logic 8, 61–76 (1943)
Mézard, M., Zecchina, R.: The random K-satisfiability problem: from an analytic solution to an efficient algorithm. Physical Review E 66, 56–126 (2002)
Mora, T., Mézard, M., Zecchina, R.: Pairs of SAT assignments and clustering in random Boolean formulae. Submitted to Theoretical Computer Science (2005), available from URL http://www.citebase.org/cgi-bin/citations?id=oai:arXiv.org:cond-mat/0506053
Roth, D.: On the hardness of approximate reasoning. Artificial Intelligence 82, 273–302 (1996)
Vardi, M.Y., Aguirre, A.S.M.: Random 3-SAT and BDDs: The Plot Thickens Further. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, pp. 121–136. Springer, Heidelberg (2001)
Selman, B., Kautz, H.: Knowledge compilation and theory approximation. J. ACM 43, 193–224 (1996)
Sloan, R.H., Szörényi, B., Turán, G.: On k-term DNF with the maximal number of prime implicants. Submitted for publication. Preliminary version available as Electronic Colloquium on Computational Complexity (ECCC) Technical Report TR05-023, available on-line at http://www.eccc.uni-trier.de/eccc/
Truemper, K.: Effective Logic Computation. Wiley-Interscience, Chichester (1998)
van Norden, L., van Maaren, H.: Hidden Threshold Phenomena for Fixed-Density SAT-formulae. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 135–149. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Langlois, M., Sloan, R.H., Turán, G. (2007). Horn Upper Bounds and Renaming. In: Marques-Silva, J., Sakallah, K.A. (eds) Theory and Applications of Satisfiability Testing – SAT 2007. SAT 2007. Lecture Notes in Computer Science, vol 4501. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72788-0_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-72788-0_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72787-3
Online ISBN: 978-3-540-72788-0
eBook Packages: Computer ScienceComputer Science (R0)