词条 | Implication graph |
释义 |
In mathematical logic, an implication graph is a skew-symmetric directed graph G = (V, E) composed of vertex set V and directed edge set E. Each vertex in V represents the truth status of a Boolean literal, and each directed edge from vertex u to vertex v represents the material implication "If the literal u is true then the literal v is also true". Implication graphs were originally used for analyzing complex Boolean expressions. ApplicationsA 2-satisfiability instance in conjunctive normal form can be transformed into an implication graph by replacing each of its disjunctions by a pair of implications. For example, the statement can be rewritten as the pair . An instance is satisfiable if and only if no literal and its negation belong to the same strongly connected component of its implication graph; this characterization can be used to solve 2-satisfiability instances in linear time.[1] In CDCL SAT-solvers, unit propagation can be naturally associated with an implication graph that captures all possible ways of deriving all implied literals from decision literals,[2] which is then used for clause learning. References1. ^{{cite journal|author = Aspvall, Bengt; Plass, Michael F.; Tarjan, Robert E.|title = A linear-time algorithm for testing the truth of certain quantified boolean formulas|journal = Information Processing Letters | volume = 8 | issue = 3 | pages = 121–123|year = 1979|doi = 10.1016/0020-0190(79)90002-4}} 2. ^{{cite conference|author1=Paul Beame |author2=Henry Kautz |author3=Ashish Sabharwal |title = Understanding the Power of Clause Learning| conference = IJCAI | pages = 1194–1201|year = 2003|url=https://www.cs.rochester.edu/u/kautz/papers/learnIjcai.pdf}} 4 : Boolean algebra|Application-specific graphs|Directed graphs|Graph families |
随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识,基本涵盖了大多数领域的百科知识,是一部内容自由、开放的电子版国际百科全书。