Combinatorial Search_ From Algorithms to Systems [Hamadi 2013-11-12].pdf

(3468 KB) Pobierz
Youssef Hamadi
Combinatorial
Search: From
Algorithms to
Systems
Combinatorial Search: From Algorithms to Systems
Youssef Hamadi
Combinatorial Search:
From Algorithms to Systems
Youssef Hamadi
Microsoft Research Cambridge
Cambridge, UK
ISBN 978-3-642-41481-7
ISBN 978-3-642-41482-4 (eBook)
DOI 10.1007/978-3-642-41482-4
Springer Heidelberg New York Dordrecht London
Library of Congress Control Number: 2013953692
© Springer-Verlag Berlin Heidelberg 2013
This work is subject to copyright. All rights are reserved by the Publisher, whether the whole or part of
the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation,
broadcasting, reproduction on microfilms or in any other physical way, and transmission or information
storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology
now known or hereafter developed. Exempted from this legal reservation are brief excerpts in connection
with reviews or scholarly analysis or material supplied specifically for the purpose of being entered
and executed on a computer system, for exclusive use by the purchaser of the work. Duplication of
this publication or parts thereof is permitted only under the provisions of the Copyright Law of the
Publisher’s location, in its current version, and permission for use must always be obtained from Springer.
Permissions for use may be obtained through RightsLink at the Copyright Clearance Center. Violations
are liable to prosecution under the respective Copyright Law.
The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication
does not imply, even in the absence of a specific statement, that such names are exempt from the relevant
protective laws and regulations and therefore free for general use.
While the advice and information in this book are believed to be true and accurate at the date of pub-
lication, neither the authors nor the editors nor the publisher can accept any legal responsibility for any
errors or omissions that may be made. The publisher makes no warranty, express or implied, with respect
to the material contained herein.
Printed on acid-free paper
Springer is part of Springer Science+Business Media (www.springer.com)
Foreword
To solve a problem as efficiently as possible, a user selects a type of solver (MIP, CP,
SAT), then defines a model and selects a method of resolution. The model expresses
the problem in a way understandable for the solver. The method of resolution can be
complete (one is certain not to miss solutions) or incomplete (it uses a heuristic, i.e.,
a method that favors the chances of finding a solution but offers no completeness
guarantee).
Since solvers exist, researchers try to simplify the task of the end user, helping
her in these keys steps: the creation of the model, and the finding of a method of
resolution. In this book, Youssef Hamadi helps the user on the second point by
presenting ways to automatically select and adjust resolution strategies.
This book proposes several methods for both SAT and CP solvers. Firstly, the au-
thor demonstrates the benefit of parallelism through the duplication of search strate-
gies. In the best case, this can provide super linear speed up in the resolution process.
In most cases, this results in a more robust resolution method, to the point that such
a solver is never beaten by a solver using the best method. The solver ManySAT,
co-developed by Mr. Hamadi, is based on this idea and has won numerous prizes in
SAT competitions. Its fame goes far beyond the SAT solving domain and this line
of work is now a reference for the domain.
Any resolution method must be guided by the user through the definition of a
resolution strategy which typically defines the next decision to be made, i.e., which
variable must be assigned to which value? This book considers the automatic learn-
ing of the parameters of resolution strategies. It shows how to extract knowledge
from the information available during search. The difficulty is to determine the rel-
evant information and decide how they can be exploited. A particularly novel ap-
proach is proposed. It considers the successive resolutions of similar problems to
gradually build an efficient strategy.
This is followed by the presentation of Autonomous Search, a major contribution
of the book. In that formalism, the solver determines itself the best way to find solu-
tions. This is a very important topic, which has often been approached too quickly,
and which is finally well defined in this book. Many researchers should benefit from
this contribution.
v

Plik z chomika:

Inne pliki z tego folderu:

Inne foldery tego chomika:

Zgłoś jeśli naruszono regulamin