کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
423661 685273 2008 15 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic
چکیده انگلیسی

In a CAV'05 paper [Meir, O. and O. Strichman, Yet another decision procedure for equality logic, in: K. Etessami and S. Rajamani, editors, Proc. 17th Intl. Conference on Computer Aided Verification (CAV'05), Lect. Notes in Comp. Sci. 3576 (2005), pp. 307–320] we introduced a new decision procedure for Equality Logic: each equality predicate is encoded with a Boolean variable, and then a set of transitivity constraints are added to compensate for the loss of transitivity of equality. The constraints are derived by analyzing Contradictory Cycles: cycles in the equality graph with exactly one disequality. Such a cycle is called constrained under a formula ϕ if ϕ is not satisfied with an assignment of true to all equality edges and false to the disequality edge. While we proved in [Meir, O. and O. Strichman, Yet another decision procedure for equality logic, in: K. Etessami and S. Rajamani, editors, Proc. 17th Intl. Conference on Computer Aided Verification (CAV'05), Lect. Notes in Comp. Sci. 3576 (2005), pp. 307–320] that it is sufficient to constrain all simple contradictory cycles, we left open the question of how to find the necessary constraints in polynomial time. Instead, we showed two possible compromises: an exponential algorithm, or, alternatively, a polynomial approximation that constrains all contradictory cycles rather than only the simple ones. In this article we show a polynomial algorithm that constrains only the simple contradictory cycles.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 198, Issue 2, 6 May 2008, Pages 3-17