國立高雄大學圖資館 |

登入

回首頁

Searching for truth :Techniques for satisfiability of Boolean formulas.

紀錄類型:	書目-電子資源 : Monograph/item
正題名/作者:	Searching for truth :
其他題名:	Techniques for satisfiability of Boolean formulas.
作者:	Zhang, Lintao.
面頁冊數:	197 p.
附註:	Adviser: Sharad Malik.
附註:	Source: Dissertation Abstracts International, Volume: 64-09, Section: B, page: 4544.
Contained By:	Dissertation Abstracts International64-09B.
標題:	Engineering, Electronics and Electrical.
電子資源:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3102236
ISBN:	0496498061

Searching for truth :Techniques for satisfiability of Boolean formulas.
Zhang, Lintao.

Searching for truth :Techniques for satisfiability of Boolean formulas. [electronic resource] - 197 p.

Adviser: Sharad Malik.

Thesis (Ph.D.)--Princeton University, 2003.

Even though researchers have been studying SAT solving algorithms for a long time, efforts were mainly concentrated on improving the algorithms to prune search spaces. In this thesis, the implementation issues of SAT solvers are studied. Some of the most widely used techniques in SAT solving algorithms are quantitatively evaluated. Techniques on efficient and effective implementation of these techniques to achieve the best performance are provided. The SAT solver developed by utilizing these results can often achieve 10--100x speedups over other existing SAT solvers. It is widely used by many research groups and is widely regarded as one of the best SAT solvers available.

ISBN: 0496498061Subjects--Topical Terms:

226981
Engineering, Electronics and Electrical.

Searching for truth :Techniques for satisfiability of Boolean formulas.
LDR:04410nmm _2200313 _450 001 162134
005 20051017073414.5
008 230606s2003 eng d
020 $a 0496498061
035 $a 00148635
035 $a 162134
040 $a UnM $c UnM
100 0 $a Zhang, Lintao. $3 227247
245 1 0 $a Searching for truth : $b Techniques for satisfiability of Boolean formulas. $h [electronic resource]
300 $a 197 p.
500 $a Adviser: Sharad Malik.
500 $a Source: Dissertation Abstracts International, Volume: 64-09, Section: B, page: 4544.
502 $a Thesis (Ph.D.)--Princeton University, 2003.
520 # $a Even though researchers have been studying SAT solving algorithms for a long time, efforts were mainly concentrated on improving the algorithms to prune search spaces. In this thesis, the implementation issues of SAT solvers are studied. Some of the most widely used techniques in SAT solving algorithms are quantitatively evaluated. Techniques on efficient and effective implementation of these techniques to achieve the best performance are provided. The SAT solver developed by utilizing these results can often achieve 10--100x speedups over other existing SAT solvers. It is widely used by many research groups and is widely regarded as one of the best SAT solvers available.
520 # $a For some applications, it is often desirable for the SAT solver to have some special abilities besides simply determining the satisfiability of a Boolean formula. Two of such special abilities are discussed in this thesis. For mission critical applications, the SAT solvers employed are often required to provide a means for third party checkers to check the deduction process in order to verify the correctness of the proof. In the thesis a method to provide such a certification procedure is discussed. The second ability discussed is to find a small unsatisfiable sub-formula from an unsatisfiable SAT instance. This ability is often useful for debugging purposes for some applications that use SAT. This thesis discusses how these two special abilities are related and how to implement them on existing SAT solver frameworks. Extensive experimental results are provided to prove the practical feasibility of the approach.
520 # $a For some of the Boolean reasoning tasks, propositional Boolean formulas are not sufficient. This thesis discusses the problem of deciding the satisfiability of Quantified Boolean Formulas (QBF). A Quantified Boolean formula contains both universal and existential quantifiers. Therefore, it is more expressive than a propositional Boolean formula. A technique called learning and non-chronological backtracking, which has been shown to work very well on SAT solvers, is applied on a QBF solver. Experimental results show that these techniques, when properly adapted, can greatly improve the QBF solver as well.
520 # $a Given a propositional Boolean formula, the problem of determining whether it can evaluate to the value true is called the Boolean Satisfiability Problem, or SAT. SAT is one of the most important and widely studied problems in computer science. Researchers have been investigating algorithms to solve SAT problems for more than forty years and great progress has been made.
520 # $a In practice, SAT is a core problem that appears in many applications in Electronic Design Automation (EDA), Artificial Intelligence (AI) and other areas. This thesis investigates the practical problem of using SAT solvers as a feasible reasoning and deduction engine in real world applications. To facilitate the application of SAT to real world situations, the problems are attacked on several fronts.
520 # $a Overall, this thesis is about properly engineering algorithms to make tools that can help solving practical problems. In particular, the tools discussed are SAT and QBF solvers. By carefully examine the algorithms and their implementation details, improvements have been made on these solvers that can help wider employment of them as feasible deduction engines for real world applications.
590 $a School code: 0181.
650 # 0 $a Engineering, Electronics and Electrical. $3 226981
650 # 0 $a Computer Science. $3 212513
650 # 0 $a Artificial Intelligence. $3 212515
710 0 # $a Princeton University. $3 212488
773 0 # $g 64-09B. $t Dissertation Abstracts International
790 $a 0181
790 1 0 $a Malik, Sharad, $e advisor
791 $a Ph.D.
792 $a 2003
856 4 0 $u http://libsw.nuk.edu.tw/login?url=http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3102236 $z http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3102236