東華大學圖書館 |

Language: English

Help

回圖書館首頁

手機版館藏查詢

Back

Switch To: Labeled | MARC Mode | ISBD

Linked to FindBook

Google Book

Amazon

博客來

Neural Guidance in Constraint Solvers.

Record Type:	Electronic resources : Monograph/item
Title/Author:	Neural Guidance in Constraint Solvers./
Author:	Lederman, Gil.
Published:	Ann Arbor : ProQuest Dissertations & Theses, : 2021,
Description:	133 p.
Notes:	Source: Dissertations Abstracts International, Volume: 83-03, Section: B.
Contained By:	Dissertations Abstracts International83-03B.
Subject:	Computer science. -
Online resource:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=28539783
ISBN:	9798535562810

Neural Guidance in Constraint Solvers.
Lederman, Gil.

Neural Guidance in Constraint Solvers. - Ann Arbor : ProQuest Dissertations & Theses, 2021 - 133 p.

Source: Dissertations Abstracts International, Volume: 83-03, Section: B.

Thesis (Ph.D.)--University of California, Berkeley, 2021.

This item must not be sold to any third party vendors.

Boolean Constraint Satisfaction Problems naturally arise in a variety of fields in Formal Methods and Artificial Intelligence. Constraint Solvers, the specialized software tools that solve them, are therefore a core enabling technology in industry and research. They are normally used as black-box components, applied to practical problems such as hardware and software verification, test generation, planning, synthesis and more. Based on classical algorithms that have been optimized over decades by researchers, there is a noticeable gap between Constraint Solvers and the technology of Deep Learning, which over the last decade found its way into countless domains, outperforming established domain-specific algorithms.This thesis aims to narrow this gap, and by using Deep Neural Networks, teach classical Constraint Solvers to "learn from experience''. The research I present in this thesis starts by addressing the challenge of representation, using a Graph Neural Networks based architecture to process propositional formulas as graphs. I will then show how to automatically learn a solver's branching heuristic by mapping it to a Markov Decision Process and training it using Deep Reinforcement Learning. I will present an implementation based on different two competitive solvers, and experiments showing automatically learned heuristics to outperform the state of the art in the two domains.

ISBN: 9798535562810Subjects--Topical Terms:

523869
Computer science.
Subjects--Index Terms:

Constraint solvers

Neural Guidance in Constraint Solvers.
LDR:02589nmm a2200397 4500 001 2348598
005 20220912135614.5
008 241004s2021 ||||||||||||||||| ||eng d
020 $a 9798535562810
035 $a (MiAaPQ)AAI28539783
035 $a AAI28539783
040 $a MiAaPQ $c MiAaPQ
100 1 $a Lederman, Gil. $3 3687963
245 1 0 $a Neural Guidance in Constraint Solvers.
260 1 $a Ann Arbor : $b ProQuest Dissertations & Theses, $c 2021
300 $a 133 p.
500 $a Source: Dissertations Abstracts International, Volume: 83-03, Section: B.
500 $a Advisor: Lee, Edward A.;Seshia, Sanjit A.
502 $a Thesis (Ph.D.)--University of California, Berkeley, 2021.
506 $a This item must not be sold to any third party vendors.
520 $a Boolean Constraint Satisfaction Problems naturally arise in a variety of fields in Formal Methods and Artificial Intelligence. Constraint Solvers, the specialized software tools that solve them, are therefore a core enabling technology in industry and research. They are normally used as black-box components, applied to practical problems such as hardware and software verification, test generation, planning, synthesis and more. Based on classical algorithms that have been optimized over decades by researchers, there is a noticeable gap between Constraint Solvers and the technology of Deep Learning, which over the last decade found its way into countless domains, outperforming established domain-specific algorithms.This thesis aims to narrow this gap, and by using Deep Neural Networks, teach classical Constraint Solvers to "learn from experience''. The research I present in this thesis starts by addressing the challenge of representation, using a Graph Neural Networks based architecture to process propositional formulas as graphs. I will then show how to automatically learn a solver's branching heuristic by mapping it to a Markov Decision Process and training it using Deep Reinforcement Learning. I will present an implementation based on different two competitive solvers, and experiments showing automatically learned heuristics to outperform the state of the art in the two domains.
590 $a School code: 0028.
650 4 $a Computer science. $3 523869
650 4 $a Software. $2 gtt. $3 619355
650 4 $a Semiconductor research. $3 3683765
650 4 $a Accuracy. $3 3559958
650 4 $a Deep learning. $3 3554982
650 4 $a Datasets. $3 3541416
650 4 $a Success. $3 518195
650 4 $a Boolean. $3 3683493
650 4 $a Artificial intelligence. $3 516317
650 4 $a Logic. $3 529544
650 4 $a Neural networks. $3 677449
650 4 $a Variables. $3 3548259
650 4 $a Computer engineering. $3 621879
650 4 $a Feature selection. $3 3560270
650 4 $a Algorithms. $3 536374
650 4 $a Ablation. $3 3562462
650 4 $a Heuristic. $3 568476
650 4 $a Cognition & reasoning. $3 3556293
653 $a Constraint solvers
653 $a Machine learning
653 $a Model counting
653 $a QBF
653 $a Reinforcement learning
653 $a SAT
690 $a 0984
690 $a 0395
690 $a 0464
690 $a 0800
710 2 $a University of California, Berkeley. $b Computer Science. $3 1043689
773 0 $t Dissertations Abstracts International $g 83-03B.
790 $a 0028
791 $a Ph.D.
792 $a 2021
793 $a English
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=28539783