zbMATH — the first resource for mathematics

Lower and upper bounds for random minimum satisfiability problem. (Lower and upper bounds for random mimimum satisfiability problem.) (English) Zbl 1407.68452
Wang, Jianxin (ed.) et al., Frontiers in algorithmics. 9th international workshop, FAW 2015, Guilin, China, July 3–5, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9130, 115-124 (2015).
Summary: Given a Boolean formula in conjunctive normal form with \(n\) variables and \(m=rn\) clauses, if there exists a truth assignment satisfying \((1-2^{-k}-q(1-2^{-k}))m\) clauses, call the formula \(q\)-satisfiable. The Minimum Satisfiability Problem (MinSAT) is a special case of \(q\)-satisfiable, which asks for an assignment to minimize the number of satisfied clauses. When each clause contains \(k\) literals, it is called Min\(k\)SAT. If each clause is independently and randomly selected from all possible clauses over the \(n\) variables, it is called random MinSAT. In this paper, we give upper and lower bounds of \(r\) (the ratio of clauses to variables) for random \(k\)-CNF formula with \(q\)-satisfiable. The upper bound is proved by the first moment argument, while the proof of lower bound is the second moment with weighted scheme. Interestingly, our experimental results about MinSAT demonstrate that the lower and upper bounds are very tight. Moreover, these results give a partial explanation for the excellent performance of MinSatz, the state-of-the-art MinSAT solver, from the perspective of pruning effects. Finally, we give a conjecture about the relationship between the minimum number and the maximum number of satisfied clauses on random SAT instances.
For the entire collection see [Zbl 1314.68017].
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
MAX-2-SAT; MiniSat
Full Text: DOI
[1] Avidor, A., Zwick, U.: Approximating MIN 2-SAT and MIN 3-SAT. Theor. Comput. Syst. 38(3), 329-345 (2005) · Zbl 1101.68603 · doi:10.1007/s00224-005-1140-7
[2] Achlioptas D., Naor A., Peres, Y.: On the maximum satisfiability of random formulas. In: FOCS 2003, pp. 362-370 (2003) · Zbl 1291.68175
[3] Achlioptas, D., Peres, Y.: The threshold for random k-SAT is · Zbl 1093.68075 · doi:10.1090/S0894-0347-04-00464-3
[4] Anstegui, C., Bonet, M.L., Levy, J.: SAT-based MaxSAT algorithms. Artif. Intell. 196, 77-105 (2013) · Zbl 1270.68265 · doi:10.1016/j.artint.2013.01.002
[5] Anstegui, C., Malitsky, Y., Sellmann, M: MaxSAT by improved instance-specific algorithm configuration. In: AAAI 2014, pp. 2594-2600 (2014)
[6] Bollobas, B., Borgs, C., Chayes, J.T., Kim, J.H., Wilson, D.B.: The scaling window of the 2-SAT transition. Random Struct. Algorithms 18(3), 201-256 (2001) · Zbl 0979.68053 · doi:10.1002/rsa.1006
[7] Bollobas, B.: Random Graphs. Cambridge Studies in Advanced Mathematics, vol. 73, 2nd edn. Cambridge University Press, Cambridge (2001) · Zbl 0979.05003 · doi:10.1017/CBO9780511814068
[8] Cai, S.W., Luo, C., Thornton, J., Su, K.L.: Tailoring local search for partial MaxSAT. In: AAAI 2014, pp. 2623-2629 (2014)
[9] Coppersmith, D., Gamarnik, D., Hajiaghayi, M.T., Sorkin, G.B.: Random MAX SAT random MAX CUT, and their phase transitions. Random Struct. Algorithms 24, 502-545 (2004) · Zbl 1077.68118 · doi:10.1002/rsa.20015
[10] Eén, N., Sörensson, N.: Translating pseudo-boolean constraints into SAT. J. Satisfiability Boolean Model. Comput. 2(2006), 21-26 (2006) · Zbl 1116.68083
[11] Gramm, J., Hirsch, E.A., Niedermeier, R., Rossmanith, P.: Worst-case upper bounds for MAX-2-SAT with an application to MAX-CUT. Discrete Appl. Math. 130, 139-155 (2003) · Zbl 1051.68078 · doi:10.1016/S0166-218X(02)00402-X
[12] Hirsch, E.A.: A new algorithm for MAX-2-SAT. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 65-73. Springer, Heidelberg (2000) · Zbl 0959.68047 · doi:10.1007/3-540-46541-3_5
[13] Huang, P., Yin, M.H.: An upper (lower) bound for Max(Min) CSP. Sci. China Inf. Sci. 57(7), 1-9 (2014) · Zbl 1343.68117
[14] Kohli, R., Krishnamurti, R., Mirchandani, P.: The minimum satisfiability problem. SIAM J. Discrete Math. 7, 275-283 (1994) · Zbl 0806.68060 · doi:10.1137/S0895480191220836
[15] Li, C.M., Many, F., Nouredine, N.O., Planes, J.: Resolution-based lower bounds in MaxSAT. Constraints 15(4), 456-484 (2010) · Zbl 1208.68204 · doi:10.1007/s10601-010-9097-9
[16] Li, C.M., Manyà, F., Quan, Z., Zhu, Z.: Exact MinSAT solving. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 363-368. Springer, Heidelberg (2010) · Zbl 1306.68164 · doi:10.1007/978-3-642-14186-7_33
[17] Li, C.M., Zhu, Z., Many, F., Simon, L.: Minimum satisfiability and its applications. In: IJCAI 2011, pp. 605-610 (2011)
[18] Li, C.M., Zhu, Z., Many, F., Simon, L.: Optimizing with minimum satisfiability. Artif. Intell. 190, 32-44 (2012) · Zbl 1251.68209 · doi:10.1016/j.artint.2012.05.004
[19] Lin, H., Su, K.L., Li, C.M.: Within problem learning for efficient lower bound computation in Max-SAT solving. In: AAAI 2008, pp. 351-356 (2008)
[20] Marathe, M.V., Ravi, S.S.: On approximation algorithms for the minimum satisfiability problem. Inf. Process. Lett. 58, 23-29 (1996) · Zbl 0875.68544 · doi:10.1016/0020-0190(96)00031-2
[21] Robinson, N., Gretton, C., Pham, D.N., Sattar, A.: A compact and efficient SAT encoding for planning. In: ICAPS 2008, pp. 296-303 (2008)
[22] Spencer, J.H.: Ten Lectures on the Probabilistic Method. SIAM, Philadelphia (1994) · Zbl 0822.05060 · doi:10.1137/1.9781611970074
[23] Whitley, D., Howe, A.E., Hains, D.: Greedy or Not? Best Improving versus first improving stochastic local search for MAXSAT. In: AAAI 2013 (2013)
[24] Xu, X.L., Gao, Z.S., Xu, K.: A tighter upper bound for random MAX 2-SAT. Inf. Process. Lett. 111(3), 115-119 (2011) · Zbl 1260.68164 · doi:10.1016/j.ipl.2010.11.002
[25] Xu, K., Li, W.: Exact phase transitions in random constraint satisfaction problems. J. Artif. Intell. Res. (JAIR) 12, 93-103 (2000) · Zbl 0940.68099
[26] Zhou, G.Y., G Z.S., Liu J.: On the lower bounds of random Max 3 and 4-SAT. Manuscript
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.