Nội dung được dịch bởi AI, chỉ mang tính chất tham khảo
Về hiệu suất của các bộ giải MaxSAT và MinSAT trên 2SAT-MaxOnes
Tóm tắt
Chúng tôi phân tích và so sánh hai bộ giải cho các vấn đề tối ưu Boolean: WMaxSatz, một bộ giải cho Partial MaxSAT, và MinSatz, một bộ giải cho Partial MinSAT. Cả MaxSAT và MinSAT đều tương tự nhau, nhưng các kết quả trước đây cho thấy khi giải quyết các vấn đề tối ưu sử dụng cả hai bộ giải, hiệu suất có sự khác biệt đáng kể trong một số trường hợp. Để hiểu rõ hơn về sự khác biệt trong hiệu suất của hai bộ giải này, chúng tôi phân tích hành vi của chúng khi giải quyết các ví dụ vấn đề 2SAT-MaxOnes, với điều kiện rằng 2SAT-MaxOnes có thể coi là vấn đề tối ưu đơn giản nhất nhưng là NP-khó mà chúng tôi có thể giải quyết được bằng chúng. Phân tích này dựa trên việc nghiên cứu các giới hạn được tính toán bởi cả hai thuật toán trên một số ví dụ 2SAT-MaxOnes đặc biệt, được đặc trưng bởi sự hiện diện của một số cấu trúc cụ thể. Chúng tôi nhận thấy rằng tỷ lệ các ký tự dương trong các điều khoản là một yếu tố quan trọng liên quan đến chất lượng của các giới hạn được tính toán bởi các thuật toán. Sau đó, chúng tôi cũng nghiên cứu tầm quan trọng của yếu tố này trong độ phức tạp trường hợp điển hình của Random-p 2SAT-MaxOnes, một biến thể của vấn đề nơi các ví dụ được tạo ra ngẫu nhiên với xác suất p có các ký tự dương trong các điều khoản. Đối với trường hợp p=0, các kết quả hiệu suất chỉ ra một lợi thế rõ ràng của MinSatz so với WMaxSatz, nhưng khi chúng tôi xem xét các giá trị dương của p, WMaxSatz bắt đầu cho thấy hiệu suất tốt hơn, mặc dù cùng lúc đó độ phức tạp điển hình của Random-p 2SAT-MaxOnes giảm khi p tăng. Chúng tôi cũng nghiên cứu giá trị điển hình của giới hạn được tính toán bởi hai thuật toán trên các tập hợp ví dụ này, cho thấy rằng hành vi này nhất quán với phân tích của chúng tôi về các giới hạn được tính toán trên các ví dụ cụ thể mà chúng tôi đã nghiên cứu ban đầu.
Từ khóa
Tài liệu tham khảo
Abramé, A., Habet, D.: On the resiliency of unit propagation to max-resolution. In: proceedings of the 24th International Joint Conference on Artificial Intelligence (2015)
Ansótegui, C., Bonet, M.L., Levy, J.: Solving (weighted) partial maxSAT through satisfiability testing. In: Proceedings of SAT, vol. 2009, pp 427–440 (2009)
Ansótegui, C., Bonet, M.L., Levy, J.: Sat-based maxsat algorithms. Artif. Intell. 196, 77–105 (2013)
Argelich, J., Béjar, R., Fernández, C., Mateu, C.: On 2sat-maxones with unbalanced polarity: from easy problems to hard maxclique problems. In: proceedings of CCIA’2011, volume 232 of Frontiers in Artificial Intelligence and Applications, pp 21–30. IOS Press (2011)
Argelich, J., Li, C.M., Manyà, F., Planes, J.: The first and second maxSAT evaluations. JSAT 4(2–4), 251–278 (2008)
Argelich, J., Lynce, I., Marques-Silva, J.P.: On solving boolean multilevel optimization problems. In: Proceedings of IJCAI, vol. 2009, pp 393–398 (2009)
Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.). IOS Press (2009)
Bjorner, N., Narodytska, N.: Maximum satisfiability using cores and correction sets. In: proceedings of the 24th International Joint Conference on Artificial Intelligence (2015)
Cha, B., Iwama, K., Kambayashi, Y., Miyazaki, S.: Local search algorithms for partial maxSAT. In: AAAI’97, pp 263–268 (1997)
Chen, Y., Safarpour, S., Veneris, A.G., Marques-Silva, J.P.: Spatial and temporal design debug using partial maxSAT. In: Proceedings of 19th ACM Great Lakes Symposium on VLSI, pp 345–350 (2009)
Conrad, J., Gomes, C.P., van Hoeve, W.J., Sabharwal, A., Suter, J.: Connections in networks Hardness of feasibility versus optiMality. In: Proceedings of CPAIOR2007, pp 16–28 (2007)
Goerdt, A.: A threshold for unsatisfiability. J. Comput. Syst. Sci. 53(3), 469–486 (2006)
Graça, A., Lynce, I., Marques-Silva, J., Oliveira, A.L.: Haplotype inference combining pedigrees and unrelated individuals. In: WCB09, pp 27–36 (2009)
Håstad, J.: Clique is hard to approximate within n (1−𝜖). In: FOCS’06, pp 627–636 (1996)
Li, C.M., Manyà, F.: An exact inference scheme for minsat. In: Proceedings of the 24th International Joint Conference on Artificial Intelligence (2015)
Li, C.M., Manyà, F., Mohamedou, N.O., Planes, J.: Resolution-based lower bounds in maxSAT. Constraints 15(4), 456–484 (2010)
Li, C.M., Manyà, F., Planes, J.: New inference rules for Max-SAT. J. Artif Intell. Res. (JAIR) 30, 321–359 (2007)
Li, C.M., Quan, Z.: An efficient branch-and-bound algorithm based on maxSAT for the maximum clique problem. In: proceedings of AAAI’10, pp 128–133 (2010)
Li, C.M., Zhu, Z., Manyà, F., Simon, L.: Optimizing with minimum satisfiability. Artif. Intell. 190, 32–44 (2012)
Marques-Silva, J., Argelich, J., Graça, A., Lynce, I.: Boolean lexicographic optimization: algorithms & applications. Ann. Math. Artif. Intell. 62(3-4), 317–343 (2011)
Martins, R., Manquinho, V.M., Lynce, I.: Open-WBO A modular maxsat solver. In: Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, pp 438–445. Proceedings, Vienna, Austria (2014)
Morgado, A., Dodaro, C., Marques-Silva, J.: Core-guided maxsat with soft cardinality constraints. In: Principles and Practice of Constraint Programming - 20th International Conference, CP 2014, pp 564–573. Proceedings, Lyon, France (2014)
Morgado, A., Heras, F., Liffiton, M.H., Planes, J., Marques-Silva, J.: Iterative and core-guided maxSAT solving: A survey and assessment. Constraints 18 (4), 478–534 (2013)
Rosa, E.D., Giunchiglia, E., Maratea, M.: Solving satisfiability problems with preferences. Constraints 15, 485–515 (2010)
Slaney, J.K., Walsh, T.: Phase transition behavior: from decision to optimization. In: Proceedings of SAT2002 (2002)
Zhang, W.: Phase transitions and backbones of 3-SAT and maximum 3-SAT. In: Proceedings of CP 2001, pp 153–167. Springer (2001)
Zhang, W., Korf, R.E.: A study of complexity transitions on the asymmetric traveling salesman problem. Artif. Intell. 81(1-2), 223–239 (1996)