-
simulating circuit-level simplifications on cnf
جزئیات بیشتر مقاله- تاریخ ارائه: 1392/07/24
- تاریخ انتشار در تی پی بین: 1392/07/24
- تعداد بازدید: 1128
- تعداد پرسش و پاسخ ها: 0
- شماره تماس دبیرخانه رویداد: -
boolean satisfiability (sat) and its extensions have become a core technology in many application domains, such as planning and formal verification, and continue finding various new application domains today. the sat-based approach divides into three steps: encoding, preprocessing, and search. it is often argued that by encoding arbitrary boolean formulas in conjunctive normal form (cnf), structural properties of the original problem are not reflected in the cnf. this should result in the fact that cnf-level preprocessing and sat solver techniques have an inherent disadvantage compared to related techniques applicable on the level of more structural sat instance representations such as boolean circuits. motivated by this, various simplification techniques and intricate cnf encodings for circuit-level sat instance representations have been proposed. on the other hand, based on the highly efficient cnf-level clause learning sat solvers, there is also strong support for the claim that cnf is sufficient as an input format for sat solvers. in this work we study the effect of cnf-level simplification techniques, focusing on satelite-style variable elimination (ve) and what we call blocked clause elimination (bce). we show that bce is surprisingly effective both in theory and in practice on cnf formulas resulting from a standard cnf encoding for circuits: without explicit knowledge of the underlying circuit structure, it achieves the same level of simplification as a combination of circuit-level simplifications and previously suggested polarity-based cnf encodings. we also show that ve can achieve many of the same effects as bce, but not all. on the other hand, it turns out that ve and bce are indeed partially orthogonal techniques. we also study the practical effects of combining bce and ve for reducing the size of formulas and on the running times of state-of-the-art sat solvers. furthermore, we address the problem of how to construct original witnesses to satisfiable cnf formulas when applying a combination of bce and ve.
مقالات جدیدترین رویدادها
-
استفاده از تحلیل اهمیت-عملکرد در ارائه الگوی مدیریت خلاقیت سازمانی و ارائه راهکار جهت بهبود
-
بررسی تاثیر ارزش وجوه نقد مازاد بر ساختار سرمایه شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر سطح افشای ریسک بر قرارداد بدهی شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر رتبه بندی اعتباری مبتنی بر مدل امتیاز بازار نوظهور بر نقد شوندگی سهام با تأکید بر خصوصی سازی شرکت ها
-
تأثیر آمیخته بازاریابی پوشاک ایرانی بر تصویر ذهنی مشتری پوشاک ایرانی (هاکوپیان)
-
بررسی تاثیر ابعاد قطعات بتنی در تعیین سرعت امواج فراصوتی و تاثیرآن در تخمین مقاومت فشاری بتن سخت شده
-
تحلیل حدی کران بالا ظرفیت بیرون کشیدکی لرزه ای مهار نواری افقی بر مبنای روش شبه دینامیکی
-
بهینه سازی هزینه و زمان در پروژه های ساخت
-
بررسی کمی و کیفی گونه جنگل کاری شده گز (.tamarix aphylla l) در حاشیه دریاچه ارومیه (مطالعه موردی: جبل کندی ارومیه)
-
مقایسه شتاب نگاشت های مقیاس شده و مصنوعی بر اساس طیف لرزه ای طراحی آیین نامه 2800
مقالات جدیدترین ژورنال ها
-
مدیریت و بررسی افسردگی دانش آموزان دختر مقطع متوسطه دوم در دروان کرونا در شهرستان دزفول
-
مدیریت و بررسی خرد سیاسی در اندیشه ی فردوسی در ادب ایران
-
واکاوی و مدیریت توصیفی قلمدان(جاکلیدی)ضریح در موزه آستان قدس رضوی
-
بررسی تاثیر خلاقیت، دانش و انگیزه کارکنان بر پیشنهادات نوآورانه کارکنان ( مورد مطالعه: هتل های 3 و 4 ستاره استان کرمان)
-
بررسی تاثیر کیفیت سیستم های اطلاعاتی بر تصمیم گیری موفق در شرکتهای تولیدی استان اصفهان (مورد مطالعه: مدیران شرکتهای تولیدی استان اصفهان)
-
تأثیر آموزش مهارت خودافشایی بر کاهش افسردگی دانش آموزان دختر مقطع متوسطه اول
-
مداخله ی آموزشی مبتنی بر مذهب بر نشانگان افسردگی زنان متاهل مراجعه کننده به مراکز فرهنگی شهر بابل
-
بررسی اثر دارویی استویا (stevia rebaudiana) در کنترل دیابت نوع دوم
-
بهره گیری از تکنیک خوشه بندی در ارتقای کارایی مدیریت ریسک در شرکتهای بیمه
-
evaluation the moisture susceptibility of asphalt mixtures containing demolished concrete waste materials
سوال خود را در مورد این مقاله مطرح نمایید :