Nội dung được dịch bởi AI, chỉ mang tính chất tham khảo
Tối ưu hóa đệ quy trong việc chuyển đổi CNF sang DNF bằng cách sử dụng điện toán lưới
Tóm tắt
Một bài toán NP khó về chuyển đổi CNF sang DNF là một lĩnh vực nghiên cứu rộng lớn trong trí tuệ nhân tạo, thiết kế mạch, FPGA (Miltersen et al. trong On converting CNF to DNF, 2003), PLA, v.v. (Beame trong A switching lemma primer, 1994; Kottler và Kaufmann trong SArTagnan—một bộ giải SAT song song với chia sẻ điều khoản vật lý không khóa, 2011). Tối ưu hóa và các thống kê của nó đã trở thành một yêu cầu tiềm năng cho phân tích và hành vi của việc chuyển đổi dạng chuẩn. Nhiều ứng dụng đang yêu cầu điều này như phân tích gnome, điện toán lưới, tin sinh học, hệ thống hình ảnh, và các tập hợp thô cần thuật toán xử lý biến cao hơn. Câu hỏi đặt ra là—thiết kế và thực hiện chuyển đổi từ dạng chuẩn liên hợp tối ưu sang dạng chuẩn phân liệt tối ưu (những yếu tố nguyên tố) mà là một “chuyển đổi NP khó thành NP hoàn chỉnh”. Do đó, chuyển đổi từ CNF sang DNF chỉ có thể được xem xét để đánh giá hiệu suất tốt nhất cho xử lý biến cao trên các hệ thống tiên tiến. Các đại diện tốt nhất của các hàm Boolean f là những đại diện dưới dạng các phép cộng của các hạng tử (DNF) và dưới dạng các phép nhân của các điều khoản (CNF) (Beame 1994; Kottler và Kaufmann 2011) (Wegener trong Độ phức tạp của các hàm Boolean, 1987). Thật thuận tiện khi định nghĩa kích thước DNF của f là số lượng tối thiểu các hạng tử trong một DNF đại diện cho f và kích thước CNF là số lượng tối thiểu các điều khoản trong một CNF đại diện cho f (Kottler và Kaufmann 2011).
Từ khóa
#CNF #DNF #NP khó #tối ưu hóa #điện toán lưới #hàm BooleanTài liệu tham khảo
Beame P (1994) A switching lemma primer. University of Toronto
Kottler S, Kaufmann M (2011) SArTagnan—a parallel portfolio SAT solver with lockless physical clause sharing. University of Tuebingen, Tuebingen
Rosen KH (2003) Discrete mathematics and it’s applications, 6th edn, CRC Press, Boca Raton
Wegener I (1987) The complexity of boolean functions. Wiley and B.G.Teubner, Stuttgart
Auora R, Hsiao MS (2004) CNF formula simplification using implication reasoning. IEEE Transactions 0-7803-8714-7104 2004
Wahid Chrabakh, Rich Wolski (2003) GrADSAT: a parallel SAT solver for the grid. UCSB CS 2003-05, University of California
Biere A (2010) “Lingeling, Plingeling, PicoSAT and PrecoSAT”, FMV Reports Series, Aug 2010, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria
Hamadi Y, Jabbour S (2009) ManySAT: a parallel SAT solver. J Satisf Boolean Model Comput 6:245–262
Fontoura M, Sadanandan S, Shanmugasundaram J, Vassilvitski S, Vee E, Venkatesan S, Zien J (2010) Efficiently evaluating complex boolean expressions, SIGMOD’10, 6–11 June 2010, Indianapolis, Indiana, USA
Miltersen PB, Radhakrishnan J Wegener I (2003) On converting CNF To DNF, Electronic Colloquium on Computational Complexity, Report No. 17, 2003
Zuim R, de Sousa JT, Coelho CN (2008) Decision heuristic for Davis Putnam, Loveland and Logemann algorithm satisfiability solving based on cube subtraction. IET Comput Digit Tech 2(1):30–39
Raut MK, Singh A (2004) Prime implicates of first order formulas. IITM Int J Comput Sci Appl 1:1–11
Nam G-J, Aloul F (2004) A comparative study of two boolean formulations of FPGA detailed routing constraints. IEEE Trans Comput 53(6):688–696
UCI Machine library for source input dataset (2012). http://archives.uci.com/machine