ในวิทยาการคอมพิวเตอร์อี-กราฟ (e-graph)คือโครงสร้างข้อมูลที่เก็บความสัมพันธ์สมมูลระหว่างคำศัพท์ต่างๆ ใน ภาษาใดภาษาหนึ่ง

ให้เป็นเซตของฟังก์ชันที่ไม่ถูกตีความโดยที่เป็นเซตย่อยของที่ประกอบด้วยฟังก์ชันที่มีอาร์กิวเมนต์ให้เป็นเซตที่นับได้ของตัวระบุที่ไม่โปร่งใสซึ่งสามารถเปรียบเทียบความเท่าเทียมกันได้ เรียกว่ารหัสคลาส eการประยุกต์ใช้กับรหัสคลาส e จะใช้สัญลักษณ์และเรียกว่าโหนด e${\displaystyle \Sigma }$${\displaystyle \Sigma _{n}}$${\displaystyle \Sigma }$${\displaystyle n}$${\displaystyle \mathbb {id} }$${\displaystyle f\in \Sigma _{n}}$${\displaystyle i_{1},i_{2},\ldots ,i_{n}\in \mathbb {id} }$${\displaystyle f(i_{1},i_{2},\ldots ,i_{n})}$

จากนั้น กราฟeจะแสดงคลาสสมมูลของโหนด e โดยใช้โครงสร้างข้อมูลต่อไปนี้: ^{[ 1 ]}

• โครงสร้างยูเนียน-ฟินด์ที่แสดงถึงคลาสสมมูลของรหัส e-class พร้อมด้วยการดำเนินการตามปกติ, และรหัส e-class เป็นแบบมาตรฐานหาก; โหนด e เป็นแบบมาตรฐานหากแต่ละโหนดเป็นแบบมาตรฐาน ( ใน)${\displaystyle U}$${\displaystyle \mathrm {ค้นหา} }$${\displaystyle \mathrm {เพิ่ม} }$${\displaystyle \mathrm {ผสาน} }$${\displaystyle e}$${\displaystyle \mathrm {find} (U,e)=e}$${\displaystyle f(i_{1},\ldots ,i_{n})}$${\displaystyle i_{j}}$${\displaystyle j}$${\displaystyle 1,\ldots ,n}$
• การเชื่อมโยงรหัส e-class กับชุดของ e-node ซึ่งเรียกว่าe-classประกอบด้วย
  • แฮชคอน (เช่น การจับคู่) จากอีโหนดไปยังอีคลาส ID และ${\displaystyle H}$
  • แผนที่e-class ที่แมป ID e-class กับ e-class โดยที่ID ที่เทียบเท่ากันจะถูกแมปไปยังชุด e-node เดียวกัน:${\displaystyle M}$${\displaystyle M}$${\displaystyle \forall i,j\in \mathbb {id} ,M[i]=M[j]\Leftrightarrow \mathrm {find} (U,i)=\mathrm {find} (U,j)}$

นอกจากโครงสร้างข้างต้นแล้ว กราฟ e ที่ถูกต้องยังสอดคล้องกับค่าคงที่ของโครงสร้างข้อมูลหลายประการ[ 2 ^{]โหนดe}สองโหนดจะเทียบเท่ากันหากอยู่ในคลาส e เดียวกัน ค่าคง ที่ความสอดคล้องระบุว่ากราฟ e ต้องรับประกันว่าความเทียบเท่าจะปิดภายใต้ความสอดคล้องโดยที่โหนด e สองโหนดจะสอดคล้องกันเมื่อ ค่าคงที่ แฮชคอนระบุว่าแฮชคอนจะแมปโหนด e มาตรฐานไปยัง ID คลาส e ของโหนดนั้น ${\displaystyle f(i_{1},\ldots ,i_{n}),f(j_{1},\ldots ,j_{n})}$${\displaystyle \mathrm {find} (U,i_{k})=\mathrm {find} (U,j_{k}),k\in \{1,\ldots ,n\}}$

กราฟ E เปิดเผยตัวห่อหุ้มรอบ การดำเนินการ , , และจากการค้นหาแบบยูเนียนที่รักษาคุณสมบัติคงที่ของกราฟ E การดำเนินการสุดท้ายคือการจับคู่แบบ E ซึ่งจะอธิบายไว้ด้านล่าง ${\displaystyle \mathrm {เพิ่ม} }$${\displaystyle \mathrm {ค้นหา} }$${\displaystyle \mathrm {ผสาน} }$

นอกจากนี้ กราฟ e-graph ยังสามารถกำหนดได้ในรูปของกราฟสองส่วน โดยที่ ${\displaystyle G=(N\uplus \mathrm {id} ,E)}$

• ${\displaystyle \mathrm {id} }$คือชุดของรหัส e-class (ดังที่กล่าวมาข้างต้น)
• ${\displaystyle N}$คือเซตของอี-โหนด และ
• ${\displaystyle E\subseteq (\mathrm {id} \times N)\cup (N\times \mathrm {id} )}$คือเซตของเส้นขอบที่มีทิศทาง

มีขอบที่มีทิศทางจากแต่ละคลาส e ไปยังสมาชิกแต่ละคลาส และจากแต่ละโหนด e ไปยังลูกแต่ละโหนด^{[ 3 ]}

ให้เป็นเซตของตัวแปร และให้เป็นเซตที่เล็กที่สุดที่รวมสัญลักษณ์ฟังก์ชันศูนย์อาร์กิวเมนต์ (เรียกอีกอย่างว่าค่าคงที่ ) รวมตัวแปร และปิดภายใต้การประยุกต์ใช้สัญลักษณ์ฟังก์ชัน กล่าวอีกนัยหนึ่งคือเซตที่เล็กที่สุดที่, , และเมื่อและแล้วเทอมที่มีตัวแปรเรียกว่ารูปแบบ เทอมที่ไม่มีตัวแปรเรียกว่า พื้นฐาน${\displaystyle V}$${\displaystyle \mathrm {Term} (\Sigma ,V)}$${\displaystyle \mathrm {Term} (\Sigma ,V)}$${\displaystyle V\subset \mathrm {Term} (\Sigma ,V)}$${\displaystyle \Sigma _{0}\subset \mathrm {Term} (\Sigma ,V)}$${\displaystyle x_{1},\ldots ,x_{n}\in \mathrm {Term} (\Sigma ,V)}$${\displaystyle f\in \Sigma _{n}}$${\displaystyle f(x_{1},\ldots ,x_{n})\in \mathrm {Term} (\Sigma ,V)}$

กราฟ e แทนเทอมพื้นฐาน ได้ก็ต่อ เมื่อคลาส e คลาสใดคลาสหนึ่งของกราฟนั้นแทนเทอมพื้นฐานได้คลาส e แทนเทอมพื้นฐานได้ก็ต่อเมื่อโหนด e บางโหนด แทนเทอมพื้นฐาน ได้ โหนด e แทนเทอมพื้นฐานได้ ก็ต่อ เมื่อและแต่ละคลาส e แทนเทอมพื้นฐาน( ใน) ${\displaystyle E}$${\displaystyle t\in \mathrm {Term} (\Sigma ,\emptyset )}$${\displaystyle t}$${\displaystyle C}$${\displaystyle t}$${\displaystyle f(i_{1},\ldots ,i_{n})\in C}$${\displaystyle f(i_{1},\ldots ,i_{n})\in C}$${\displaystyle g(j_{1},\ldots ,j_{n})}$${\displaystyle f=g}$${\displaystyle M[i_{k}]}$${\displaystyle j_{k}}$${\displaystyle k}$${\displaystyle 1,\ldots ,n}$

การจับคู่แบบ eเป็นการดำเนินการที่รับรูปแบบและกราฟ e และให้ผลลัพธ์เป็นคู่ทั้งหมดโดยที่เป็นการแมปการแทนที่ตัวแปรในไปยังรหัสคลาส e และเป็นรหัสคลาส e ที่เทอมนั้นแสดงด้วยมีอัลกอริทึมการจับคู่แบบ e ที่เป็นที่รู้จักหลายแบบ^{[ 4 ] [ 5 ]} อัลกอริทึม การจับคู่แบบ e เชิงสัมพันธ์นั้นขึ้นอยู่กับการเชื่อมต่อที่เหมาะสมที่สุดในกรณีที่เลวร้ายที่สุดและเหมาะสมที่สุดในกรณีที่เลวร้ายที่สุด^{[ 6 ]}${\displaystyle p\in \mathrm {Term} (\Sigma ,V)}$${\displaystyle E}$${\displaystyle (\sigma ,C)}$${\displaystyle \sigma \subset V\times \mathbb {id} }$${\displaystyle p}$${\displaystyle C\in \mathbb {id} }$${\displaystyle \sigma (p)}$${\displaystyle C}$

เมื่อกำหนดคลาส e และฟังก์ชันต้นทุนที่แมปสัญลักษณ์ฟังก์ชันแต่ละตัวไปยังจำนวนธรรมชาติ ปัญหาการสกัดคือการหาเทอมพื้นฐานที่มีต้นทุนรวมน้อยที่สุดซึ่งแสดงโดยคลาส e ที่กำหนด ปัญหานี้เป็นปัญหาNP-hard [ ^{7 ] นอกจาก} นี้ยังไม่มีอัลกอริทึมการประมาณค่าปัจจัยคงที่สำหรับปัญหานี้ ซึ่งสามารถแสดงได้โดยการลดจากปัญหาการครอบคลุมเซตอย่างไรก็ตาม สำหรับกราฟที่มีtreewidth ที่จำกัด จะมีอัลกอริทึม ที่จัดการได้ ในเวลาเชิงเส้นและพารามิเตอร์คงที่^{[ 8 ]}${\displaystyle \Sigma }$

• กราฟ e ที่มี สมการ nสมการสามารถสร้างได้ในเวลา O( n log n ) ^{[ 9 ]}

การอิ่มตัวของความเท่าเทียมกันเป็นเทคนิคสำหรับการสร้างคอมไพเลอร์ที่ปรับให้เหมาะสมโดยใช้ e-graph ^{[ 10 ]}โดยจะดำเนินการโดยใช้ชุดการเขียนใหม่โดยใช้ e-matching จนกว่า e-graph จะอิ่มตัว หมดเวลา ถึงขีดจำกัดขนาดของ e-graph จำนวนรอบที่กำหนดเกิน หรือถึงเงื่อนไขการหยุดอื่นๆ หลังจากเขียนใหม่แล้ว จะมีการดึงเทอมที่เหมาะสมที่สุดจาก e-graph ตามฟังก์ชันต้นทุนบางอย่าง ซึ่งโดยปกติจะเกี่ยวข้องกับ ขนาด ASTหรือการพิจารณาประสิทธิภาพ

กราฟ E ใช้ในการพิสูจน์ทฤษฎีบทอัตโนมัติเป็นส่วนสำคัญของตัวแก้ปัญหา SMT สมัยใหม่ เช่นZ3 ^{[ 11 ]}และCVC4ซึ่งใช้ในการตัดสินทฤษฎีที่ว่างเปล่าโดยการคำนวณการปิดความสอดคล้องของชุดความเท่าเทียมกัน และการจับคู่ E ใช้ในการสร้างตัวบ่งปริมาณ^{[ 12 ]}ใน ตัวแก้ปัญหาแบบ DPLL(T)ที่ใช้การเรียนรู้ข้อความที่ขับเคลื่อนด้วยความขัดแย้ง (หรือที่เรียกว่าการย้อนกลับแบบไม่เรียงลำดับเวลา) กราฟ E จะถูกขยายเพื่อสร้างใบรับรองการพิสูจน์^{[ 13 ]}กราฟ E ยังถูกใช้ในตัวพิสูจน์ทฤษฎีบท Simplify ของESC /Java อีกด้วย ^{[ 14 ]}

การอิ่มตัวของความเท่าเทียมกันถูกนำมาใช้ในคอมไพเลอร์ที่ปรับแต่งเฉพาะทาง[ 15 ^{]เช่นสำหรับ}การเรียนรู้เชิงลึก^{[ 16 ]}พีชคณิตเชิงเส้น^{[ 17 ]}และการแปลงเวกเตอร์อัตโนมัติสำหรับตัวประมวลผลสัญญาณดิจิทัล^{[ 18 ]}การอิ่มตัวของความเท่าเทียมกันยังถูกนำมาใช้สำหรับการตรวจสอบความถูกต้องของการแปลที่ใช้กับชุดเครื่องมือLLVM ^{[ 19 ]}

กราฟ E ได้ถูกนำไปใช้กับปัญหาต่างๆ ในการวิเคราะห์โปรแกรมรวมถึงการฟัซซิ่ง^{[ 20 ]}การตีความเชิงนามธรรม^{[ 21 ]}และการเรียนรู้ไลบรารี^{[ 22 ]}

• โครงการไข่
• สมุดบันทึก Colab ที่อธิบายเกี่ยวกับกราฟอิเล็กทรอนิกส์