Abstract
Currently best known upper bounds for many NP-hard problems are obtained by using divide-and-conquer (splitting) algorithms. Roughly speaking, there are two ways of splitting algorithm improvement: a more involved case analysis and an introduction of a new simplification rule. It is clear that case analysis can be executed by computer, so it was considered as a machine task. Recently, several programs for automated case analysis were implemented. However, designing a new simplification rule is usually considered as a human task. In this paper we show that designing simplification rules can also be automated. We present several new (previously unknown) automatically generated simplification rules for the SAT and MAXSAT problems. The new approach allows not only to generate simplification rules, but also to find good splittings. To illustrate our technique we present a new algorithm for (n,3)-MAXSAT that uses both splittings and simplification rules based on our approach and has worst-case running time O(1.2721N L), where N is the number of variables and L is the length of an input formula. This bound improves the previously known bound O(1.3248N L) of Bansal and Raman.
Supported in part by grant No. 1 of the 6th RAS contest-expertise of young scientist projects (1999) and Grant #NSh-2203-2003-1 of the President of Russian Federation for Leading Scientific School Support.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Bansal, N., Raman, V.: Upper bounds for MaxSat: Further improved. In: Aggarwal, A.K., Pandu Rangan, C. (eds.) ISAAC 1999. LNCS, vol. 1741, pp. 247–258. Springer, Heidelberg (1999)
Byskov, J.M., Madsen, B.A., Skjernaa, B.: New algorithms for exact satisfiability. Technical Report RS-03-30, BRICS (2003)
Chen, J., Kanj, I.: Improved exact algorithms for MAX-SAT. In: Rajsbaum, S. (ed.) LATIN 2002. LNCS, vol. 2286, pp. 341–355. Springer, Heidelberg (2002)
Fedin, S.S., Kulikov, A.S.: A 2|E|/4-time algorithm for MAX-CUT. Zapiski nauchnykh seminarov POMI 293, 129–138 (2002)
Fedin, S.S., Kulikov, A.S.: Automated proofs of upper bounds on the running time of splitting algorithms. Zapiski nauchnykh seminarov POMI 316, 111–128 (2004)
Gramm, J., Guo, J., Hüffner, F., Niedermeier, R.: Automated generation of search tree algorithms for hard graph modification problems. Algorithmica 39(4), 321–347 (2004)
Hirsch, E.A.: New worst-case upper bounds for SAT. Journal of Automated Reasoning 24(4), 397–420 (2000)
Nikolenko, S.I., Sirotkin, A.V.: Worst-case upper bounds for sat: automated proof. In: Proceedings of the 8th ESSLLI Student Session, pp. 225–232 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kulikov, A.S. (2005). Automated Generation of Simplification Rules for SAT and MAXSAT. In: Bacchus, F., Walsh, T. (eds) Theory and Applications of Satisfiability Testing. SAT 2005. Lecture Notes in Computer Science, vol 3569. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11499107_35
Download citation
DOI: https://doi.org/10.1007/11499107_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26276-3
Online ISBN: 978-3-540-31679-4
eBook Packages: Computer ScienceComputer Science (R0)