-
simulating circuit-level simplifications on cnf
جزئیات بیشتر مقاله- تاریخ ارائه: 1392/07/24
- تاریخ انتشار در تی پی بین: 1392/07/24
- تعداد بازدید: 1130
- تعداد پرسش و پاسخ ها: 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.
مقالات جدیدترین رویدادها
-
استفاده از تحلیل اهمیت-عملکرد در ارائه الگوی مدیریت خلاقیت سازمانی و ارائه راهکار جهت بهبود
-
بررسی تاثیر ارزش وجوه نقد مازاد بر ساختار سرمایه شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر سطح افشای ریسک بر قرارداد بدهی شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر رتبه بندی اعتباری مبتنی بر مدل امتیاز بازار نوظهور بر نقد شوندگی سهام با تأکید بر خصوصی سازی شرکت ها
-
تأثیر آمیخته بازاریابی پوشاک ایرانی بر تصویر ذهنی مشتری پوشاک ایرانی (هاکوپیان)
-
تحلیلی ساختاری بر استراتژی توسعه شهری مطالعه موردی: شهر بم
-
طرح جامع نظام پرداخت: پیش نیاز بانکداری الکترونیک، پول و تجارت الکترونیک (عملکرد و چالش ها)
-
مدل سازی اجزای محدود نمونه مکعبی بتن مزو مقیاس با استفاده از پردازش تصاویر سیتی اسکن
-
evaluation of seismic behavior of reinforced concrete frames with buckling restrained braces (brb) in zigzag configuration in high-risk seismic zone
-
on-line optimization of fedbatch bioreactors by adaptive extremum seeking control
مقالات جدیدترین ژورنال ها
-
مدیریت و بررسی افسردگی دانش آموزان دختر مقطع متوسطه دوم در دروان کرونا در شهرستان دزفول
-
مدیریت و بررسی خرد سیاسی در اندیشه ی فردوسی در ادب ایران
-
واکاوی و مدیریت توصیفی قلمدان(جاکلیدی)ضریح در موزه آستان قدس رضوی
-
بررسی تاثیر خلاقیت، دانش و انگیزه کارکنان بر پیشنهادات نوآورانه کارکنان ( مورد مطالعه: هتل های 3 و 4 ستاره استان کرمان)
-
بررسی تاثیر کیفیت سیستم های اطلاعاتی بر تصمیم گیری موفق در شرکتهای تولیدی استان اصفهان (مورد مطالعه: مدیران شرکتهای تولیدی استان اصفهان)
-
بررسی تاثیر فشارهای اجتماعی، تعهد و ویژگی های شخصیتی بر قضاوت حسابرسان
-
توسعه و نهادینه کردن عدالت آموزشی و تربیتی با استفاده از ارتباطات سیار سلولی نسل پنجم بر اساس اهداف راهبرد های کلان تحول بنیادین آموزش و پرورش
-
نقش اخلاق حسابداری در جلب اعتماد مشتریان نمایندگی گروه خودرو سازی سایپا در استان اردبیل
-
بررسی نقش انعطاف پذیری مالی در توسعه پایدار بر عملکرد شرکت در طول بحران بیماری کوید 19 با توجه به دارایی های مشهود (مطالعه موردی: شرکت های پذیرفته شده در بورس اوراق بهادار تهران)
-
a hybrid of artificial neural networks and particle swarm optimization algorithm for inverse modeling of leakage in earth dams
سوال خود را در مورد این مقاله مطرح نمایید :