×

Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions. (English) Zbl 07418688

Summary: The Boolean SATisfiability problem (SAT) is of central importance in computer science. Although SAT is known to be NP-complete, progress on the engineering side – especially that of Conflict-Driven Clause Learning (CDCL) and Local Search SAT solvers – has been remarkable. Yet, while SAT solvers, aimed at solving industrial-scale benchmarks in Conjunctive Normal Form (CNF), have become quite mature, SAT solvers that are effective on other types of constraints (e.g., cardinality constraints and XORs) are less well-studied; a general approach to handling non-CNF constraints is still lacking.
To address the issue above, we design FourierSAT an incomplete SAT solver based on Fourier Analysis (also known as Walsh-Fourier Transform) of Boolean functions, a technique to represent Boolean functions by multilinear polynomials. By such a reduction to continuous optimization, we propose an algebraic framework for solving systems consisting of different types of constraints. The idea is to leverage gradient information to guide the search process in the direction of local improvements. We show this reduction enjoys interesting theoretical properties. Empirical results demonstrate that FourierSAT can be a useful complement to other solvers on certain classes of benchmarks.

MSC:

68Txx Artificial intelligence
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Ignatiev, A.; Pereira, F.; Narodytska, N.; Marques-Silva, J., A sat-based approach to learn explainable decision sets, (Galmiche, D.; Schulz, S.; Sebastiani, R., Automated Reasoning (2018), Springer International Publishing: Springer International Publishing Cham), 627-645 · Zbl 06958127
[2] Velev, M. N., Efficient translation of boolean formulas to cnf in formal verification of microprocessors, (ASP-DAC 2004: Asia and South Pacific Design Automation Conference 2004 (IEEE Cat. No. 04EX753) (2004)), 310-315
[3] Chavira, M.; Darwiche, A., On probabilistic inference by weighted model counting, Artif. Intell., 172, 6, 772-799 (2008) · Zbl 1182.68297
[4] Zulkoski, E.; Ganesh, V.; Czarnecki, K., Mathcheck: a math assistant via a combination of computer algebra systems and sat solvers, (Felty, A. P.; Middeldorp, A., Automated Deduction - CADE-25 (2015), Springer International Publishing: Springer International Publishing Cham), 607-622 · Zbl 1465.68300
[5] Marques-Silva, J. P.; Sakallah, K. A., GRASP: a search algorithm for propositional satisfiability, IEEE Trans. Comput., 48, 5, 506-521 (1999) · Zbl 1392.68388
[6] Davis, M.; Putnam, H., A computing procedure for quantification theory, J. ACM, 7, 3, 201-215 (1960) · Zbl 0212.34203
[7] Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem-proving, Commun. ACM, 5, 7, 394-397 (1962) · Zbl 0217.54002
[8] Moskewicz, M. W.; Madigan, C. F.; Zhao, Y.; Zhang, L.; Malik, S., Chaff: engineering an efficient sat solver, (DAC ’01 (2001)), 530-535
[9] Eén, N.; Sörensson, N., An extensible SAT-solver, (SAT (2003)), 502-518 · Zbl 1204.68191
[10] Biere, A., PicoSAT essentials, JSAT, 4, 75-97 (2008) · Zbl 1159.68403
[11] Biere, A., Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010 (2010)
[12] Audemard, G.; Simon, L., Lazy clause exchange policy for parallel SAT solvers, (SAT 2014, Cham (2014)), 197-205 · Zbl 1423.68431
[13] Liang, J. H., Machine learning for sat solvers (Dec. 2018), University of Waterloo, Ph.D. thesis
[14] Selman, B.; Levesque, H.; Mitchell, D., A new method for solving hard satisfiability problems (1992)
[15] B. Selman, H. Kautz, B. Cohen, Local Search Strategies for Satisfiability Testing, Second DIMACS Implementation, Challenge 26. · Zbl 0864.90093
[16] Gong, W.; Zhou, X., A survey of SAT solver, AIP Conf. Proc., 1836, 1, Article 020059 pp. (2017)
[17] McAllester, D.; Selman, B.; Kautz, H., (Evidence for Invariants in Local Search (1997))
[18] Balint, A.; Fröhlich, A., Improving stochastic local search for SAT with a new probability distribution, (SAT 2010 (2010)), 10-15 · Zbl 1306.68150
[19] Hoos, H.; Stützle, T., Local search algorithms for sat: an empirical evaluation, J. Autom. Reason., 24, 421-481 (2000) · Zbl 0961.68039
[20] Hutter, F.; Tompkins, D. A.D.; Hoos, H., Scaling and probabilistic smoothing: efficient dynamic local search for sat, (CP (2002))
[21] Tompkins, D. A.D.; Hoos, H. H., Ubcsat: an implementation and experimentation environment for sls algorithms for sat and max-sat, (Hoos, H. H.; Mitchell, D. G., Theory and Applications of Satisfiability Testing (2005), Springer Berlin Heidelberg: Springer Berlin Heidelberg Berlin, Heidelberg), 306-320 · Zbl 1122.68620
[22] Balint, A.; Schöning, U., Choosing probability distributions for stochastic local search and the role of make versus break, (SAT 2012 (2012)), 16-29 · Zbl 1273.68333
[23] Lei, Z.; Cai, S., Solving (weighted) partial maxsat by dynamic local search for sat, (Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence. Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI-18, International Joint Conferences on Artificial Intelligence Organization (2018)), 1346-1352
[24] Brueggemann, T.; Kern, W., An improved deterministic local search algorithm for 3-SAT, Theor. Comput. Sci., 329, 1, 303-313 (2004) · Zbl 1086.68051
[25] Fang, H.; Ruml, W., Complete local search for propositional satisfiability, (AAAI (2004))
[26] Audemard, G.; Simon, L., Gunsat: A Greedy Local Search Algorithm for Unsatisfiability, 2256-2261 (2007)
[27] Bogdanov, A.; Khovratovich, D.; Rechberger, C., Biclique cryptanalysis of the full AES, (ASIACRYPT 2011 (2011)) · Zbl 1227.94032
[28] Costa, M.-C.; de Werra, D.; Picouleau, C.; Ries, B., Graph coloring with cardinality constraints on the neighborhoods, Discrete Optim., 6, 4, 362-369 (2009) · Zbl 1175.05053
[29] Dinur, I.; Regev, O.; Smyth, C., The hardness of 3-uniform hypergraph coloring, Combinatorica, 25, 5, 519-535 (2005) · Zbl 1106.68080
[30] Feldman, J.; Wainwright, M. J.; Karger, D. R., Using linear programming to decode binary linear codes, IEEE Trans. Inf. Theory, 51, 3, 954-972 (2005) · Zbl 1234.94086
[31] Gwynne, M.; Kullmann, O., On sat representations of xor constraints, (Dediu, A.-H.; Martín-Vide, C.; Sierra-Rodríguez, J.-L.; Truthe, B., Language and Automata Theory and Applications (2014), Springer International Publishing: Springer International Publishing Cham), 409-420 · Zbl 1408.68077
[32] Philipp, T.; Steinke, P., Pblib – a library for encoding pseudo-boolean constraints into cnf, (Heule, M.; Weaver, S., Theory and Applications of Satisfiability Testing - SAT 2015 (2015), Springer International Publishing: Springer International Publishing Cham), 9-16 · Zbl 1471.68261
[33] Prestwich, S., CNF encodings, (Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications (2009))
[34] Quimper, C.-G.; Walsh, T., Decomposing global grammar constraints, (CP 2007 (2007)), 590-604 · Zbl 1145.68529
[35] Kautz, H.; Mcallester, D.; Selman, B., Exploiting variable dependency in local search, (Abstracts of the Poster Sessions of IJCAI-97 (1997))
[36] Martins, R.; Manquinho, V.; Lynce, I., Exploiting cardinality encodings in parallel maximum satisfiability, (ICTAI (2011)), 313-320
[37] Soos, M.; Nohl, K.; Castelluccia, C., Extending SAT solvers to cryptographic problems, (SAT (2009)), 244-257
[38] Liffiton, M. H.; Maglalang, J. C., A cardinality solver: more expressive constraints for free, (SAT 2012 (2012))
[39] Sheini, H. M.; Sakallah, K. A., Pueblo: a hybrid pseudo-boolean sat solver, JSAT, 2, 165-189 (2006) · Zbl 1116.68090
[40] Elffers, J.; Nordström, J., Divide and Conquer: towards faster pseudo-Boolean solving, (Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence. Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI-18, International Joint Conferences on Artificial Intelligence Organization (2018)), 1291-1299
[41] Bayless, S.; Bayless, N.; Hoos, H. H.; Hu, A. J., SAT modulo monotonic theories, (AAAI (2015))
[42] O’Donnell, R., Analysis of Boolean Functions (2014), Cambridge University Press: Cambridge University Press New York, NY, USA · Zbl 1336.94096
[43] Linial, N.; Mansour, Y.; Nisan, N., Constant depth circuits, Fourier transform, and learnability, (ASFCS (1989))
[44] Wei, C.; Ermon, S., General bounds on satisfiability thresholds for random CSPs via Fourier analysis (2017)
[45] Achim, T.; Sabharwal, A.; Ermon, S., Beyond parity constraints: Fourier analysis of hash functions for inference, (ICML (2016)), 2254-2262
[46] Xue, Y.; Ermon, S.; Le Bras, R.; Gomes, C. P.; Selman, B., Variable elimination in the Fourier domain (2015)
[47] Ge, R.; Huang, F.; Jin, C.; Yuan, Y., Escaping from saddle points — online stochastic gradient for tensor decomposition (2015)
[48] Jin, C.; Netrapalli, P.; Ge, R.; Kakade, S. M.; Jordan, M. I., Stochastic gradient descent escapes saddle points efficiently (2019)
[49] Lee, J. D.; Simchowitz, M.; Jordan, M. I.; Recht, B., Gradient descent converges to minimizers (2016)
[50] Zhang, Z., Solving Hybrid Boolean Constraints by Fourier Expansions and Continuous Optimization (Jan. 2020)
[51] Kyrillidis, A.; Shrivastava, A.; Vardi, M. Y.; Zhang, Z., FourierSAT: a Fourier expansion-based algebraic framework for solving hybrid Boolean constraints, (AAAI (2020))
[52] Wah, B.; Shang, Y., A discrete lagrangian-based global-search method for solving satisfiability problems, J. Glob. Optim., 12, 1, 61-99 (1998) · Zbl 0904.90154
[53] Morris, P., The breakout method for escaping from local minima, (AAAI (1993))
[54] Dixon, H. E.; Ginsberg, M. L.; Luks, E. M.; Parkes, A. J., Generalizing boolean satisfiability ii: theory, J. Artif. Intell. Res., 22, 481-534 (2004) · Zbl 1080.68660
[55] Tran, Q.-N.; Vardi, M., Groebner bases computation in boolean rings for symbolic model checking, (Proceedings of the IASTED International Conference on Modelling and Simulation (2007)), 440-445
[56] Clegg, M.; Edmonds, J.; Impagliazzo, R., Using the groebner basis algorithm to find proofs of unsatisfiability, (Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing. Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing, STOC ’96 (1996), Association for Computing Machinery: Association for Computing Machinery New York, NY, USA), 174-183 · Zbl 0938.68825
[57] Ritirc, D.; Biere, A.; Kauers, M., Improving and extending the algebraic approach for verifying gate-level multipliers, (2018 Design, Automation Test in Europe Conference, Exhibition (DATE) (2018)), 1556-1561
[58] Condrat, C.; Kalla, P., A gröbner basis approach to cnf-formulae preprocessing, (Grumberg, O.; Huth, M., Tools and Algorithms for the Construction and Analysis of Systems (2007), Springer Berlin Heidelberg: Springer Berlin Heidelberg Berlin, Heidelberg), 618-631 · Zbl 1186.68576
[59] Warners, J. P.; van Maaren, H., A two-phase algorithm for solving a class of hard satisfiability problems, Oper. Res. Lett., 23, 3, 81-88 (1998) · Zbl 0960.90100
[60] Horáček, J.; Kreuzer, M., On conversions from cnf to anf, Symbolic Computation and Satisfiability Checking. Symbolic Computation and Satisfiability Checking, J. Symb. Comput., 100, 164-186 (2020) · Zbl 1432.68600
[61] Choo, D.; Soos, M.; Chai, K. M.A.; Meel, K. S., Bosphorus: bridging anf and cnf solvers (2018)
[62] Gu, Jun, Global optimization for satisfiability (sat) problem, IEEE Trans. Knowl. Data Eng., 6, 3, 361-381 (1994)
[63] Calinescu, G.; Chekuri, C.; Pál, M.; Vondrák, J., Maximizing a monotone submodular function subject to a matroid constraint, SIAM J. Comput., 40, 6, 1740-1766 (2011) · Zbl 1234.68459
[64] Walsh, J. L., A closed set of normal orthogonal functions, Am. J. Math., 45, 1, 5-24 (1923) · JFM 49.0293.03
[65] Hadamard, J., Resolution d’une question relative aux determinants, Bull. Sci. Math., 2, 240-246 (1893) · JFM 25.0221.02
[66] Bonami, A., Étude des coefficients de fourier des fonctions de \(l^p(g)\), Ann. Inst. Fourier, 20, 2, 335-402 (1970) · Zbl 0195.42501
[67] Kahn, J.; Kalai, G.; Linial, N., The influence of variables on boolean functions, ([Proceedings 1988] 29th Annual Symposium on Foundations of Computer Science (1988)), 68-80
[68] Tal, A., Tight bounds on the fourier spectrum of ac0, (Proceedings of the 32nd Computational Complexity Conference. Proceedings of the 32nd Computational Complexity Conference, CCC ’17 (2017), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik Dagstuhl, DEU)
[69] Kalai, G.; Safra, S., Threshold phenomena and influence, with some perspectives from mathematics, computer science, and economics (2005), The Federmann Center for the Study of Rationality, the Hebrew University: The Federmann Center for the Study of Rationality, the Hebrew University Jerusalem, Discussion paper series
[70] Kalai, G., A fourier-theoretic perspective on the condorcet paradox and arrow’s theorem, Adv. Appl. Math., 29, 412-426 (2002) · Zbl 1038.91027
[71] Achim, T.; Sabharwal, A.; Ermon, S., Beyond parity constraints: Fourier analysis of hash functions for inference, (Balcan, M. F.; Weinberger, K. Q., Proceedings of the 33rd International Conference on Machine Learning. Proceedings of the 33rd International Conference on Machine Learning, Proceedings of Machine, vol. 48 (2016), Learning Research, PMLR, New York: Learning Research, PMLR, New York New York, USA), 2254-2262
[72] Edwards, C. R., The application of the rademacher-walsh transform to boolean function classification and threshold logic synthesis, IEEE Trans. Comput., C-24, 1, 48-62 (1975) · Zbl 0291.94018
[73] Moore, J.; Fazel, K.; Thornton, M. A.; Miller, D. M., Boolean function matching using walsh spectral decision diagrams, (2006 IEEE Dallas/CAS Workshop on Design, Applications, Integration and Software (2006)), 127-130
[74] Thornton, M. A.; Nair, V. S.S., Efficient calculation of spectral coefficients and their applications, IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., 14, 11, 1328-1341 (1995)
[75] Bryant, R. E., Binary decision diagrams and beyond: enabling technologies for formal verification, (Proceedings of IEEE International Conference on Computer Aided Design (ICCAD) (1995)), 236-243
[76] Moore, J.; Fazel, K.; Thornton, M. A.; Miller, D. M., Boolean function matching using walsh spectral decision diagrams, (2006 IEEE Dallas/CAS Workshop on Design, Applications, Integration and Software (2006)), 127-130
[77] Thornton, M.; Drechsler, R.; Miller, D., Spectral techniques in vlsi cad (2001)
[78] Savický, P., On the bent boolean functions that are symmetric, Eur. J. Comb., 15, 4, 407-410 (1994) · Zbl 0797.94011
[79] Dawson, E.; Wu, C.-K., On the linear structure of symmetric boolean functions, Australas. J. Comb., 16, 239-243 (1997) · Zbl 0889.94016
[80] MA317-UBC, Lecture 1, harmonic functions
[81] Thornton, M.; Nair, V., Efficient spectral coefficient calculation using circuit output probabilities, Digit. Signal Process., 4, 4, 245-254 (1994)
[82] Kyrillidis, A.; Vardi, M. Y.; Zhang, Z., On continuous local BDD-based search for hybrid SAT solving (2020)
[83] Dauphin, Y. N.; Pascanu, R.; Gulcehre, C.; Cho, K.; Ganguli, S.; Bengio, Y., Identifying and attacking the saddle point problem in high-dimensional non-convex optimization, (Advances in Neural Information Processing Systems 27 (2014), Curran Associates, Inc.), 2933-2941
[84] Choromanska, A.; Henaff, M.; Mathieu, M.; Ben Arous, G.; LeCun, Y., The loss surfaces of multilayer networks (2014)
[85] Nesterov, Y., Introductory Lectures on Convex Optimization: A Basic Course (2014)
[86] He, N., Lecture Notes in IE, vol. 598 (2016), Big Data Optimization
[87] Nesterov, Y., Introductory Lectures on Convex Optimization: A Basic Course (2014), Springer Publishing Company, Incorporated
[88] Bubeck, S., Convex optimization: algorithms and complexity (2014)
[89] D. Kraft, A Software Package for Sequential Quadratic Programming, Forschungsbericht- Deutsche Forschungs- und Versuchsanstalt fur Luft- und Raumfahrt. · Zbl 0646.90065
[90] Jones, E.; Oliphant, T.; Peterson, P., SciPy: Open Source Scientific Tools for Python (2001)
[91] Cai, S.; Su, K.; Luo, C., Improving walksat for random k-satisfiability problem with k > 3, (AAAI (2013))
[92] Ignatiev, A.; Morgado, A.; Marques-Silva, J., PySAT: a python toolkit for prototyping with SAT oracles, (SAT (2018)), 428-437 · Zbl 1484.68215
[93] Sakai, M.; Nabeshima, H., Construction of an robdd for a pb-constraint in band form and related techniques for pb-solvers, IEICE Trans. Inf. Syst., E98.D, 6, 1121-1127 (2015)
[94] Martins, R.; Manquinho, V.; Lynce Open-wbo, I., A modular maxsat solver, (Sinz, C.; Egly, U., Theory and Applications of Satisfiability Testing - SAT 2014 (2014), Springer International Publishing: Springer International Publishing Cham), 438-445 · Zbl 1423.68461
[95] Berg, J.; Demirović, E.; Stuckey, P. J., Core-boosted linear search for incomplete maxsat, (Rousseau, L.-M.; Stergiou, K., Integration of Constraint Programming, Artificial Intelligence, and Operations Research (2019), Springer International Publishing: Springer International Publishing Cham), 39-56 · Zbl 07116684
[96] Sinz, C., Towards an optimal CNF encoding of Boolean cardinality constraints, (CP 2005 (2005)), 827-831 · Zbl 1153.68488
[97] Batcher, K. E., Sorting networks and their applications, (Spring Joint Computer Conference, AFIPS ’68. Spring Joint Computer Conference, AFIPS ’68, Spring (1968))
[98] Bailleux, O.; Boufkhad, Y., Efficient CNF encoding of Boolean cardinality constraints, (CP (2003)) · Zbl 1273.68332
[99] Eén, N.; Sörensson, N., Translating pseudo-Boolean constraints into SAT, JSAT, 2, 1-26 (2006) · Zbl 1116.68083
[100] Li, C. M., Integrating equivalency reasoning into Davis-Putnam procedure, (AAAI (2000), AAAI Press), 291-296
[101] Gurobi Optimization, L. (2019), Gurobi Optimizer Reference Manual
[102] Crawford, J. M.; Kearns, M. J., The Minimal Disagreement Parity Problem as a Hard Satisfiability Problem (1994)
[103] Hoos, H.; Stützle, T., (SATLIB: an Online Resource for Research on SAT (04 2000)) · Zbl 0979.68128
[104] Dudek, J. M.; Meel, K. S.; Vardi, M. Y., Combining the k-CNF and XOR phase-transitions, (IJCAI (2016))
[105] Pote, Y.; Joshi, S.; Meel, K. S., Phase transition behavior of cardinality and XOR constraints, (IJCAI-19 (2019))
[106] Cox, D. A.; Little, J.; O’shea, D., Ideals, Varieties and Algorithms (1994)
[107] Loera, J. A.D.; Lee, J.; Malkin, P. N.; Margulies, S., Computing infeasibility certificates for combinatorial problems through Hilbert’s Nullstellensatz, J. Symb. Comput., 46, 1260-1283 (2011) · Zbl 1247.13026
[108] Barbosa Julian, Romero, (Applied Hilbert’s Nullstellensatz for Combinatorial Problems (2016))
[109] Bruck, J.; Smolensky, R., Polynomial threshold functions, AC0 functions, and spectral norms, SIAM J. Comput., 21, 1, 33-42 (1992) · Zbl 0743.68063
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.