Stochastische Lokale Suche bei SAT-Solvern

SAT 求解器中的随机局部搜索

• 批准号: 206226417
• 负责人: Professor Dr. Uwe Schöning
• 金额: --
• 依托单位: Institut für Theoretische Informatik (Theo)
• 依托单位国家: 德国
• 项目类别: Priority Programmes
• 财政年份: 2011
• 资助国家: 德国
• 起止时间: 2010-12-31 至 2013-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/206226417?language=en
• 关键词: Stochastische; Lokale; Suche; bei; SAT

In diesem Projekt wird die Algorithm Engineering Methode auf SAT-Solving angewandt, und zwar speziell auf solche SAT-Algorithmen, die auf dem Konzept der lokalen Suche beruhen. Die Ziele des Projekts gliedern sich in 3 Punkte: Zum ersten sollen effizientere SAT-Solver entwickelt und implementiert werden. Diese werden der internationalen Szene auf der SAT-Konferenz präsentiert bzw. bei dem SAT-Kontest 2013 eingereicht. Zweitens, die Lücke zwischen den bei Algorithmen-Experimenten beobachteten Laufzeiten und den theoretischen Analysen derartiger Algorithmen soll weiter geschlossen werden; und dies ebenso auf der praktischen wie auf der theoretischen Seite. Zum dritten, wegen des generischen Charakters des SAT-Problems als ein NP-vollständiges Problem, und ebenso, wegen des generischen Charakters der Lokale Such-Methode, sollen die erzielten Resultate es ermöglichen, auch auf andere Problemstellungen angewandt zu werden.

在本课题中，提出了一种求解SAT问题的算法工程方法，并给出了求解SAT问题的具体方法，以解决局部问题。该项目包含三个方面：首先要解决SAT-求解器的有效性和韦尔登。这些韦尔登的国际合作将在卫星会议上进行。在2013年SAT竞赛中。第二，通过实验研究和理论分析，可以得出更好的结论韦尔登，并将其应用于实践，正如应用于理论一样。因此，SAT问题的一般特征是一个NP-问题，而Lokale方法的一般特征，解决了这一问题的结果，也使问题的解决成为韦尔登。