國立虎尾科技大學 |

Exploring a Two-Solver Architecture for Clause Learning CSP Solvers.

Record Type:	Language materials, manuscript : Monograph/item
Title/Author:	Exploring a Two-Solver Architecture for Clause Learning CSP Solvers./
Author:	Erdem, Ozan.
Description:	1 online resource (149 pages)
Notes:	Source: Dissertation Abstracts International, Volume: 79-04(E), Section: B.
Contained By:	Dissertation Abstracts International79-04B(E).
Subject:	Artificial intelligence. -
Online resource:	click for full text (PQDT)
ISBN:	9780355440966

Exploring a Two-Solver Architecture for Clause Learning CSP Solvers.
Erdem, Ozan.

Exploring a Two-Solver Architecture for Clause Learning CSP Solvers. - 1 online resource (149 pages)

Source: Dissertation Abstracts International, Volume: 79-04(E), Section: B.

Thesis (Ph.D.)--University of Toronto (Canada), 2017.

Includes bibliographical references

Many real world problems can be encoded as Constraint Satisfaction Problems (CSPs). Constraint satisfaction problems contain variables over finite domains, as well as constraints over these variables. There exists many solvers that can solve these problems efficiently. Once these problems are solved, their solutions correspond to solutions of the real world problem the CSP encodes.

Electronic reproduction.
Ann Arbor, Mich. :
ProQuest,
2018

Mode of access: World Wide Web

ISBN: 9780355440966Subjects--Topical Terms:

559380
Artificial intelligence.
Index Terms--Genre/Form:

554714
Electronic books.

Exploring a Two-Solver Architecture for Clause Learning CSP Solvers.
LDR:03551ntm a2200385Ki 4500 001 916751
005 20180928111500.5
006 m o u
007 cr mn||||a|a||
008 190606s2017 xx obm 000 0 eng d
020 $a 9780355440966
035 $a (MiAaPQ)AAI10246661
035 $a (MiAaPQ)toronto:15109
035 $a AAI10246661
040 $a MiAaPQ $b eng $c MiAaPQ $d NTU
100 1 $a Erdem, Ozan. $3 1190571
245 1 0 $a Exploring a Two-Solver Architecture for Clause Learning CSP Solvers.
264 0 $c 2017
300 $a 1 online resource (149 pages)
336 $a text $b txt $2 rdacontent
337 $a computer $b c $2 rdamedia
338 $a online resource $b cr $2 rdacarrier
500 $a Source: Dissertation Abstracts International, Volume: 79-04(E), Section: B.
500 $a Adviser: Fahiem Bacchus.
502 $a Thesis (Ph.D.)--University of Toronto (Canada), 2017.
504 $a Includes bibliographical references
520 $a Many real world problems can be encoded as Constraint Satisfaction Problems (CSPs). Constraint satisfaction problems contain variables over finite domains, as well as constraints over these variables. There exists many solvers that can solve these problems efficiently. Once these problems are solved, their solutions correspond to solutions of the real world problem the CSP encodes.
520 $a Similarly, many problems can be encoded as instances of the Satisfiability Problem (SAT). In SAT all the variables are binary propositions, and the only kind of constraint they allow is the disjunction of a set of variables. SAT and CSP are closely related, and they both are NP-complete.
520 $a These two approaches have their own advantages and disadvantages. SAT solvers perform clause learning, which prevents them from visiting similar subtrees in the search tree. The advantage of CSP solvers is that the CSP instances contain higher level constraints, which allows better reasoning. Recently, methods combining the advantages of SAT and CSP solvers have emerged. In such methods, solvers maintain a propositional representation of the CSP problem, and perform clause learning over this representation. Such solvers are called "clause learning CSP solvers".
520 $a However, the question of how to handle constraints in such solvers is unresolved. For each constraint, a solver must choose whether to encode the constraint entirely in SAT or use a special purpose propagator, and this choice also determines the propagation strength and efficiency. Different choices perform better in different scenarios, hence hybrid methods which can be adaptive are promising.
520 $a In this thesis, we propose an alternative architecture for clause learning CSP solvers, which incorporates two solvers of different strength. One of the solvers directs the search using fast and weak propagators. Once it gets into a dead end, it produces a conflict clause, and asks the other solver to enhance it using stronger but slower propagators. In this way, the slower propagators are run only whenever they are likely to be needed, instead of each node in the search tree. We instantiate this architecture in different ways, and perform experiments to demonstrate the trade-offs between these instantiations.
533 $a Electronic reproduction. $b Ann Arbor, Mich. : $c ProQuest, $d 2018
538 $a Mode of access: World Wide Web
650 4 $a Artificial intelligence. $3 559380
650 4 $a Computer science. $3 573171
655 7 $a Electronic books. $2 local $3 554714
690 $a 0800
690 $a 0984
710 2 $a ProQuest Information and Learning Co. $3 1178819
710 2 $a University of Toronto (Canada). $b Computer Science. $3 845521
773 0 $t Dissertation Abstracts International $g 79-04B(E).
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=10246661 $z click for full text (PQDT)