Clause shortening combined with pruning yields a new upper bound for deterministic SAT algorithms

Evgeny Dantsin, Edward A. Hirsch, Alexander Wolpert

פרסום מחקרי: פרק בספר / בדוח / בכנספרסום בספר כנסביקורת עמיתים

12 ציטוטים ‏(Scopus)

תקציר

We give a deterministic algorithm for testing satisfiability of Boolean formulas in conjunctive normal form with no restriction on clause length. Its upper bound on the worst-case running time matches the best known upper bound for randomized satisfiability-testing algorithms [6]. In comparison with the randomized algorithm in [6], our deterministic algorithm is simpler and more intuitive.

שפה מקוריתאנגלית
כותר פרסום המארחAlgorithms and Complexity - 6th Italian Conference, CIAC 2006, Proceedings
עמודים60-68
מספר עמודים9
מזהי עצם דיגיטלי (DOIs)
סטטוס פרסוםפורסם - 2006
פורסם באופן חיצוניכן
אירוע6th Italian Conference on Algorithms and Complexity, CIAC 2006 - Rome, איטליה
משך הזמן: 29 מאי 200631 מאי 2006

סדרות פרסומים

שםLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
כרך3998 LNCS
ISSN (מודפס)0302-9743
ISSN (אלקטרוני)1611-3349

כנס

כנס6th Italian Conference on Algorithms and Complexity, CIAC 2006
מדינה/אזוראיטליה
עירRome
תקופה29/05/0631/05/06

טביעת אצבע

להלן מוצגים תחומי המחקר של הפרסום 'Clause shortening combined with pruning yields a new upper bound for deterministic SAT algorithms'. יחד הם יוצרים טביעת אצבע ייחודית.

פורמט ציטוט ביבליוגרפי