ورود به حساب

نام کاربری گذرواژه

گذرواژه را فراموش کردید؟ کلیک کنید

حساب کاربری ندارید؟ ساخت حساب

ساخت حساب کاربری

نام نام کاربری ایمیل شماره موبایل گذرواژه

برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید


09117307688
09117179751

در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید

دسترسی نامحدود

برای کاربرانی که ثبت نام کرده اند

ضمانت بازگشت وجه

درصورت عدم همخوانی توضیحات با کتاب

پشتیبانی

از ساعت 7 صبح تا 10 شب

دانلود کتاب Handbook of Satisfiability

دانلود کتاب راهنمای رضایتمندی

Handbook of Satisfiability

مشخصات کتاب

Handbook of Satisfiability

ویرایش:  
نویسندگان: , , , ,   
سری: Frontiers in Artificial Intelligence and Applications 185 
ISBN (شابک) : 1586039296, 160750376X 
ناشر: IOS Press 
سال نشر: 2009 
تعداد صفحات: 981 
زبان: English 
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) 
حجم فایل: 5 مگابایت

قیمت کتاب (تومان) : 35,000



ثبت امتیاز به این کتاب

میانگین امتیاز به این کتاب :
       تعداد امتیاز دهندگان : 9


در صورت تبدیل فایل کتاب Handbook of Satisfiability به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.

توجه داشته باشید کتاب راهنمای رضایتمندی نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.


توضیحاتی در مورد کتاب راهنمای رضایتمندی

موضوعات مرتبط با رضایتمندی (SAT) محققان را از رشته های مختلف جذب کرده است: منطق، حوزه های کاربردی مانند برنامه ریزی، زمان بندی، تحقیق در عملیات و بهینه سازی ترکیبی، اما همچنین مسائل نظری در موضوع پیچیدگی و موارد دیگر، همه آنها از طریق SAT به هم متصل می شوند. علاقه شخصی من به SAT از حل واقعی ناشی می شود: افزایش قدرت حل کننده های مدرن SAT در 15 سال گذشته فوق العاده بوده است. این به فناوری کلیدی در تأیید خودکار سخت افزار و نرم افزار رایانه تبدیل شده است. بررسی مدل محدود (BMC) سخت افزار کامپیوتر در حال حاضر احتمالاً پرکاربردترین تکنیک بررسی مدل است. نمونه‌های متقابلی که می‌یابد فقط نمونه‌های رضایت‌بخش یک فرمول بولی هستند که با باز کردن یک مدار ترتیبی به عمق ثابت و مشخصات آن در منطق زمانی خطی به دست می‌آیند. گسترش بررسی مدل به راستی‌آزمایی نرم‌افزار مشکلی بسیار دشوارتر در مرز تحقیقات کنونی است. یکی از رویکردهای امیدوارکننده برای زبان‌هایی مانند C با اعداد صحیح با طول کلمه محدود، استفاده از همان ایده در BMC اما با یک روش تصمیم‌گیری برای تئوری بردارهای بیت به جای SAT است. تمام مراحل تصمیم گیری برای بردارهای بیت که من با آنها آشنا هستم، در نهایت از یک حل کننده سریع SAT برای مدیریت فرمول های پیچیده استفاده می کنند. روش‌های تصمیم‌گیری برای نظریه‌های پیچیده‌تر، مانند محاسبات واقعی و صحیح خطی، نیز در تأیید برنامه استفاده می‌شوند. اکثر آنها از حل کننده های قدرتمند SAT به صورت اساسی استفاده می کنند. واضح است که حل کارآمد SAT یک فناوری کلیدی برای علم کامپیوتر قرن بیست و یکم است. من انتظار دارم که این مجموعه مقالات در مورد تمام جنبه های نظری و عملی حل SAT برای دانشجویان و محققان بسیار مفید باشد و منجر به پیشرفت های بیشتر در این زمینه شود.'
ادموند کلارک (برنده جایزه تورینگ 2007 و A.M. پروفسور علوم کامپیوتر دانشگاه FORE Systems و استاد مهندسی برق و کامپیوتر در دانشگاه کارنگی ملون)

IOS Press یک ناشر بین المللی علمی، فنی و پزشکی کتاب های با کیفیت بالا برای دانشگاهیان، دانشمندان و متخصصان در همه زمینه ها است.

برخی از حوزه هایی که ما در آنها منتشر می کنیم:

-زیست پزشکی
-انکولوژی
-هوش مصنوعی
-پایگاه های اطلاعاتی و سیستم های اطلاعاتی
-مهندسی دریایی
-نانو فناوری
- مهندسی زمین
-همه جنبه های فیزیک
-حاکمیت الکترونیکی-تجارت الکترونیک
-اقتصاد دانش
-مطالعات شهری
-کنترل تسلیحات
- درک و پاسخ به تروریسم
- انفورماتیک پزشکی
- علوم کامپیوتر


توضیحاتی درمورد کتاب به خارجی

'Satisfiability (SAT) related topics have attracted researchers from various disciplines: logic, applied areas such as planning, scheduling, operations research and combinatorial optimization, but also theoretical issues on the theme of complexity and much more, they all are connected through SAT. My personal interest in SAT stems from actual solving: The increase in power of modern SAT solvers over the past 15 years has been phenomenal. It has become the key enabling technology in automated verification of both computer hardware and software. Bounded Model Checking (BMC) of computer hardware is now probably the most widely used model checking technique. The counterexamples that it finds are just satisfying instances of a Boolean formula obtained by unwinding to some fixed depth a sequential circuit and its specification in linear temporal logic. Extending model checking to software verification is a much more difficult problem on the frontier of current research. One promising approach for languages like C with finite word-length integers is to use the same idea as in BMC but with a decision procedure for the theory of bit-vectors instead of SAT. All decision procedures for bit-vectors that I am familiar with ultimately make use of a fast SAT solver to handle complex formulas. Decision procedures for more complicated theories, like linear real and integer arithmetic, are also used in program verification. Most of them use powerful SAT solvers in an essential way. Clearly, efficient SAT solving is a key technology for 21st century computer science. I expect this collection of papers on all theoretical and practical aspects of SAT solving will be extremely useful to both students and researchers and will lead to many further advances in the field.'
Edmund Clarke (Winner of the 2007 A.M. Turing Award & FORE Systems University Professor of Computer Science and Professor of Electrical and Computer Engineering at Carnegie Mellon University)

IOS Press is an international science, technical and medical publisher of high-quality books for academics, scientists, and professionals in all fields.

Some of the areas we publish in:

-Biomedicine
-Oncology
-Artificial intelligence
-Databases and information systems
-Maritime engineering
-Nanotechnology
-Geoengineering
-All aspects of physics
-E-governance -E-commerce
-The knowledge economy
-Urban studies
-Arms control
- Understanding and responding to terrorism
- Medical informatics
- Computer Sciences



فهرست مطالب

Content: Title page
 Contents
 Part I. Theory and Algorithms
 Chapter 1. A History of Satisfiability
 1.1 Preface: the concept of satisfiability
 1.2 The ancients
 1.3 The medieval period
 1.4 The renaissance
 1.5 The first logic machine
 1.6 Boolean algebra
 1.7 Frege, logicism, and quantification logic
 1.8 Russell and Whitehead
 1.9 G""odel's incompleteness theorem
 1.10 Effective process and recursive functions
 1.11 Herbrand's theorem
 1.12 Model theory and Satisfiability
 1.13 Completeness of first-order logic
 1.14 Application of logic to circuits
 1.15 Resolution 1.16 The complexity or resolution1.17 Refinement of Resolution-Based SAT Solvers
 1.18 Upper bounds
 1.19 Classes of easy expressions
 1.20 Binary Decision Diagrams
 1.21 Probabilistic analysis: SAT algorithms
 1.22 Probabilistic analysis: thresholds
 1.23 Stochastic Local Search
 1.24 Maximum Satisfiability
 1.25 Nonlinear formulations
 1.26 Pseudo-Boolean Forms
 1.27 Quantified Boolean formulas
 References
 Chapter 2. CNF Encodings
 2.1 Introduction
 2.2 Transformation to CNF
 2.3 Case studies
 2.4 Desirable properties of CNF encodings
 2.5 Conclusion
 References Chapter 3. Complete Algorithms3.1 Introduction
 3.2 Technical Preliminaries
 3.3 Satisfiability by Existential Quantification
 3.4 Satisfiability by Inference Rules
 3.5 Satisfiability by Search: The DPLL Algorithm
 3.6 Satisfiability by Combining Search and Inference
 3.7 Conclusions
 References
 Chapter 4. CDCL Solvers
 4.1 Introduction
 4.2 Notation
 4.3 Organization of CDCL Solvers
 4.4 Conflict Analysis
 4.5 Modern CDCL Solvers
 4.6 Bibliographical and Historical Notes
 References
 Chapter 5. Look-Ahead Based SAT Solvers
 5.1 Introduction
 5.2 General and Historical Overview 5.3 Heuristics5.4 Additional Reasoning
 5.5 Eager Data-Structures
 References
 Chapter 6. Incomplete Algorithms
 6.1 Greedy Search and Focused Random Walk
 6.2 Extensions of the Basic Local Search Method
 6.3 Discrete Lagrangian Methods
 6.4 The Phase Transition Phenomenon in Random k-SAT
 6.5 A New Technique for Random k-SAT: Survey Propagation
 6.6 Conclusion
 References
 Chapter 7. Fundaments of Branching Heuristics
 7.1 Introduction
 7.2 A general framework for branching algorithms
 7.3 Branching tuples and the canonical projection
 7.4 Estimating tree sizes 7.5 Axiomatising the canonical order on branching tuples7.6 Alternative projections for restricted branching width
 7.7 How to select distances and measures
 7.8 Optimising distance functions
 7.9 The order of branches
 7.10 Beyond clause-sets
 7.11 Conclusion and outlook
 References
 Chapter 8. Random Satisfiability
 8.1 Introduction
 8.2 The State of the Art
 8.3 Random MAX k-SAT
 8.4 Physical Predictions for Solution-space Geometry
 8.5 The Role of the Second Moment Method
 8.6 Generative models
 8.7 Algorithms
 8.8 Belief/Survey Propagation and the Algorithmic Barrier




نظرات کاربران

تمامی حقوق معنوی و مادی وبسایت متعلق به اینترنشنال لایبرری می باشد
نماد اعتماد الکترونیکی