zbMATH — the first resource for mathematics

Volt: a lazy grounding framework for solving very large maxsat instances. (English) Zbl 06512581
Heule, Marijn (ed.) et al., Theory and applications of satisfiability testing – SAT 2015. 18th international conference, Austin, TX, USA, September 24–27, 2015. Proceedings. Cham: Springer (ISBN 978-3-319-24317-7/pbk; 978-3-319-24318-4/pbk). Lecture Notes in Computer Science 9340, 299-306 (2015).
Summary: Very large MaxSAT instances, comprising \(10^{20}\) clauses and beyond, commonly arise in a variety of domains. We present VOLT, a framework for solving such instances, using an iterative, lazy grounding approach. In each iteration, VOLT grounds a subset of clauses in the MaxSAT problem, and solves it using an off-the-shelf MaxSAT solver. VOLT provides a common ground to compare and contrast different lazy grounding approaches for solving large MaxSAT instances. We cast four diverse approaches from the literature on information retrieval and program analysis as instances of VOLT. We have implemented VOLT and evaluate its performance under different state-of-the-art MaxSAT solvers.
For the entire collection see [Zbl 1323.68009].
68Q25 Analysis of algorithms and problem complexity
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Full Text: DOI
[1] http://www.maxsat.udl.cat/14/index.html
[2] http://web.udl.es/usuaris/q4374304/
[3] Blackburn, S.M., Garner, R., Hoffman, C., Khan, A.M., McKinley, K.S., Bentzur, R., Diwan, A., Feinberg, D., Frampton, D., Guyer, S.Z., Hirzel, M., Hosking, A., Jump, M., Lee, H., Moss, J.E.B., Phansalkar, A., Stefanović, D., VanDrunen, T., von Dincklage, D., Wiedermann, B.: The DaCapo benchmarks: Java benchmarking development and analysis. In: OOPSLA (2006) · doi:10.1145/1167473.1167488
[4] Chaganty, A., Lal, A., Nori, A.V., Rajamani, S.K.: Combining relational learning with SMT solvers using CEGAR. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 447–462. Springer, Heidelberg (2013) · Zbl 06233052 · doi:10.1007/978-3-642-39799-8_30
[5] Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. JACM 50(5) (2003) · Zbl 1325.68145 · doi:10.1145/876638.876643
[6] Davies, J., Bacchus, F.: Postponing optimization to speed up MAXSAT solving. In: CP (2013) · Zbl 06294280 · doi:10.1007/978-3-642-40627-0_21
[7] Janota, M.: MiFuMax – a literate MaxSAT solver (2013)
[8] Marques-Silva, J., Ignatiev, A., Morgado, A.: MSCG - Maximum Satisfiability: a Core-Guided approach (2014)
[9] Kok, S., Sumner, M., Richardson, M., Singla, P., Poon, H., Lowd, D., Domingos, P.: The alchemy system for statistical relational AI. Tech. rep., Department of Computer Science and Engineering, University of Washington, Seattle, WA (2007). http://alchemy.cs.washington.edu
[10] Kügel, A.: Improved exact solver for the weighted MAX-SAT problem. In: POS 2010. Pragmatics of SAT (2010)
[11] Lewis, H.R.: Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci. 21(3), 317–353 (1980) · Zbl 0471.03034 · doi:10.1016/0022-0000(80)90027-6
[12] Luo, C., Cai, S., Wu, W., Jie, Z., Su, K.: CCLS: an efficient local search algorithm for weighted maximum satisfiability. IEEE Trans. Computers 64(7), 1830–1843 (2015) · Zbl 1360.68786 · doi:10.1109/TC.2014.2346196
[13] Morgado, A., Dodaro, C., Marques-Silva, J.: Core-guided MaxSAT with soft cardinality constraints. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 564–573. Springer, Heidelberg (2014) · Zbl 06461437 · doi:10.1007/978-3-319-10428-7_41
[14] Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSAT resolution. In: AAAI (2014) · Zbl 1423.68432
[15] Niu, F., Ré, C., Doan, A., Shavlik, J.W.: Tuffy: scaling up statistical inference in markov logic networks using an RDBMS. In: VLDB (2011) · doi:10.14778/1978665.1978669
[16] Noessner, J., Niepert, M., Stuckenschmidt, H.: RockIt: Exploiting parallelism and symmetry for MAP inference in statistical relational models. In: AAAI (2013)
[17] Riedel, S.: Improving the accuracy and efficiency of MAP inference for markov logic. In: UAI (2008)
[18] Whaley, J., Lam, M.: Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In: PLDI (2004) · doi:10.1145/996841.996859
[19] Zhang, X., Mangal, R., Grigore, R., Naik, M., Yang, H.: On abstraction refinement for program analyses in datalog. In: PLDI (2014)
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.