% This file was created with JabRef 2.3.1.
% Encoding: EUC_JP

@string{ICCAD-2002 = {Proceedings of the 2002 International Conference on
Computer-Aided Design (ICCAD 2002)}}

@string{DATE-2008 = {Proceedings of Design, Automation and Test in
  Europe (DATE 2008)}}

@string{AAMAS-2002 = {Proceedings of the 1st International Joint Conference on
Autonomous Agents {\&} Multiagent Systems}}
@string{IJCAR-2001 = {Proceedings of the 1st International Joint Conference on
Automated Reasoning (IJCAR 2001), LNCS 2083}}

@STRING{AAAI-1992 = {Proceedings of the 10th National Conference on Artificial Intelligence
	(AAAI 1992)}}

@STRING{AAAI-1993 = {Proceedings of the 11th National Conference on Artificial Intelligence
	(AAAI 1993)}}

@STRING{AAAI-1994 = {Proceedings of the 12th National Conference on Artificial Intelligence
	(AAAI 1994)}}

@STRING{AAAI-1996 = {Proceedings of the 13th National Conference on Artificial Intelligence
	(AAAI 1996)}}

@STRING{AAAI-1997 = {Proceedings of the 14th National Conference on Artificial Intelligence
	(AAAI 1997)}}

@STRING{AAAI-1998 = {Proceedings of the 15th National Conference on Artificial Intelligence
	(AAAI 1998)}}

@STRING{AAAI-1999 = {Proceedings of the 16th National Conference on Artificial Intelligence
	(AAAI 1999)}}

@STRING{AAAI-2000 = {Proceedings of the 17th National Conference on Artificial Intelligence
	(AAAI 2000)}}

@STRING{AAAI-2002 = {Proceedings of the 18th National Conference on Artificial Intelligence
	(AAAI 2002)}}

@STRING{AAAI-2004 = {Proceedings of the 19th National Conference on Artificial Intelligence
	(AAAI 2004)}}

@STRING{AAAI-2005 = {Proceedings of the 20th National Conference on Artificial Intelligence
	(AAAI 2005)}}

@STRING{AAAI-2006 = {Proceedings of the 21st National Conference on Artificial Intelligence
	(AAAI 2006)}}

@STRING{AAAI-2007 = {Proceedings of the 22nd National Conference on Artificial Intelligence
	(AAAI 2007)}}

@STRING{AAAI-2008 = {Proceedings of the 23rd National Conference on Artificial Intelligence
	(AAAI 2008)}}

@STRING{ACM-TOCL = {ACM Transactions on Computational Logic}}

@STRING{ACM-TOPLAS = {ACM Transactions on Programming Languages and Systems}}

@STRING{ACMCS = {ACM Computing Surveys}}

@STRING{AI = {Artificial Intelligence}}

@STRING{AI*IA-2007 = {Proceedings of the 10th Congress of the Italian Association for Artificial
	Intelligence ({AI*IA} 2007), LNCS 4733}}

@STRING{AIPS-1998 = {Proceedings of the 4th International Conference on Artificial Intelligence
	Planning Systems (AIPS 1998)}}

@STRING{AMAI = {Annals of Mathematics and Artificial Intelligence}}

@STRING{AUSAI-2002 = {Proceedings of the 15th Australian Joint Conference on Artificial
	Intelligence, LNCS 2557}}

@STRING{AUSAI-2006 = {Proceedings of the 19th Australian Joint Conference on Artificial
	Intelligence, LNCS 4304}}

@STRING{CACM = {Communications of the ACM}}

@STRING{CADE-2000 = {Proceedings of the 17th International Conference on Automated Deduction
	(CADE-17), LNCS 1831}}

@STRING{CADE-2002 = {Proceedings of the 18th International Conference on Automated Deduction
	(CADE-18), LNCS 2392}}

@STRING{CADE-2003 = {Proceedings of the 19th International Conference on Automated Deduction
	(CADE-19), LNCS 2741}}

@STRING{CADE-2005 = {Proceedings of the 20th International Conference on Automated Deduction
	(CADE-20), LNCS 3632}}

@STRING{CADE-2007 = {Proceedings of the 21st International Conference on Automated Deduction
	(CADE-21), LNCS 4603}}

@STRING{CAV-2002 = {Proceedings of the 14th International Conference on Computer Aided
	Verification (CAV 2002), LNCS 2404}}

@STRING{CAV-2003 = {Proceedings of the 15th International Conference on Computer Aided
	Verification (CAV 2003), LNCS 2725}}

@STRING{CAV-2004 = {Proceedings of the 16th International Conference on Computer Aided
	Verification (CAV 2004), LNCS 3114}}

@STRING{CAV-2005 = {Proceedings of the 17th International Conference on Computer Aided
	Verification (CAV 2005), LNCS 3576}}

@STRING{COMPSOFT = {コンピュータソフトウェア}}

@STRING{CONSTRAINTS = {Constraints}}

@STRING{CP-1997 = {Proceedings of the 3rd International Joint Conference on Principles
	and Practice of Constraint Programming (CP 1997), LNCS 1330}}

@STRING{CP-1998 = {Proceedings of the 4th International Joint Conference on Principles
	and Practice of Constraint Programming (CP 1998), LNCS 1520}}

@STRING{CP-1999 = {Proceedings of the 5th International Joint Conference on Principles
	and Practice of Constraint Programming (CP 1999), LNCS 1713}}

@STRING{CP-2000 = {Proceedings of the 6th International Joint Conference on Principles
	and Practice of Constraint Programming (CP 2000), LNCS 1894}}

@STRING{CP-2001 = {Proceedings of the 7th International Joint Conference on Principles
	and Practice of Constraint Programming (CP 2001), LNCS 2239}}

@STRING{CP-2002 = {Proceedings of the 8th International Joint Conference on Principles
	and Practice of Constraint Programming (CP 2002), LNCS 2470}}

@STRING{CP-2003 = {Proceedings of the 9th International Joint Conference on Principles
	and Practice of Constraint Programming (CP 2003), LNCS 2833}}

@STRING{CP-2004 = {Proceedings of the 10th International Joint Conference on Principles
	and Practice of Constraint Programming (CP 2004), LNCS 3258}}

@STRING{CP-2005 = {Proceedings of the 11th International Joint Conference on Principles
	and Practice of Constraint Programming (CP 2005), LNCS 3709}}

@STRING{CP-2006 = {Proceedings of the 12th International Joint Conference on Principles
	and Practice of Constraint Programming (CP 2006), LNCS 4204}}

@STRING{CP-2007 = {Proceedings of the 13th International Joint Conference on Principles
	and Practice of Constraint Programming (CP 2007), LNCS 4741}}

@STRING{CP-2008 = {Proceedings of the 14th International Joint Conference on Principles
	and Practice of Constraint Programming (CP 2008), LNCS 5202}}

@STRING{CPAIOR-2004 = {Proceedings of the 1st International Conference on Integration of
	AI and OR Techniques in Constraint Programming for Combinatorial
	Optimization Problems (CPAIOR 2004), LNCS 3011}}

@STRING{CPAIOR-2005 = {Proceedings of the 2nd International Conference on Integration of
	AI and OR Techniques in Constraint Programming for Combinatorial
	Optimization Problems (CPAIOR 2005), LNCS 3524}}

@STRING{CPAIOR-2006 = {Proceedings of the 3rd International Conference on Integration of
	AI and OR Techniques in Constraint Programming for Combinatorial
	Optimization Problems (CPAIOR 2006), LNCS 3990}}

@STRING{CPAIOR-2007 = {Proceedings of the 4th International Conference on Integration of
	AI and OR Techniques in Constraint Programming for Combinatorial
	Optimization Problems (CPAIOR 2007), LNCS 4510}}

@STRING{CPAIOR-2008 = {Proceedings of the 5th International Conference on Integration of
	AI and OR Techniques in Constraint Programming for Combinatorial
	Optimization Problems (CPAIOR 2008), LNCS 5015}}

@STRING{CPAIOR-2009 = {Proceedings of the 6th International Conference on Integration of
	AI and OR Techniques in Constraint Programming for Combinatorial
	Optimization Problems (CPAIOR 2009), LNCS 5547}}

@STRING{CSC-2006 = {Proceedings of the 2nd International CSP Solver Competition}}

@STRING{CSC-2008 = {Proceedings of the 3rd International CSP Solver Competition}}

@STRING{CSCLP-2004 = {Proceedings of the International Workshop on Constraint Solving and
	Constraint Logic Programming (CSCLP 2004), LNCS 3419}}

@STRING{DAC-2001 = {Proceedings of the 38th Design Automation Conference (DAC 2001)}}

@STRING{DAM = {Discrete Applied Mathematics}}

@STRING{ECAI-1992 = {Proceedings of the 10th European Conference on Artificial Intelligence
	(ECAI 1992)}}

@STRING{ECAI-2002 = {Proceedings of the 15th European Conference on Artificial Intelligence
	(ECAI 2002)}}

@STRING{ECAI-2004 = {Proceedings of the 16th European Conference on Artificial Intelligence
	(ECAI 2004)}}

@STRING{ECAI-2006 = {Proceedings of the 17th European Conference on Artificial Intelligence
	(ECAI 2006), FAIA 141}}

@STRING{ECAI-2008 = {Proceedings of the 18th European Conference on Artificial Intelligence
	(ECAI 2008), FAIA 178}}

@STRING{ECP-1997 = {Proceedings of the 4th European Conference on Planning (ECP 1997),
	LNCS 1348}}

@STRING{ECP-1999 = {Proceedings of the 5th European Conference on Planning (ECP 1999),
	LNCS 1809}}

@STRING{ENTCS = {Electronic Notes in Theoretical Computer Science}}

@STRING{FOCS-1989 = {Proceedings of the 30th Annual Symposium on Foundations of Computer Science
	(FOCS 1989)}}

@STRING{FOCS-1997 = {Proceedings of the 38th Annual Symposium on Foundations of Computer Science
	(FOCS 1997)}}

@STRING{FOCS-2003 = {Proceedings of the 44th Annual Symposium on Foundations of Computer Science
	(FOCS 2003)}}

@STRING{FROCOS-2002 = {Proceedings of the 4th International Workshop on Frontiers of Combining
	System (FroCoS 2002), LNCS 2309}}

@STRING{HOS = {Handbook of Satisfiability}}

@STRING{ICAPS-2006 = {Proceedings of the International Conference on Automated Planning
	and Scheduling 2006 (ICAPS 2006)}}

@STRING{ICCAD-2001 = {Proceedings of the 2001 International Conference on Computer-Aided
	Design (ICCAD 2001)}}

@STRING{ICSE-2003 = {Proceedings of the 25th International Conference on Software Engineering
	(ICSE 2003)}}

@STRING{ICTAI-2005 = {Proceedings of the 17th IEEE International Conference on Tools with
	Artificial Intelligence (ICTAI 2005)}}

@STRING{IEEE-TIT = {IEEE Transactions on Information Theory}}

@STRING{IEEE-TSE = {IEEE Transactions on Software Engineering}}

@STRING{IEEE-TKDE = {IEEE Transactions on Knowledge and Data Engineering}}

@STRING{IEICETR-AI = {電子情報通信学会技術研究報告，AI}}

@STRING{IJCAI-1989 = {Proceedings of the 11th International Joint Conference on Artificial
	Intelligence (IJCAI 1989)}}

@STRING{IJCAI-1997 = {Proceedings of the 15th International Joint Conference on Artificial
	Intelligence (IJCAI 1997)}}

@STRING{IJCAI-1999 = {Proceedings of the 16th International Joint Conference on Artificial
	Intelligence (IJCAI 1999)}}

@STRING{IJCAI-2001 = {Proceedings of the 17th International Joint Conference on Artificial
	Intelligence (IJCAI 2001)}}

@STRING{IJCAI-2003 = {Proceedings of the 18th International Joint Conference on Artificial
	Intelligence (IJCAI 2003)}}

@STRING{IJCAI-2005 = {Proceedings of the 19th International Joint Conference on Artificial
	Intelligence (IJCAI 2005)}}

@STRING{IJCAI-2007 = {Proceedings of the 20th International Joint Conference on Artificial
	Intelligence (IJCAI 2007)}}

@STRING{IJCAI-2009 = {Proceedings of the 21st International Joint Conference on Artificial
	Intelligence (IJCAI 2009)}}

@STRING{IPC-5 = {Proceedings of the 5th International Planning Competition (IPC-5)}}

@STRING{IPC-6 = {Proceedings of the 6th International Planning Competition (IPC-6)}}

@STRING{JACM = {Journal of the ACM}}

@STRING{JAIR = {Journal of Artificial Intelligence Research}}

@STRING{JAR = {Journal of Automated Reasoning}}

@STRING{JCSS = {Journal of Computer and System Sciences}}

@STRING{JELIA-2006 = {Proceedings of the 10th European Conference on Logics in Artificial
	Intelligence (JELIA 2006), LNCS 4160}}

@STRING{JLP = {Journal of Logic Programming}}

@STRING{JSAI = {人工知能学会誌}}

@STRING{JSAT = {Journal on Satisfiability, Boolean Modeling and Computation}}

@STRING{KR-1998 = {Proceedings of the 6th nternational Conference on Principles of Knowledge
	Representation and Reasoning (KR 1998)}}

@STRING{LICS-2001 = {Proceedings of the 17th IEEE Symposium on Logic in Computer Science
	(LICS 2001)}}

@STRING{LICS-2003 = {Proceedings of the 18th IEEE Symposium on Logic in Computer Science
	(LICS 2003)}}

@STRING{ModRef-2004 = {Proceedings of the 3rd International Workshop on Modelling and Reformulating
	Constraint Satisfaction Problems}}

@STRING{RTA-2002 = {Proceedings of the 13th International Conference on Term Rewriting
	and Applications (RTA 2002), LNCS 2378}}

@STRING{RTA-2005 = {Proceedings of the 16th International Conference on Term Rewriting
	and Applications (RTA 2005), LNCS 3467}}

@STRING{SAT-2003 = {Proceedings of the 6th International Conference on Theory and Applications
	of Satisfiability Testing (SAT 2003), LNCS 2919}}

@STRING{SAT-2004 = {Proceedings of the 7th International Conference on Theory and Applications
	of Satisfiability Testing (SAT 2004), LNCS 3542}}

@STRING{SAT-2005 = {Proceedings of the 8th International Conference on Theory and Applications
	of Satisfiability Testing (SAT 2005), LNCS 3569}}

@STRING{SAT-2006 = {Proceedings of the 9th International Conference on Theory and Applications
	of Satisfiability Testing (SAT 2006), LNCS 4121}}

@STRING{SAT-2007 = {Proceedings of the 10th International Conference on Theory and Applications
	of Satisfiability Testing (SAT 2007), LNCS 4501}}

@STRING{SAT-2008 = {Proceedings of the 11th International Conference on Theory and Applications
	of Satisfiability Testing (SAT 2008), LNCS 4996}}

@STRING{SAT-2009 = {Proceedings of the 12th International Conference on Theory and Applications
	of Satisfiability Testing (SAT 2009), LNCS 5584}}

@STRING{TABLEAUX-1996 = {Proceedings of the 5th International Workshop on Theorem Proving
	with Analytic Tableaux and Related Methods (TABLEAUX 1996), LNCS
	1071}}

@STRING{TACAS-1999 = {Proceedings of the 5th International Conference on Tools and Algorithms
	for Construction and Analysis of Systems (TACAS 1999), LNCS 1579}}

@STRING{TACAS-2005 = {Proceedings of the 11th International Conference on Tools and Algorithms
	for Construction and Analysis of Systems (TACAS 2005), LNCS 3440}}

@STRING{TCS = {Theoretical Computer Science}}

@STRING{TIPSJ = {情報処理学会論文誌}}

@STRING{TJSAI = {人工知能学会論文誌}}

@ARTICLE{JSAI:Nabeshima10,
  author = {鍋島 英知},
  title = {{SAT}によるプランニングとスケジューリング},
  journal = JSAI,
  year = {2010},
  volume = {25},
  number = {1},
  timestamp = {2009.11.05},
  yomi = {Hidetomo Nabeshima}
}

@ARTICLE{JSAI:Iwama01,
  author = {岩間 一雄},
  title = {{CNF}充足可能性判定問題の計算複雑さ},
  journal = JSAI,
  year = {2001},
  volume = {16},
  pages = {636--647},
  number = {5},
  timestamp = {2009.11.05},
  yomi = {Kazuo Iwama}
}

@ARTICLE{JSAI:Miyashita01,
  author = {宮下 和雄},
  title = {プランニングとスケジューリング},
  journal = JSAI,
  year = {2001},
  volume = {16},
  pages = {611--616},
  number = {5},
  month = {9},
  timestamp = {2009.11.05},
  yomi = {Kazuo Miyashita}
}

@BOOK{BOOK:Hagiya94,
  title = {ソフトウェア科学のための論理学},
  publisher = {岩波書店},
  year = {1994},
  author = {萩谷 昌己},
  timestamp = {2009.11.05},
  yomi = {Masami Hagiya}
}

@ARTICLE{JSAI:BanbaraT10,
  author = {番原 睦則 and 田村 直之},
  title = {{SAT}によるシステム検証},
  journal = JSAI,
  year = {2010},
  volume = {25},
  number = {1},
  timestamp = {2009.11.05},
  yomi = {Mutsunori Banbara and Naoyuki Tamura}
}

@ARTICLE{JSAI:HirayamaY10,
  author = {平山 勝敏 and 横尾 真},
  title = {$*$-{SAT}: {SAT}の拡張},
  journal = JSAI,
  year = {2010},
  volume = {25},
  number = {1},
  timestamp = {2009.11.05},
  yomi = {Katsutoshi Hirayama and Makoto Yokoo}
}

@ARTICLE{JSAI:InoueT10,
  author = {井上 克巳 and 田村 直之},
  title = {{SAT}ソルバーの基礎},
  journal = JSAI,
  year = {2010},
  volume = {25},
  number = {1},
  timestamp = {2009.11.05},
  yomi = {Katsumi Inoue and Naoyuki Tamura}
}

@ARTICLE{JSAI:IwanumaN10,
  author = {岩沼 宏治 and 鍋島 英知},
  title = {{SMT}: 個別理論を取り扱う{SAT}技術},
  journal = JSAI,
  year = {2010},
  volume = {25},
  number = {1},
  timestamp = {2009.11.05},
  yomi = {Koji Iwanuma and Hidetomo Nabeshima}
}

@ARTICLE{JSAI:NabeshimaS10,
  author = {鍋島 英知 and 宋 剛秀},
  title = {高速{SAT}ソルバーの原理},
  journal = JSAI,
  year = {2010},
  volume = {25},
  number = {1},
  timestamp = {2009.11.05},
  yomi = {Hidetomo Nabeshima and Takehide Soh}
}

@ARTICLE{COMPSOFT:InoueS08,
  author = {井上 克巳 and 坂間 千秋},
  title = {論理プログラミングから解集合プログラミングへ},
  journal = COMPSOFT,
  year = {2008},
  volume = {25},
  pages = {20--32},
  number = {3},
  timestamp = {2009.11.05},
  yomi = {Katsumi Inoue and Chiaki Sakama}
}

@ARTICLE{JSAI:NabeshimaI01,
  author = {鍋島 英知 and 井上 克巳},
  title = {プランニンググラフと{SAT}プランニング},
  journal = JSAI,
  year = {2001},
  volume = {16},
  pages = {605--610},
  number = {5},
  timestamp = {2009.11.05},
  yomi = {Hidetomo Nabeshima and Katsumi Inoue}
}

@BOOK{BOOK:ArikawaH88,
  title = {述語論理と論理プログラミング},
  publisher = {オーム社},
  year = {1988},
  author = {有川 節夫 and 原口 誠},
  timestamp = {2009.11.05},
  yomi = {Setsuo Arikawa and Makoto Haraguchi}
}

@ARTICLE{COMPSOFT:IwanumaNI,
  author = {岩沼 宏治 and 鍋島 英知 and 井上 克巳},
  title = {一階論理上の等号推論：理論と実際},
  journal = COMPSOFT,
  note = {(投稿予定)},
  timestamp = {2009.11.05},
  yomi = {Koji Iwanuma and Hidetomo Nabeshima and Katsumi Inoue}
}

@ARTICLE{JSAI:HasegawaFK10,
  author = {長谷川 隆三 and 藤田 博 and 越村 三幸},
  title = {モデル列挙とモデル計数},
  journal = JSAI,
  year = {2010},
  volume = {25},
  number = {1},
  timestamp = {2009.11.05},
  yomi = {Ryuzo Hasegawa and Hiroshi Fujita and Miyuki Koshimura}
}

@ARTICLE{JSAI:TamuraTB10,
  author = {田村 直之 and 丹生 智也 and 番原 睦則},
  title = {制約最適化問題と{SAT}符号化},
  journal = JSAI,
  year = {2010},
  volume = {25},
  number = {1},
  timestamp = {2009.11.05},
  yomi = {Naoyuki Tamura and Tomoya Tanjo and Mutsunori Banbara}
}

@ARTICLE{COMPSOFT:HasegawaFK08,
  author = {長谷川 隆三 and 藤田 博 and 越村 三幸},
  title = {モデル生成型定理証明と要素技術},
  journal = COMPSOFT,
  year = {2008},
  volume = {25},
  pages = {2--10},
  number = {3},
  timestamp = {2009.11.05},
  yomi = {Ryuzo Hasegawa and Hiroshi Fujita and Miyuki Koshimura}
}

@ARTICLE{JSAI:HasegawaFK01,
  author = {長谷川 隆三 and 藤田 博 and 越村 三幸},
  title = {タブロー法とモデル生成型定理証明},
  journal = JSAI,
  year = {2001},
  volume = {16},
  pages = {661--667},
  number = {5},
  timestamp = {2009.11.05},
  yomi = {Ryuzo Hasegawa and Hiroshi Fujita and Miyuki Koshimura}
}

@ARTICLE{TJSAI:HasegawaFK01,
  author = {長谷川 隆三 and 藤田 博 and 越村 三幸},
  title = {分岐補題の抽出による極小モデル生成の効率化},
  journal = TJSAI,
  year = {2001},
  volume = {16},
  pages = {234--245},
  number = {2},
  timestamp = {2009.11.05},
  yomi = {Ryuzo Hasegawa and Hiroshi Fujita and Miyuki Koshimura}
}

@INPROCEEDINGS{SS09:KoshimuraNFH09,
  author = {越村 三幸 and 鍋島 英知 and 藤田 博 and 長谷川 隆三},
  title = {{SAT}変換による未解決ジョブショップスケジューリング問題への挑戦},
  booktitle = {スケジューリング・シンポジウム2009講演論文集},
  year = {2009},
  pages = {209--213},
  timestamp = {2009.11.05},
  yomi = {Miyuki Koshimura and Hidetomo Nabeshima and Hiroshi Fujita and Ryuzo
	Hasegawa}
}

@INPROCEEDINGS{JSSST25:KoshimuraNFH08,
  author = {越村 三幸 and 鍋島 英知 and 藤田 博 and 長谷川 隆三},
  title = {極小モデル生成とジョブショップスケジューリング問題の解法},
  booktitle = {日本ソフトウェア科学会第25回大会 講演論文集},
  year = {2008},
  note = {8A-2},
  timestamp = {2009.11.05},
  yomi = {Miyuki Koshimura and Hidetomo Nabeshima and Hiroshi Fujita and Ryuzo
	Hasegawa}
}

@INPROCEEDINGS{SS07:TagaTKB07,
  author = {多賀 明子 and 田村 直之 and 北川 哲 and 番原 睦則},
  title = {グリッド計算環境上でのショップ・スケジューリング問題の{SAT}変換による解法},
  booktitle = {スケジューリング・シンポジウム2007講演論文集},
  year = {2007},
  pages = {109--114},
  timestamp = {2009.11.05},
  yomi = {Akiko Taga and Naoyuki Tamura and Satoshi Kitagawa and Mutsunori Banbara}
}

@ARTICLE{IEICETR-AI:NabeshimaSII06,
  author = {鍋島 英知 and 宋 剛秀 and 井上 克巳 and 岩沼 宏治},
  title = {効率的な{SAT}プランニングと{SAT}スケジューリングのための補題再利用},
  journal = IEICETR-AI,
  year = {2006},
  volume = {106},
  pages = {18--24},
  number = {38},
  timestamp = {2009.11.05},
  yomi = {Hidetomo Nabeshima and Takehide Soh and Katsumi Inoue and Koji Iwanuma}
}

@INPROCEEDINGS{SS07:TamuraTBSNI07,
  author = {田村 直之 and 多賀 明子 and 番原 睦則 and 宋 剛秀 and 鍋島 英知 and 井上 克巳},
  title = {ショップ・スケジューリング問題の{SAT}変換による解法},
  booktitle = {スケジューリング・シンポジウム2007講演論文集},
  year = {2007},
  pages = {97--102},
  timestamp = {2009.11.05},
  yomi = {Naoyuki Tamura and Akiko Taga and Mutsunori Banbara and Takehide Soh
	and Hidetomo Nabeshima and Katsumi Inoue}
}

@INPROCEEDINGS{DBLP:conf/ijcai/Kleer89,
  author = {Johan {de Kleer}},
  title = {A Comparison of {ATMS} and {CSP} Techniques},
  booktitle = IJCAI-1989,
  year = {1989},
  pages = {290--296},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ecp/ArmandoCG99,
  author = {Alessandro Armando and Claudio Castellini and Enrico Giunchiglia},
  title = {SAT-Based Procedures for Temporal Reasoning},
  booktitle = ECP-1999,
  year = {1999},
  pages = {97--108},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/sat/AudemardBHJS08,
  author = {Gilles Audemard and Lucas Bordeaux and Youssef Hamadi and Sa\"{\i}d
	Jabbour and Lakhdar Sais},
  title = {A Generalized Framework for Conflict Analysis},
  booktitle = SAT-2008,
  year = {2008},
  pages = {21--27},
  ee = {http://dx.doi.org/10.1007/978-3-540-79719-7_3},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ijcai/AudemardS09,
  author = {Gilles Audemard and Laurent Simon},
  title = {Predicting Learnt Clauses Quality in Modern {SAT} Solvers},
  booktitle = IJCAI-2009,
  year = {2009},
  pages = {399--404},
  ee = {http://ijcai.org/papers09/Papers/IJCAI09-074.pdf},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/cp/Bacchus07a,
  author = {Fahiem Bacchus},
  title = {{GAC} via Unit Propagation},
  booktitle = CP-2007,
  year = {2007},
  pages = {133--147},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/focs/BacchusDP03,
  author = {Fahiem Bacchus and Shannon Dalmao and Toniann Pitassi},
  title = {Algorithms and Complexity Results for {\#SAT} and Bayesian Inference},
  booktitle = FOCS-2003,
  year = {2003},
  pages = {340--351},
  ee = {http://csdl.computer.org/comp/proceedings/focs/2003/2040/00/20400340abs.htm},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/sat/BailleuxBR09,
  author = {Olivier Bailleux and Yacine Boufkhad and Olivier Roussel},
  title = {New Encodings of Pseudo-Boolean Constraints into {CNF}},
  booktitle = SAT-2009,
  year = {2009},
  pages = {181--194},
  ee = {http://dx.doi.org/10.1007/978-3-642-02777-2_19},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/jsat/BailleuxBR06,
  author = {Olivier Bailleux and Yacine Boufkhad and Olivier Roussel},
  title = {A Translation of Pseudo Boolean Constraints to {SAT}},
  journal = JSAT,
  year = {2006},
  volume = {2},
  pages = {191--200},
  number = {1-4},
  ee = {http://jsat.ewi.tudelft.nl/content/volume2/JSAT2_8_Bailleux.pdf},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/cp/BandaMRW06,
  author = {Maria J. Garc\'{\i}a de la Banda and Kim Marriott and Reza Rafeh
	and Mark Wallace},
  title = {The Modelling Language {Zinc}},
  booktitle = CP-2006,
  year = {2006},
  pages = {700--705},
  timestamp = {2009.11.03}
}

@MISC{SMTCOMP,
  author = {B. Barrett and M. Deters and A. Oliveras and A. Stump},
  title = {International Satisfiability Modulo Theories Competition},
  howpublished = {{\tt http://www.smtcomp.org}},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/frocos/BarrettDS02,
  author = {Clark W. Barrett and David L. Dill and Aaron Stump},
  title = {A Generalization of Shostak's Method for Combining Decision Procedures},
  booktitle = FROCOS-2002,
  year = {2002},
  pages = {132--146},
  ee = {http://link.springer.de/link/service/series/0558/bibs/2309/23090132.htm},
  timestamp = {2009.11.05}
}

@INCOLLECTION{DBLP:series/faia/BarrettSST09,
  author = {Clark W. Barrett and Roberto Sebastiani and Sanjit A. Seshia and
	Cesare Tinelli},
  title = {Satisfiability Modulo Theories},
  booktitle = HOS,
  publisher = {{IOS} Press},
  year = {2009},
  pages = {825--885},
  ee = {http://dx.doi.org/10.3233/978-1-58603-929-5-825},
  timestamp = {2009.11.05}
}

@MISC{WWW:Bartak98,
  author = {Roman Bart\'{a}k},
  title = {On-line Guide to Constraint Programming},
  howpublished = {{\tt http://kti.ms.mff.cuni.cz\slash\~{}bartak\slash constraints/}},
  year = {1998},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/ai/BaumgartnerT08,
  author = {Peter Baumgartner and Cesare Tinelli},
  title = {The Model Evolution Calculus as a First-order {DPLL} Method},
  journal = AI,
  year = {2008},
  volume = {172},
  pages = {591--632},
  number = {4-5},
  ee = {http://dx.doi.org/10.1016/j.artint.2007.09.005},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/aaai/Pehoushek00,
  author = {Roberto J. {Bayardo Jr.} and Joseph Daniel Pehoushek},
  title = {Counting Models Using Connected Components},
  booktitle = AAAI-2000,
  year = {2000},
  pages = {157--162},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/aaai/BayardoS97,
  author = {Roberto J. {Bayardo Jr.} and Robert Schrag},
  title = {Using {CSP} Look-Back Techniques to Solve Real-World {SAT} Instances},
  booktitle = AAAI-1997,
  year = {1997},
  pages = {203--208},
  timestamp = {2009.11.03}
}

@ARTICLE{ORS:Beasley90,
  author = {J. E. Beasley},
  title = {{OR}-Library: Distributing Test Problems by Electronic Mail},
  journal = {Operational Research Society},
  year = {1990},
  volume = {41},
  pages = {1069--1072},
  no = {11},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/sat/BessiereHW03,
  author = {Christian Bessi{\`e}re and Emmanuel Hebrard and Toby Walsh},
  title = {Local Consistencies in {SAT}},
  booktitle = SAT-2003,
  year = {2003},
  pages = {299--314},
  timestamp = {2009.11.03}
}

@INCOLLECTION{DBLP:series/faia/Biere09,
  author = {Armin Biere},
  title = {Bounded Model Checking},
  booktitle = HOS,
  publisher = {{IOS} Press},
  year = {2009},
  pages = {457--481},
  ee = {http://dx.doi.org/10.3233/978-1-58603-929-5-457},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/tacas/BiereCCZ99,
  author = {Armin Biere and Alessandro Cimatti and Edmund M. Clarke and Yunshan
	Zhu},
  title = {Symbolic Model Checking without {BDDs}},
  booktitle = TACAS-1999,
  year = {1999},
  pages = {193--207},
  ee = {http://link.springer.de/link/service/series/0558/bibs/1579/15790193.htm},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/jair/BirnbaumL99,
  author = {Elazar Birnbaum and Eliezer L. Lozinskii},
  title = {The Good Old Davis-Putnam Procedure Helps Counting Models},
  journal = JAIR,
  year = {1999},
  volume = {10},
  pages = {457--477},
  ee = {http://www.cs.washington.edu/research/jair/abstracts/birnbaum99a.html},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/ai/BlumF97,
  author = {Avrim Blum and Merrick L. Furst},
  title = {Fast Planning Through Planning Graph Analysis},
  journal = AI,
  year = {1997},
  volume = {90},
  pages = {281--300},
  number = {1-2},
  ee = {http://dx.doi.org/10.1016/S0004-3702(96)00047-1},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/ai/BonetG01,
  author = {Blai Bonet and Hector Geffner},
  title = {Planning as Heuristic Search},
  journal = AI,
  year = {2001},
  volume = {129},
  pages = {5--33},
  number = {1-2},
  ee = {http://dx.doi.org/10.1016/S0004-3702(01)00108-4},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/csur/BordeauxHZ06,
  author = {Lucas Bordeaux and Youssef Hamadi and Lintao Zhang},
  title = {Propositional Satisfiability and Constraint Programming: A Comparative
	Survey},
  journal = ACMCS,
  year = {2006},
  volume = {38},
  number = {4},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/jair/Brafman01,
  author = {Ronen I. Brafman},
  title = {On Reachability, Relevance, and Resolution in the Planning as Satisfiability
	Approach},
  journal = JAIR,
  year = {2001},
  volume = {14},
  pages = {1--28},
  ee = {http://www.cs.washington.edu/research/jair/abstracts/brafman01a.html},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/rsa/BraunsteinMZ05,
  author = {Alfredo Braunstein and Marc M{\'e}zard and Riccardo Zecchina},
  title = {Survey Propagation: An Algorithm for Satisfiability},
  journal = {Random Structures \& Algorithms},
  year = {2005},
  volume = {27},
  pages = {201--226},
  number = {2},
  ee = {http://dx.doi.org/10.1002/rsa.20057},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/tableaux/BryY96,
  author = {Fran\c{c}ois Bry and Adnan H. Yahya},
  title = {Minimal Model Generation with Positive Unit Hyper-Resolution Tableaux},
  booktitle = TABLEAUX-1996,
  year = {1996},
  pages = {143--159},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/tocl/BryantGV01,
  author = {Randal E. Bryant and Steven M. German and Miroslav N. Velev},
  title = {Processor Verification Using Efficient Reductions of the Logic of
	Uninterpreted Functions to Propositional Logic},
  journal = ACM-TOCL,
  year = {2001},
  volume = {2},
  pages = {93--134},
  number = {1},
  ee = {http://doi.acm.org/10.1145/371282.371364},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/amai/BohmS96,
  author = {Max B{\"o}hm and Ewald Speckenmeyer},
  title = {A Fast Parallel {SAT}-Solver - Efficient Workload Balancing},
  journal = AMAI,
  year = {1996},
  volume = {17},
  pages = {381--400},
  number = {3-4},
  timestamp = {2009.11.03}
}

@BOOK{BOOK:ChangL71,
  title = {Symbolic Logic and Mechanical Theorem Proving},
  publisher = {Academic Press},
  year = {1971},
  author = {Chin-Liang Chang and Richard Char-Tung Lee},
  timestamp = {2009.11.05}
}

@ARTICLE{JCD:ChateauneufCK02,
  author = {M. A. Chateauneuf and Donald L. Kreher},
  title = {On the State of Strength-Three Covering Arrays},
  journal = {Journal of Combinatorial Designs},
  year = {2002},
  volume = {10},
  pages = {217--238},
  number = {4},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/ai/ChenHXZ09,
  author = {Yixin Chen and Ruoyun Huang and Zhao Xing and Weixiong Zhang},
  title = {Long-distance Mutual Exclusion for Planning},
  journal = AI,
  year = {2009},
  volume = {173},
  pages = {365--391},
  number = {2},
  ee = {http://dx.doi.org/10.1016/j.artint.2008.11.004},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{IPC6:ChenL08,
  author = {Yixin Chen and Qiang Lv},
  title = {Plan-{A}: A Cost Optimal Planner Based on {SAT}-Constrained Optimization},
  booktitle = IPC-6,
  year = {2008},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ausai/ChoiHLS06,
  author = {Chiu Wo Choi and Warwick Harvey and J. H. M. Lee and Peter J. Stuckey},
  title = {Finite Domain Bounds Consistency Revisited},
  booktitle = AUSAI-2006,
  year = {2006},
  pages = {49--58},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/jsat/ChuHS09,
  author = {Geoffrey Chu and Aaron Harwood and Peter J. Stuckey},
  title = {Cache Conscious Data Structures for Boolean Satisfiability Solvers},
  journal = JSAT,
  year = {2009},
  volume = {6},
  pages = {99--120},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/jlp/CodognetD96,
  author = {Philippe Codognet and Daniel Diaz},
  title = {Compiling Constraints in {clp(FD)}},
  journal = JLP,
  year = {1996},
  volume = {27},
  pages = {185--226},
  number = {3},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/tse/CohenDFP97,
  author = {David M. Cohen and Siddhartha R. Dalal and Michael L. Fredman and
	Gardner C. Patton},
  title = {The {AETG} System: An Approach to Testing Based on Combinatiorial
	Design},
  journal = IEEE-TSE,
  year = {1997},
  volume = {23},
  pages = {437--444},
  number = {7},
  ee = {http://www.computer.org/tse/ts1997/e0437abs.htm},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/icse/CohenGMC03,
  author = {Myra B. Cohen and Peter B. Gibbons and Warwick B. Mugridge and Charles
	J. Colbourn},
  title = {Constructing Test Suites for Interaction Testing},
  booktitle = ICSE-2003,
  year = {2003},
  pages = {38--48},
  ee = {http://computer.org/proceedings/icse/1877/18770038abs.htm},
  timestamp = {2009.11.03}
}

@MISC{WWW:Colbourn09,
  author = {Charles J. Colbourn},
  title = {Covering Array Tables for t=2,3,4,5,6},
  howpublished = {{\tt http://www.public.asu.edu\slash\~{}ccolbou\slash src\slash tabby\slash
	catable.html}},
  year = {2009},
  note = {Last Accessed on Oct 11 2009},
  timestamp = {2009.11.03}
}

@ARTICLE{LM:Colbourn04,
  author = {Charles J. Colbourn},
  title = {Combinatorial Aspects of Covering Arrays},
  journal = {Le Matematiche (Catania)},
  year = {2004},
  volume = {58},
  pages = {121--167},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/stoc/Cook71,
  author = {Stephen A. Cook},
  title = {The Complexity of Theorem-Proving Procedures},
  booktitle = {Proceedings of the 3rd Annual {ACM} Symposium on Theory of Computing
	({STOC} 1971)},
  year = {1971},
  pages = {151--158},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/ai/CrawfordA96,
  author = {James M. Crawford and Larry D. Auton},
  title = {Experimental Results on the Crossover Point in Random 3-{SAT}},
  journal = AI,
  year = {1996},
  volume = {81},
  pages = {31--57},
  number = {1-2},
  ee = {http://dx.doi.org/10.1016/0004-3702(95)00046-1},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/aaai/CrawfordB94,
  author = {James M. Crawford and Andrew B. Baker},
  title = {Experimental Results on the Application of Satisfiability Algorithms
	to Scheduling Problems},
  booktitle = AAAI-1994,
  year = {1994},
  pages = {1092--1097},
  timestamp = {2009.11.03}
}

@INCOLLECTION{DBLP:series/faia/DantsinH09,
  author = {Evgeny Dantsin and Edward A. Hirsch},
  title = {Worst-Case Upper Bounds},
  booktitle = HOS,
  publisher = {{IOS} Press},
  year = {2009},
  pages = {403--424},
  ee = {http://dx.doi.org/10.3233/978-1-58603-929-5-403},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/ecai/Darwiche04,
  author = {Adnan Darwiche},
  title = {New Advances in Compiling {CNF} into Decomposable Negation Normal
	Form},
  booktitle = ECAI-2004,
  year = {2004},
  pages = {328--332},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/jacm/Darwiche01,
  author = {Adnan Darwiche},
  title = {Decomposable Negation Normal Form},
  journal = JACM,
  year = {2001},
  volume = {48},
  pages = {608--647},
  number = {4},
  ee = {http://doi.acm.org/10.1145/502090.502091},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/aaai/DaviesB07,
  author = {Jessica Davies and Fahiem Bacchus},
  title = {Using More Reasoning to Improve {\#SAT} Solving},
  booktitle = AAAI-2007,
  year = {2007},
  pages = {185--190},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/cacm/DavisLL62,
  author = {Martin Davis and George Logemann and Donald W. Loveland},
  title = {A Machine Program for Theorem-Proving},
  journal = CACM,
  year = {1962},
  volume = {5},
  pages = {394--397},
  number = {7},
  ee = {http://doi.acm.org/10.1145/368273.368557},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/jacm/DavisP60,
  author = {Martin Davis and Hilary Putnam},
  title = {A Computing Procedure for Quantification Theory},
  journal = JACM,
  year = {1960},
  volume = {7},
  pages = {201--215},
  number = {3},
  ee = {http://doi.acm.org/10.1145/321033.321034},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/ai/DechterF02,
  author = {Rina Dechter and Daniel Frost},
  title = {Backjump-based Backtracking for Constraint Satisfaction Problems},
  journal = AI,
  year = {2002},
  volume = {136},
  pages = {147--188},
  number = {2},
  ee = {http://dx.doi.org/10.1016/S0004-3702(02)00120-0},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/jar/DequenD06,
  author = {Gilles Dequen and Olivier Dubois},
  title = {An Efficient Approach to Solving Random k-sat Problems},
  journal = JAR,
  year = {2006},
  volume = {37},
  pages = {261--276},
  number = {4},
  ee = {http://dx.doi.org/10.1007/s10817-006-9025-2},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ecp/DimopoulosNK97,
  author = {Yannis Dimopoulos and Bernhard Nebel and Jana Koehler},
  title = {Encoding Planning Problems in Nonmonotonic Logic Programs},
  booktitle = ECP-1997,
  year = {1997},
  pages = {169--181},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/cp/DimopoulosS06,
  author = {Yannis Dimopoulos and Kostas Stergiou},
  title = {Propagation in {CSP} and {SAT}},
  booktitle = CP-2006,
  year = {2006},
  pages = {137--151},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{CSC06:DongenLR08,
  author = {M. R. C. van Dongen and Christophe Lecoutre and Olivier Roussel},
  title = {Results of the Second {CSP} Solver Competition},
  booktitle = CSC-2006,
  year = {2008},
  pages = {1--10},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/jacm/DowneyS78,
  author = {Peter J. Downey and Ravi Sethi},
  title = {Assignment Commands with Array References},
  journal = JACM,
  year = {1978},
  volume = {25},
  pages = {652--666},
  number = {4},
  ee = {db/journals/jacm/DowneyS78.html, http://doi.acm.org/10.1145/322092.322104},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/jacm/DowneyST80,
  author = {Peter J. Downey and Ravi Sethi and Robert Endre Tarjan},
  title = {Variations on the Common Subexpression Problem},
  journal = JACM,
  year = {1980},
  volume = {27},
  pages = {758--771},
  number = {4},
  ee = {db/journals/jacm/DowneyST80.html, http://doi.acm.org/10.1145/322217.322228},
  timestamp = {2009.11.05}
}

@BOOK{BOOK:Drechsler09,
  title = {Test Pattern Generation using Boolean Proof Engines},
  publisher = {Springer},
  year = {2009},
  author = {Rolf Drechsler and Stephan Eggersgl{\"u}{\ss} and G{\"o}rschwin Fey
	and Daniel Tille},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/aaai/EglyETW00,
  author = {Uwe Egly and Thomas Eiter and Hans Tompits and Stefan Woltran},
  title = {Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas},
  booktitle = AAAI-2000,
  year = {2000},
  pages = {417--422},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ijcai/ErnstMW97,
  author = {Michael D. Ernst and Todd D. Millstein and Daniel S. Weld},
  title = {Automatic {SAT}-Compilation of Planning Problems},
  booktitle = IJCAI-1997,
  year = {1997},
  pages = {1169--1177},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/jsat/EenS06,
  author = {Niklas E{\'e}n and Niklas S{\"o}rensson},
  title = {Translating Pseudo-{Boolean} Constraints into {SAT}},
  journal = JSAT,
  year = {2006},
  volume = {2},
  pages = {1--26},
  number = {1-4},
  ee = {http://jsat.ewi.tudelft.nl/content/volume2/JSAT2_1_Een.pdf},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{SAT05:EenS05,
  author = {Niklas E{\'e}n and Niklas S{\"o}rensson},
  title = {{MiniSat}: A {SAT} Solver with Conflict-Clause Minimization},
  booktitle = SAT-2005,
  year = {2005},
  pages = {502--518},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/sat/EenS03,
  author = {Niklas E{\'e}n and Niklas S{\"o}rensson},
  title = {An Extensible {SAT}-solver},
  booktitle = SAT-2003,
  year = {2003},
  pages = {502--518},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2919{\&}spage=502},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/entcs/EenS03,
  author = {Niklas E{\'e}n and Niklas S{\"o}rensson},
  title = {Temporal Induction by Incremental {SAT} Solving},
  journal = ENTCS,
  year = {2003},
  volume = {89},
  number = {4},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2919{\&}spage=502},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/cav/FlanaganJOS03,
  author = {Cormac Flanagan and Rajeev Joshi and Xinming Ou and James B. Saxe},
  title = {Theorem Proving Using Lazy Proof Explication},
  booktitle = CAV-2003,
  year = {2003},
  pages = {355--367},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2725{\&}spage=355},
  timestamp = {2009.11.05}
}

@PHDTHESIS{PHD:Freeman95,
  author = {Jon William Freeman},
  title = {Improvements to Propositional Satisfiability Search Algorithms},
  school = {University of Pennsylvania},
  year = {1995},
  address = {Philadelphia, PA, USA},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/cade/Ganzinger02,
  author = {Harald Ganzinger},
  title = {Shostak Light},
  booktitle = CADE-2002,
  year = {2002},
  pages = {332--346},
  ee = {http://link.springer.de/link/service/series/0558/bibs/2392/23920332.htm},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/lics/GanzingerK03,
  author = {Harald Ganzinger and Konstantin Korovin},
  title = {New Directions in Instantiation-Based Theorem Proving},
  booktitle = LICS-2003,
  year = {2003},
  pages = {55--64},
  ee = {http://csdl.computer.org/comp/proceedings/lics/2003/1884/00/18840055abs.htm},
  timestamp = {2009.11.03}
}

@BOOK{BOOK:GareyJ79,
  title = {Computers and Intractability: A Guide to the Theory of {NP}-Completeness},
  publisher = {W. H. Freeman and Company},
  year = {1979},
  author = {Michael R. Garey and David S. Johnson},
  address = {New York},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/cp/Gavanelli07,
  author = {Marco Gavanelli},
  title = {The Log-Support Encoding of {CSP} into {SAT}},
  booktitle = CP-2007,
  year = {2007},
  pages = {815--822},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ijcai/GebserKNS07,
  author = {Martin Gebser and Benjamin Kaufmann and Andr{\'e} Neumann and Torsten
	Schaub},
  title = {Conflict-Driven Answer Set Solving},
  booktitle = IJCAI-2007,
  year = {2007},
  pages = {386-},
  ee = {http://dli.iiit.ac.in/ijcai/IJCAI-2007/PDF/IJCAI07-060.pdf},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/dam/Gelder08,
  author = {Allen Van Gelder},
  title = {Another Look at Graph Coloring via Propositional Satisfiability},
  journal = DAM,
  year = {2008},
  volume = {156},
  pages = {230--243},
  number = {2},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ecai/Gent02,
  author = {Ian P. Gent},
  title = {Arc Consistency in {SAT}},
  booktitle = ECAI-2002,
  year = {2002},
  pages = {121--125},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/ai/GentMN08,
  author = {Ian P. Gent and Ian Miguel and Peter Nightingale},
  title = {Generalised Arc Consistency for the AllDifferent Constraint: An Empirical
	Survey},
  journal = AI,
  year = {2008},
  volume = {172},
  pages = {1973--2000},
  number = {18},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{MODREF04:GentN04,
  author = {I. P. Gent and P. Nightingale},
  title = {A New Encoding of Alldifferent into {SAT}},
  booktitle = ModRef-2004,
  year = {2004},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/aaai/GereviniS98,
  author = {Alfonso Gerevini and Lenhart K. Schubert},
  title = {Inferring State Constraints for Domain-Independent Planning},
  booktitle = AAAI-1998,
  year = {1998},
  pages = {905--912},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/aiia/GiunchigliaM07,
  author = {Enrico Giunchiglia and Marco Maratea},
  title = {{SAT}-Based Planning with Minimal-\#actions Plans and ``soft'' Goals},
  booktitle = AI*IA-2007,
  year = {2007},
  pages = {422--433},
  ee = {http://dx.doi.org/10.1007/978-3-540-74782-6_37},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ecai/GiunchigliaM06,
  author = {Enrico Giunchiglia and Marco Maratea},
  title = {Solving Optimization Problems with {DLL}},
  booktitle = ECAI-2006,
  year = {2006},
  pages = {377--381},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/jelia/GiunchigliaM06,
  author = {Enrico Giunchiglia and Marco Maratea},
  title = {{optsat}: A Tool for Solving {SAT} Related Optimization Problems},
  booktitle = JELIA-2006,
  year = {2006},
  pages = {485--489},
  ee = {http://dx.doi.org/10.1007/11853886_43},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/aaai/GogateD07,
  author = {Vibhav Gogate and Rina Dechter},
  title = {Approximate Counting by Sampling the Backtrack-free Search Space},
  booktitle = AAAI-2007,
  year = {2007},
  pages = {198--203},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/dam/GoldbergN07,
  author = {Eugene Goldberg and Yakov Novikov},
  title = {{BerkMin}: A Fast and Robust {SAT}-solver},
  journal = DAM,
  year = {2007},
  volume = {155},
  pages = {1549--1561},
  number = {12},
  ee = {http://dx.doi.org/10.1016/j.dam.2006.10.007},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ijcai/GomesHSS07,
  author = {Carla P. Gomes and J{\"o}rg Hoffmann and Ashish Sabharwal and Bart
	Selman},
  title = {From Sampling to Model Counting},
  booktitle = IJCAI-2007,
  year = {2007},
  pages = {2293--2299},
  ee = {http://dli.iiit.ac.in/ijcai/IJCAI-2007/PDF/IJCAI07-369.pdf},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/sat/GomesHSS07,
  author = {Carla P. Gomes and J{\"o}rg Hoffmann and Ashish Sabharwal and Bart
	Selman},
  title = {Short {XORs} for Model Counting: From Theory to Practice},
  booktitle = SAT-2007,
  year = {2007},
  pages = {100--106},
  ee = {http://dx.doi.org/10.1007/978-3-540-72788-0_13},
  timestamp = {2009.11.05}
}

@INCOLLECTION{HKR:GomesKSS08,
  author = {Carla P. Gomes and Henry Kautz and Ashish Sabharwal and Bart Selman},
  title = {Satisfiability Solvers},
  booktitle = {Handbook of Knowledge Representation},
  publisher = {Elsevier},
  year = {2008},
  volume = {3},
  series = {Foundations of Artificial Intelligence},
  pages = {89--134},
  editors = {Frank {van Harmelen} and Vladimir Lifschitz and Bruce Porter},
  timestamp = {2009.11.03}
}

@INCOLLECTION{DBLP:series/faia/GomesSS09,
  author = {Carla P. Gomes and Ashish Sabharwal and Bart Selman},
  title = {Model Counting},
  booktitle = HOS,
  publisher = {{IOS} Press},
  year = {2009},
  pages = {633--654},
  ee = {http://dx.doi.org/10.3233/978-1-58603-929-5-633},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/ai/GomesS01,
  author = {Carla P. Gomes and Bart Selman},
  title = {Algorithm Portfolios},
  journal = AI,
  year = {2001},
  volume = {126},
  pages = {43--62},
  number = {1-2},
  ee = {http://dx.doi.org/10.1016/S0004-3702(00)00081-3},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/cp/GomesSC97,
  author = {Carla P. Gomes and Bart Selman and Nuno Crato},
  title = {Heavy-Tailed Distributions in Combinatorial Search},
  booktitle = CP-1997,
  year = {1997},
  pages = {121--135},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/jar/GomesSCK00,
  author = {Carla P. Gomes and Bart Selman and Nuno Crato and Henry A. Kautz},
  title = {Heavy-Tailed Phenomena in Satisfiability and Constraint Satisfaction
	Problems},
  journal = JAR,
  year = {2000},
  volume = {24},
  pages = {67--100},
  number = {1/2},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/aaai/GomesSK98,
  author = {Carla P. Gomes and Bart Selman and Henry A. Kautz},
  title = {Boosting Combinatorial Search Through Randomization},
  booktitle = AAAI-1998,
  year = {1998},
  pages = {431--437},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/jair/GroveHK94,
  author = {Adam J. Grove and Joseph Y. Halpern and Daphne Koller},
  title = {Random Worlds and Maximum Entropy},
  journal = JAIR,
  year = {1994},
  volume = {2},
  pages = {33--88},
  timestamp = {2009.11.05}
}

@ARTICLE{AOR:GueretP99,
  author = {Christelle Gu{\'e}ret and Christian Prins},
  title = {A New Lower Bound for the Open-shop Problem},
  journal = {Annals of Operations Research},
  year = {1999},
  volume = {92},
  pages = {165--183},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/dm/HartmanR04,
  author = {Alan Hartman and Leonid Raskin},
  title = {Problems and Algorithms for Covering Arrays},
  journal = {Discrete Mathematics},
  year = {2004},
  volume = {284},
  pages = {149--156},
  number = {1-3},
  ee = {http://dx.doi.org/10.1016/j.disc.2003.11.029},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/cade/HasegawaFK00,
  author = {Ryuzo Hasegawa and Hiroshi Fujita and Miyuki Koshimura},
  title = {Efficient Minimal Model Generation Using Branching Lemmas},
  booktitle = {CADE},
  year = {2000},
  pages = {184--199},
  ee = {http://dx.doi.org/10.1007/10721959_15},
  timestamp = {2009.11.05}
}

@BOOK{BOOK:Hentenryck99,
  title = {The {OPL} Optimization Programming Language},
  publisher = {MIT Press},
  year = {1999},
  author = {Pascal van Hentenryck},
  timestamp = {2009.11.03}
}

@PHDTHESIS{PHD:Heule08,
  author = {Marijn Heule},
  title = {{SmArT} solving: Tools and Techniques for Satisfiability Solvers},
  school = {Delft University of Technology},
  year = {2008},
  address = {Delft, The Netherlands},
  timestamp = {2009.11.05}
}

@INCOLLECTION{DBLP:series/faia/HeuleM09,
  author = {Marijn Heule and Hans van Maaren},
  title = {Look-Ahead Based {SAT} Solvers},
  booktitle = HOS,
  publisher = {{IOS} Press},
  year = {2009},
  pages = {155--184},
  ee = {http://dx.doi.org/10.3233/978-1-58603-929-5-155},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/csclp/HnichPS04,
  author = {Brahim Hnich and Steven David Prestwich and Evgeny Selensky},
  title = {Constraint-Based Approaches to the Covering Test Problem},
  booktitle = CSCLP-2004,
  year = {2004},
  pages = {172--186},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3419{\&}spage=172},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/constraints/HnichPSS06,
  author = {Brahim Hnich and Steven David Prestwich and Evgeny Selensky and Barbara
	M. Smith},
  title = {Constraint Models for the Covering Test Problem},
  journal = CONSTRAINTS,
  year = {2006},
  volume = {11},
  pages = {199--219},
  number = {2-3},
  ee = {http://dx.doi.org/10.1007/s10601-006-7094-9},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ijcai/HoffmannGSK07,
  author = {J{\"o}rg Hoffmann and Carla P. Gomes and Bart Selman and Henry A.
	Kautz},
  title = {{SAT} Encodings of State-Space Reachability Problems in Numeric Domains},
  booktitle = IJCAI-2007,
  year = {2007},
  pages = {1918--1923},
  ee = {http://dli.iiit.ac.in/ijcai/IJCAI-2007/PDF/IJCAI07-309.pdf},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ijcai/Hoos99,
  author = {Holger H. Hoos},
  title = {{SAT}-Encodings, Search Space Structure, and Local Search Performance},
  booktitle = IJCAI-1999,
  year = {1999},
  pages = {296--303},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/cp/Huang08,
  author = {Jinbo Huang},
  title = {Universal Booleanization of Constraint Models},
  booktitle = CP-2008,
  year = {2008},
  pages = {144--158},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ijcai/Huang07,
  author = {Jinbo Huang},
  title = {The Effect of Restarts on the Efficiency of Clause Learning},
  booktitle = IJCAI-2007,
  year = {2007},
  pages = {2318--2323},
  ee = {http://dli.iiit.ac.in/ijcai/IJCAI-2007/PDF/IJCAI07-373.pdf},
  timestamp = {2009.11.03}
}

@ARTICLE{SCIENCE:HubermanLH97,
  author = {Bernardo A. Huberman and Rajan M. Lukose and Tad Hogg},
  title = {An Economics Approach to Hard Computational Problems},
  journal = {Science},
  year = {1997},
  volume = {275},
  pages = {51--54},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/dam/InoueSUSBT06,
  author = {Katsumi Inoue and Takehide Soh and Seiji Ueda and Yoshito Sasaura
	and Mutsunori Banbara and Naoyuki Tamura},
  title = {A Competitive and Cooperative Approach to Propositional Satisfiability},
  journal = DAM,
  year = {2006},
  volume = {154},
  pages = {2291--2306},
  number = {16},
  ee = {http://dx.doi.org/10.1016/j.dam.2006.04.015},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ifip/IwamaM94,
  author = {Kazuo Iwama and Shuichi Miyazaki},
  title = {{SAT}-Variable Complexity of Hard Combinatorial Problems},
  booktitle = {Proceedings of the IFIP 13th World Computer Congress},
  year = {1994},
  pages = {253--258},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/soda/IwamaT04,
  author = {Kazuo Iwama and Suguru Tamaki},
  title = {Improved upper bounds for 3-{SAT}},
  booktitle = {Proceedings of the 15th ACM-SIAM Symposium on Discrete Algorithms
	(SODA 04)},
  year = {2004},
  pages = {328},
  ee = {http://doi.acm.org/10.1145/982792.982838},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/jlp/JaffarM94,
  author = {Joxan Jaffar and Michael J. Maher},
  title = {Constraint Logic Programming: A Survey},
  journal = JLP,
  year = {1994},
  volume = {19/20},
  pages = {503--581},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/dac/JainC09,
  author = {Himanshu Jain and Edmund M. Clarke},
  title = {Efficient {SAT} Solving for Non-Clausal Formulas using {DPLL}, Graphs,
	and Watched Cuts},
  booktitle = {Proceedings of the 46th Design Automation Conference (DAC 2009)},
  year = {2009},
  pages = {563--568},
  ee = {http://doi.acm.org/10.1145/1629911.1630057},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/tacas/JinHS05,
  author = {HoonSang Jin and HyoJung Han and Fabio Somenzi},
  title = {Efficient Conflict Analysis for Finding All Satisfying Assignments
	of a {Boolean} Circuit},
  booktitle = TACAS-2005,
  year = {2005},
  pages = {287--300},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3440{\&}spage=287},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/combinatorica/Karmarkar84,
  author = {Narendra Karmarkar},
  title = {A New Polynomial-time Algorithm for Linear Programming},
  journal = {Combinatorica},
  year = {1984},
  volume = {4},
  pages = {373--396},
  number = {4},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/ai/Kasif90,
  author = {Simon Kasif},
  title = {On the Parallel Complexity of Discrete Relaxation in Constraint Satisfaction
	Networks},
  journal = AI,
  year = {1990},
  volume = {45},
  pages = {275--286},
  number = {3},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/aaai/KautzHRGS02,
  author = {Henry A. Kautz and Eric Horvitz and Yongshao Ruan and Carla P. Gomes
	and Bart Selman},
  title = {Dynamic Restart Policies},
  booktitle = AAAI-2002,
  year = {2002},
  pages = {674--681},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ijcai/KautzS99,
  author = {Henry A. Kautz and Bart Selman},
  title = {Unifying {SAT}-based and Graph-based Planning},
  booktitle = IJCAI-1999,
  year = {1999},
  pages = {318--325},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/aips/KautzS98,
  author = {Henry A. Kautz and Bart Selman},
  title = {The Role of Domain-Specific Knowledge in the Planning as Satisfiability
	Framework},
  booktitle = AIPS-1998,
  year = {1998},
  pages = {181--189},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/aaai/KautzS96,
  author = {Henry A. Kautz and Bart Selman},
  title = {Pushing the Envelope: Planning, Propositional Logic and Stochastic
	Search},
  booktitle = AAAI-1996,
  year = {1996},
  pages = {1194--1201},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ecai/KautzS92,
  author = {Henry A. Kautz and Bart Selman},
  title = {Planning as Satisfiability},
  booktitle = ECAI-1992,
  year = {1992},
  pages = {359--363},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{AIPS98:KautzS98,
  author = {Henry Kautz and Bart Selman},
  title = {{BLACKBOX}: A New Approach to the Application of Theorem Proving
	to Problem Solving},
  booktitle = {AIPS98 Workshop on Planning as Combinatorial Search},
  year = {1998},
  pages = {58--60},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{IPC5:KautzSH06,
  author = {Henry Kautz and Bart Selman and J\"{o}erg Hoffmann},
  title = {{SatPlan}: Planning as Satisfiability},
  booktitle = IPC-5,
  year = {2006},
  timestamp = {2009.11.03}
}

@ARTICLE{TIPSJ:KoshimuraIH03,
  author = {Miyuki Koshimura and Megumi Iwaki and Ryuzo Hasegawa},
  title = {Minimal Model Generation with Factorization and Constrained Search},
  journal = TIPSJ,
  year = {2003},
  volume = {44},
  pages = {1163--1172},
  number = {4},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/cpaior/KrocSS08,
  author = {Lukas Kroc and Ashish Sabharwal and Bart Selman},
  title = {Leveraging Belief Propagation, Backtrack Search, and Statistics for
	Model Counting},
  booktitle = {CPAIOR},
  year = {2008},
  pages = {127--141},
  ee = {http://dx.doi.org/10.1007/978-3-540-68155-7_12},
  timestamp = {2009.11.05}
}

@TECHREPORT{TR:Kullmann02,
  author = {Oliver Kullmann},
  title = {Investigating the Behaviour of a {SAT} Solver on Random Formulas},
  institution = {University of Wales Swansea},
  year = {2002},
  type = {Tech. Report CSR 23-2002, Computer Science Report Series},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/cav/LahiriS04,
  author = {Shuvendu K. Lahiri and Sanjit A. Seshia},
  title = {The {UCLID} Decision Procedure},
  booktitle = CAV-2004,
  year = {2004},
  pages = {475--478},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3114{\&}spage=475},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/hase/LeiT98,
  author = {Yu Lei and Kuo-Chung Tai},
  title = {In-Parameter-Order: A Test Generation Strategy for Pairwise Testing},
  booktitle = {Proceedings of 3rd IEEE International Symposium on High-Assurance
	Systems Engineering (HASE 1998)},
  year = {1998},
  pages = {254--261},
  ee = {http://www.computer.org/proceedings/hase/9221/92210254abs.htm},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/jar/LetzMG94,
  author = {Reinhold Letz and Klaus Mayr and Christoph Goller},
  title = {Cotrolled Integration of the Cut Rule into Connection Tableaux Calculi},
  journal = JAR,
  year = {1994},
  volume = {13},
  pages = {297--337},
  number = {3},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/cp/LiA97,
  author = {Chu Min Li and Anbulagan},
  title = {Look-Ahead Versus Look-Back for Satisfiability Problems},
  booktitle = CP-1997,
  year = {1997},
  pages = {341--355},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ijcai/LiA97,
  author = {Chu Min Li and Anbulagan},
  title = {Heuristics Based on Unit Propagation for Satisfiability Problems.},
  booktitle = IJCAI-1997,
  year = {1997},
  pages = {366--371},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/ipl/LubySZ93,
  author = {Michael Luby and Alistair Sinclair and David Zuckerman},
  title = {Optimal Speedup of {Las} {Vegas} Algorithms},
  journal = {Information Processing Letters},
  year = {1993},
  volume = {47},
  pages = {173--180},
  number = {4},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/cacm/MalikZ09,
  author = {Sharad Malik and Lintao Zhang},
  title = {Boolean Satisfiability from Theoretical Hardness to Practical Success},
  journal = CACM,
  year = {2009},
  volume = {52},
  pages = {76--82},
  number = {8},
  ee = {http://doi.acm.org/10.1145/1536616.1536637},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/unu/MannaZ02,
  author = {Zohar Manna and Calogero G. Zarba},
  title = {Combining Decision Procedures},
  booktitle = {Formal Methods at the Crossroads. From Panacea to Foundational Support,
	LNCS 2757},
  year = {2002},
  pages = {381--422},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2757{\&}spage=381},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/jar/Maric09,
  author = {Filip Maric},
  title = {Formalization and Implementation of Modern {SAT} Solvers},
  journal = JAR,
  year = {2009},
  volume = {43},
  pages = {81--119},
  number = {1},
  ee = {http://dx.doi.org/10.1007/s10817-009-9127-8},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/tc/Marques-SilvaS99,
  author = {Jo{\~a}o P. Marques-Silva and Karem A. Sakallah},
  title = {{GRASP}: A Search Algorithm for Propositional Satisfiability},
  journal = {IEEE Transactions on Computers},
  year = {1999},
  volume = {48},
  pages = {506--521},
  number = {5},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/cav/McMillan02,
  author = {Kenneth L. McMillan},
  title = {Applying {SAT} Methods in Unbounded Symbolic Model Checking},
  booktitle = CAV-2002,
  year = {2002},
  pages = {250--264},
  ee = {http://link.springer.de/link/service/series/0558/bibs/2404/24040250.htm},
  timestamp = {2009.11.05}
}

@ARTICLE{JCD:MeagherS05,
  author = {Karen Meagher and Brett Stevens},
  title = {Group Construction of Covering Arrays},
  journal = {Journal of Combinatorial Designs},
  year = {2005},
  volume = {13},
  pages = {70--77},
  number = {1},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ictai/MorgadoS05,
  author = {Ant{\'o}nio Morgado and Jo{\~a}o P. Marques Silva},
  title = {Good Learning and Implicit Model Enumeration},
  booktitle = ICTAI-2005,
  year = {2005},
  pages = {131--136},
  ee = {http://doi.ieeecomputersociety.org/10.1109/ICTAI.2005.69},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/dac/MoskewiczMZZM01,
  author = {Matthew W. Moskewicz and Conor F. Madigan and Ying Zhao and Lintao
	Zhang and Sharad Malik},
  title = {{Chaff}: Engineering an Efficient {SAT} Solver},
  booktitle = DAC-2001,
  year = {2001},
  pages = {530--535},
  ee = {http://jamaica.ee.pitt.edu/Archives/ProceedingArchives/Dac/Dac2001/papers/2001/dac01/pdffiles/33_1.pdf},
  timestamp = {2009.11.03}
}

@ARTICLE{SCIENCE:MezardPZ02,
  author = {M. M{\'e}zard and G. Parisi and R. Zecchina},
  title = {Analytic and Algorithmic Solution of Random Satisfiability Problems},
  journal = {Science},
  year = {2002},
  volume = {297},
  pages = {812--815},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ausai/NabeshimaII02,
  author = {Hidetomo Nabeshima and Koji Iwanuma and Katsumi Inoue},
  title = {Effective {SAT} Planning by Speculative Computation},
  booktitle = AUSAI-2002,
  year = {2002},
  pages = {726--727},
  ee = {http://link.springer.de/link/service/series/0558/bibs/2557/25570726.htm},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/aips/NabeshimaSII06,
  author = {Hidetomo Nabeshima and Takehide Soh and Katsumi Inoue and Koji Iwanuma},
  title = {Lemma Reusing for {SAT} based Planning and Scheduling},
  booktitle = ICAPS-2006,
  year = {2006},
  pages = {103--112},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{ACM-CM:Nelson84,
  author = {G. Nelson},
  title = {Combining Satisfiability Procedures by Equality Sharing},
  booktitle = {Automated Theorem Proving: After 25 years},
  year = {1984},
  volume = {29},
  series = {Contemporary Mathematics},
  pages = {201--211},
  publisher = {American Mathematical Society},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/jacm/NelsonO80,
  author = {Greg Nelson and Derek C. Oppen},
  title = {Fast Decision Procedures Based on Congruence Closure},
  journal = JACM,
  year = {1980},
  volume = {27},
  pages = {356--364},
  number = {2},
  ee = {db/journals/jacm/NelsonO80.html, http://doi.acm.org/10.1145/322186.322198},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/toplas/NelsonO79,
  author = {Greg Nelson and Derek C. Oppen},
  title = {Simplification by Cooperating Decision Procedures},
  journal = ACM-TOPLAS,
  year = {1979},
  volume = {1},
  pages = {245--257},
  number = {2},
  ee = {http://doi.acm.org/10.1145/357073.357079},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/tableaux/Niemela96,
  author = {Ilkka Niemel{\"a}},
  title = {A Tableau Calculus for Minimal Model Reasoning},
  booktitle = TABLEAUX-1996,
  year = {1996},
  pages = {278--294},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/cav/NieuwenhuisO05,
  author = {Robert Nieuwenhuis and Albert Oliveras},
  title = {{DPLL(T)} with Exhaustive Theory Propagation and Its Application
	to Difference Logic},
  booktitle = CAV-2005,
  year = {2005},
  pages = {321--334},
  ee = {http://dx.doi.org/10.1007/11513988_33},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/rta/NieuwenhuisO05,
  author = {Robert Nieuwenhuis and Albert Oliveras},
  title = {Proof-Producing Congruence Closure},
  booktitle = RTA-2005,
  year = {2005},
  pages = {453--468},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3467{\&}spage=453},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/jacm/NieuwenhuisOT06,
  author = {Robert Nieuwenhuis and Albert Oliveras and Cesare Tinelli},
  title = {Solving {SAT} and {SAT} Modulo Theories: From an Abstract {Davis}-{Putnam}-{Logemann}-{Loveland}
	Procedure to {DPLL(T)}},
  journal = JACM,
  year = {2006},
  volume = {53},
  pages = {937--977},
  number = {6},
  ee = {http://doi.acm.org/10.1145/1217856.1217859},
  timestamp = {2009.11.03}
}

@INCOLLECTION{DBLP:books/el/RV01/NieuwenhuisR01,
  author = {Robert Nieuwenhuis and Albert Rubio},
  title = {Paramodulation-Based Theorem Proving},
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier and MIT Press},
  year = {2001},
  pages = {371--443},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/dam/Nurmela04,
  author = {Kari J. Nurmela},
  title = {Upper Bounds for Covering Arrays by Tabu Search},
  journal = DAM,
  year = {2004},
  volume = {138},
  pages = {143--152},
  number = {1-2},
  ee = {http://dx.doi.org/10.1016/S0166-218X(03)00291-9},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/jacm/Oppen80,
  author = {Derek C. Oppen},
  title = {Reasoning About Recursively Defined Data Structures},
  journal = JACM,
  year = {1980},
  volume = {27},
  pages = {403--411},
  number = {3},
  ee = {db/journals/jacm/Oppen80.html, http://doi.acm.org/10.1145/322203.322204},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/tcs/Oppen80,
  author = {Derek C. Oppen},
  title = {Complexity, Convexity and Combinations of Theories},
  journal = TCS,
  year = {1980},
  volume = {12},
  pages = {291--302},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/jcss/Oppen78,
  author = {Derek C. Oppen},
  title = {A $2^{2^{2^{pn}}}$ Upper Bound on the Complexity of Presburger Arithmetic},
  journal = JCSS,
  year = {1978},
  volume = {16},
  pages = {323--332},
  number = {3},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/jacm/Papadimitriou81,
  author = {Christos H. Papadimitriou},
  title = {On the Complexity of Integer Programming},
  journal = JACM,
  year = {1981},
  volume = {28},
  pages = {765--768},
  number = {4},
  ee = {db/journals/jacm/Papadimitriou81.html, http://doi.acm.org/10.1145/322276.322287},
  timestamp = {2009.11.05}
}

@BOOK{BOOK:Peral88,
  title = {Probabilistic Reasoning in Intelligent Systems: Networks of Plausible
	Inference},
  publisher = {Morgan Kaufmann},
  year = {1988},
  author = {Judea Pearl},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ijcai/PhamTS07,
  author = {Duc Nghia Pham and John Thornton and Abdul Sattar},
  title = {Building Structure into Local Search for {SAT}},
  booktitle = IJCAI-2007,
  year = {2007},
  pages = {2359--2364},
  ee = {http://dli.iiit.ac.in/ijcai/IJCAI-2007/PDF/IJCAI07-380.pdf},
  timestamp = {2009.11.03}
}

@TECHREPORT{TR:PipatsrisawatD07,
  author = {Knot Pipatsrisawat and Adnan Darwiche},
  title = {{RSat} 2.0: {SAT} Solver Description},
  institution = {Automated Reasoning Group, Computer Science Department, UCLA},
  year = {2007},
  number = {D-153},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/jar/PlaistedZ00,
  author = {David A. Plaisted and Yunshan Zhu},
  title = {Ordered Semantic Hyper-Linking},
  journal = JAR,
  year = {2000},
  volume = {25},
  pages = {167--217},
  number = {3},
  timestamp = {2009.11.03}
}

@INCOLLECTION{DBLP:series/faia/Prestwich09,
  author = {Steven David Prestwich},
  title = {{CNF} Encodings},
  booktitle = HOS,
  publisher = {{IOS} Press},
  year = {2009},
  pages = {75--97},
  ee = {http://dx.doi.org/10.3233/978-1-58603-929-5-75},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/sat/Prestwich07,
  author = {Steven David Prestwich},
  title = {Variable Dependency in Local Search: Prevention Is Better Than Cure},
  booktitle = SAT-2007,
  year = {2007},
  pages = {107--120},
  ee = {http://dx.doi.org/10.1007/978-3-540-72788-0_14},
  timestamp = {2009.11.03}
}

@INBOOK{TCP:Prestwich07,
  chapter = {15: Finding Large Cliques Using {SAT} Local Search},
  pages = {269--274},
  title = {Trends in Constraint Programming},
  publisher = {ISTE},
  year = {2007},
  author = {Steven David Prestwich},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/sat/Prestwich03,
  author = {Steven David Prestwich},
  title = {Local Search on {SAT}-encoded Colouring Problem},
  booktitle = SAT-2003,
  year = {2003},
  pages = {105--119},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DIMACS2:Pretolani93,
  author = {Daniele Pretolani},
  title = {Efficiency and Stability of Hypergraph {SAT} Algorithms},
  booktitle = {Proceedings of the Second DIMACS Implementation Challenge},
  year = {1993},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/cade/PerezV07,
  author = {Juan Antonio Navarro P{\'e}rez and Andrei Voronkov},
  title = {Encodings of Bounded {LTL} Model Checking in Effectively Propositional
	Logic},
  booktitle = CADE-2007,
  year = {2007},
  pages = {346--361},
  ee = {http://dx.doi.org/10.1007/978-3-540-73595-3_24},
  timestamp = {2009.11.05}
}

@ARTICLE{IEEE-ISM:RaniseT06,
  author = {Silvio Ranise and Cesare Tinelli},
  title = {Satisfiability Modulo Theories},
  journal = {Trends and Controversies - IEEE Intelligence Systems Magazine},
  year = {2006},
  volume = {21},
  pages = {71--81},
  number = {6},
  timestamp = {2009.11.05}
}

@INCOLLECTION{DBLP:series/faia/Rintanen09,
  author = {Jussi Rintanen},
  title = {Planning and {SAT}},
  booktitle = HOS,
  publisher = {{IOS} Press},
  year = {2009},
  pages = {483--504},
  ee = {http://dx.doi.org/10.3233/978-1-58603-929-5-483},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ecai/Rintanen08,
  author = {Jussi Rintanen},
  title = {Regression for Classical and Nondeterministic Planning},
  booktitle = ECAI-2008,
  year = {2008},
  pages = {568--572},
  ee = {http://dx.doi.org/10.3233/978-1-58603-891-5-568},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/kr/Rintanen98,
  author = {Jussi Rintanen},
  title = {A Planning Algorithm not based on Directional Search},
  booktitle = KR-1998,
  year = {1998},
  pages = {617--625},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/ai/RintanenHN06,
  author = {Jussi Rintanen and Keijo Heljanko and Ilkka Niemel{\"a}},
  title = {Planning as Satisfiability: Parallel Plans and Algorithms for Plan
	Search},
  journal = AI,
  year = {2006},
  volume = {170},
  pages = {1031--1080},
  number = {12-13},
  ee = {http://dx.doi.org/10.1016/j.artint.2006.08.002},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/jacm/Robinson65,
  author = {John Alan Robinson},
  title = {A Machine-Oriented Logic Based on the Resolution Principle},
  journal = JACM,
  year = {1965},
  volume = {12},
  pages = {23--41},
  number = {1},
  ee = {db/journals/jacm/Robinson65.html, http://doi.acm.org/10.1145/321250.321253},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{IPC6:RobinsonGP08,
  author = {Nathan Robinson and Charles Gretton and Duc-Nghia Pham},
  title = {{CO-PLAN}: Combining {SAT}-Based Planning with Forward-Search},
  booktitle = IPC-6,
  year = {2008},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/ai/Roth96,
  author = {Dan Roth},
  title = {On the Hardness of Approximate Reasoning},
  journal = AI,
  year = {1996},
  volume = {82},
  pages = {273--302},
  number = {1-2},
  ee = {http://dx.doi.org/10.1016/0004-3702(94)00092-1},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/aaai/Regin96,
  author = {Jean-Charles R{\'e}gin},
  title = {Generalized Arc Consistency for Global Cardinality Constraint},
  booktitle = AAAI-1996,
  year = {1996},
  volume = {1},
  pages = {209--215},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/aaai/Regin94,
  author = {Jean-Charles R{\'e}gin},
  title = {A Filtering Algorithm for Constraints of Difference in {CSPs}},
  booktitle = AAAI-1994,
  year = {1994},
  pages = {362--367},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/sat/SangBBKP04,
  author = {Tian Sang and Fahiem Bacchus and Paul Beame and Henry A. Kautz and
	Toniann Pitassi},
  title = {Combining Component Caching and Clause Learning for Effective Model
	Counting},
  booktitle = SAT-2004,
  year = {2004},
  ee = {http://www.satisfiability.org/SAT04/programme/21.pdf},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{AAAI05:SangBK05,
  author = {Tian Sang and Paul Beame and Henry Kautz},
  title = {Solving Bayesian Networks by Weighted Model Counting},
  booktitle = AAAI-2005,
  year = {2005},
  pages = {475--482},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/aaai/SelmanKC94,
  author = {Bart Selman and Henry A. Kautz and Bram Cohen},
  title = {Noise Strategies for Improving Local Search},
  booktitle = AAAI-1994,
  year = {1994},
  pages = {337--343},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DIMACS:SelmanKC96,
  author = {Bart Selman and Henry Kautz and Bram Cohen},
  title = {Local Search Strategies for Satisfiability Testing},
  booktitle = {Cliques, Coloring, and Satisfiability: the Second {DIMACS} Implementation
	Challenge},
  series = {{DIMACS} Series in Discrete Mathematics and Theoretical Computer Science},
  year = {1996},
  editor = {David J. Johnson and Michael A. Trick},
  volume = {26},
  pages = {521--532},
  publisher = {American Mathematical Society}
}

@INPROCEEDINGS{DBLP:conf/aaai/SelmanLM92,
  author = {Bart Selman and Hector J. Levesque and David G. Mitchell},
  title = {A New Method for Solving Hard Satisfiability Problems},
  booktitle = AAAI-1992,
  year = {1992},
  pages = {440--446},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/ai/SelmanML96,
  author = {Bart Selman and David G. Mitchell and Hector J. Levesque},
  title = {Generating Hard Satisfiability Problems},
  journal = AI,
  year = {1996},
  volume = {81},
  pages = {17--29},
  number = {1-2},
  ee = {http://dx.doi.org/10.1016/0004-3702(95)00045-3},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/tit/SeroussiB88,
  author = {Gadiel Seroussi and Nader H. Bshouty},
  title = {Vector Sets for Exhaustive Testing of Logic Circuits},
  journal = IEEE-TIT,
  year = {1988},
  volume = {34},
  pages = {513--522},
  number = {3},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/rta/ShankarR02,
  author = {Natarajan Shankar and Harald Rue{\ss}},
  title = {Combining Shostak Theories},
  booktitle = RTA-2002,
  year = {2002},
  pages = {1--18},
  ee = {http://link.springer.de/link/service/series/0558/bibs/2378/23780001.htm},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/ai/ShinD05,
  author = {Ji-Ae Shin and Ernest Davis},
  title = {Processes and Continuous Change in a {SAT}-based Planner},
  journal = AI,
  year = {2005},
  volume = {166},
  pages = {194--253},
  number = {1-2},
  ee = {http://dx.doi.org/10.1016/j.artint.2005.04.001},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/jacm/Shostak84,
  author = {Robert E. Shostak},
  title = {Deciding Combinations of Theories},
  journal = JACM,
  year = {1984},
  volume = {31},
  pages = {1--12},
  number = {1},
  ee = {http://doi.acm.org/10.1145/2422.322411},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/epia/Silva99,
  author = {Jo{\~a}o P. Marques Silva},
  title = {The Impact of Branching Heuristics in Propositional Satisfiability
	Algorithms},
  booktitle = {Proceedings of the 9th Portuguese Conference on Artificial Intelligence
	(EPIA 1999), LNCS 1695},
  year = {1999},
  pages = {62--74},
  timestamp = {2009.11.03}
}

@ARTICLE{JCD:Sloane93,
  author = {N. J. A. Sloane},
  title = {Covering Arrays and Intersecting Codes},
  journal = {Journal of Combinatorial Designs},
  year = {1993},
  volume = {1},
  pages = {51--63},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DSCP05:SohIBT05,
  author = {Takehide Soh and Katsumi Inoue and Mutsunori Banbara and Naoyuki
	Tamura},
  title = {Experimental Results for Solving Job-Shop Scheduling Problems with
	Multiple {SAT} Solvers},
  booktitle = {Proceedings of the 1st International Workshop on Distributed and
	Speculative Constraint Processing (DSCP 2005)},
  year = {2005},
  timestamp = {2009.11.03}
}

@ARTICLE{JACIL:SohITBN09,
  author = {Takehide Soh and Katsumi Inoue and Naoyuki Tamura and Mutsunori Banbara
	and Hidetomo Nabeshima},
  title = {A {SAT}-based Method for Solving the Two-dimensional Strip Packing
	Problem},
  journal = {Journal of Algorithms in Cognition, Informatics and Logic},
  year = {2009},
  note = {to appear},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/lics/StumpBDL01,
  author = {Aaron Stump and Clark W. Barrett and David L. Dill and Jeremy R.
	Levitt},
  title = {A Decision Procedure for an Extensional Theory of Arrays},
  booktitle = LICS-2001,
  year = {2001},
  pages = {29--37},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/jacm/SuzukiJ80,
  author = {Norihisa Suzuki and David Jefferson},
  title = {Verification Decidability of Presburger Array Programs},
  journal = JACM,
  year = {1980},
  volume = {27},
  pages = {191--205},
  number = {1},
  ee = {http://doi.acm.org/10.1145/322169.322185},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/sat/SorenssonB09,
  author = {Niklas S{\"o}rensson and Armin Biere},
  title = {Minimizing Learned Clauses},
  booktitle = SAT-2009,
  year = {2009},
  pages = {237--243},
  ee = {http://dx.doi.org/10.1007/978-3-642-02777-2_23},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{CSC06:TamuraB08,
  author = {Naoyuki Tamura and Mutsunori Banbara},
  title = {Sugar: a {CSP} to {SAT} Translator Based on Order Encoding},
  booktitle = CSC-2006,
  year = {2008},
  pages = {65--69},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/constraints/TamuraTKB09,
  author = {Naoyuki Tamura and Akiko Taga and Satoshi Kitagawa and Mutsunori
	Banbara},
  title = {Compiling Finite Linear {CSP} into {SAT}},
  journal = CONSTRAINTS,
  year = {2009},
  volume = {14},
  pages = {254--272},
  number = {2},
  ee = {http://dx.doi.org/10.1007/s10601-008-9061-0},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/cp/TamuraTKB06,
  author = {Naoyuki Tamura and Akiko Taga and Satoshi Kitagawa and Mutsunori
	Banbara},
  title = {Compiling Finite Linear {CSP} into {SAT}},
  booktitle = CP-2006,
  year = {2006},
  pages = {590--603},
  ee = {http://dx.doi.org/10.1007/11889205_42},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{CSC08:TamuraTB08,
  author = {Naoyuki Tamura and Tomoya Tanjo and Mutsunori Banbara},
  title = {System Description of a {SAT}-based {CSP} Solver {Sugar}},
  booktitle = CSC-2008,
  year = {2008},
  pages = {71--75},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{CSC08:TanjoTB08,
  author = {Tomoya Tanjo and Naoyuki Tamura and Mutsunori Banbara},
  title = {{Sugar++}: a {SAT}-based {Max-CSP}/{COP} Solver},
  booktitle = CSC-2008,
  year = {2008},
  pages = {77--82},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{CSC08:Choco08,
  author = {{The choco team}},
  title = {{choco}: an Open Source {Java} Constraint Programming Library},
  booktitle = CSC-2008,
  year = {2008},
  pages = {7--13},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/sat/Thurley06,
  author = {Marc Thurley},
  title = {{sharpSAT} - Counting Models with Advanced Component Caching and
	Implicit {BCP}},
  booktitle = SAT-2006,
  year = {2006},
  pages = {424--429},
  ee = {http://dx.doi.org/10.1007/11814948_38},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{CDPSS04:Tinelli04,
  author = {Cesare Tinelli},
  title = {The Combination Problem in First-Order Logic The Unsorted Case},
  booktitle = {Proceedings of the Combination of Decision Procedures: Summer School
	2004},
  year = {2004},
  howpublished = {{\tt http://verify.stanford.edu\slash summerschool2004/}},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/jar/TinelliZ05,
  author = {Cesare Tinelli and Calogero G. Zarba},
  title = {Combining Nonstably Infinite Theories},
  journal = JAR,
  year = {2005},
  volume = {34},
  pages = {209--238},
  number = {3},
  ee = {http://dx.doi.org/10.1007/s10817-005-5204-9},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/focs/Toda89,
  author = {Seinosuke Toda},
  title = {On the Computational Power of {PP} and {$\oplus$P}},
  booktitle = FOCS-1989,
  year = {1989},
  pages = {514--519},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{AC:TungA00,
  author = {Yu-Wen Tung and W. S. Aldiwan},
  title = {Automating Test Case Generation for the New Generation Mission Software
	System},
  booktitle = {Proceedings of IEEE Aerospace Conference},
  year = {2000},
  pages = {431--437},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/tcs/Valiant79,
  author = {Leslie G. Valiant},
  title = {The Complexity of Computing the Permanent},
  journal = TCS,
  year = {1979},
  volume = {8},
  pages = {189--201},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/cp/Walsh00,
  author = {Toby Walsh},
  title = {{SAT} v {CSP}},
  booktitle = {Proceedings of the 6th International Conference on Principles and
	Practice of Constraint Programming (CP 2000)},
  year = {2000},
  pages = {441--456},
  ee = {http://link.springer.de/link/service/series/0558/bibs/1894/18940441.htm},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/aaai/WeiES04,
  author = {Wei Wei and Jordan Erenrich and Bart Selman},
  title = {Towards Efficient Sampling: Exploiting Random Walk Strategies},
  booktitle = AAAI-2004,
  year = {2004},
  pages = {670--676},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/sat/WeiS05,
  author = {Wei Wei and Bart Selman},
  title = {A New Approach to Model Counting},
  booktitle = SAT-2005,
  year = {2005},
  pages = {324--339},
  ee = {http://dx.doi.org/10.1007/11499107_24},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/pts/Williams00,
  author = {Alan W. Williams},
  title = {Determination of Test Configurations for Pair-Wise Interaction Coverage},
  booktitle = {Proceedings of 13th International Conference on Testing Communicating
	Systems (TestCom 2000)},
  year = {2000},
  pages = {59--74},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/ijcai/WolfmanW99,
  author = {Steven A. Wolfman and Daniel S. Weld},
  title = {The {LPSAT} Engine {\&} its Application to Resource Planning},
  booktitle = IJCAI-1999,
  year = {1999},
  pages = {310--317},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{IPC5:XingCZ06,
  author = {Zhao Xing and Yixin Chen and and Weixiong Zhang},
  title = {{MaxPlan}: Optimal Planning by Decomposed Satisfiability and Backward
	Reduction},
  booktitle = IPC-5,
  year = {2006},
  pages = {53--56},
  timestamp = {2009.11.03}
}

@ARTICLE{DBLP:journals/jair/XuHHL08,
  author = {Lin Xu and Frank Hutter and Holger H. Hoos and Kevin Leyton-Brown},
  title = {{SATzilla}: Portfolio-based Algorithm Selection for {SAT}},
  journal = JAIR,
  year = {2008},
  volume = {32},
  pages = {565--606},
  ee = {http://jair.org/papers/paper2490.html},
  timestamp = {2009.11.03}
}

@INCOLLECTION{DBLP:series/faia/Zhang09,
  author = {Hantao Zhang},
  title = {Combinatorial Designs by SAT Solvers},
  booktitle = HOS,
  publisher = {{IOS} Press},
  year = {2009},
  pages = {533--568},
  ee = {http://dx.doi.org/10.3233/978-1-58603-929-5-533},
  timestamp = {2009.11.05}
}

@INPROCEEDINGS{DBLP:conf/iccad/ZhangMMM01,
  author = {Lintao Zhang and Conor F. Madigan and Matthew W. Moskewicz and Sharad
	Malik},
  title = {Efficient Conflict Driven Learning in Boolean Satisfiability Solver},
  booktitle = ICCAD-2001,
  year = {2001},
  pages = {279--285},
  ee = {http://www.sigda.org/Archives/ProceedingArchives/Iccad/Iccad2001/papers/2001/iccad01/htmfiles/sun_sgi/iccadabs.htm\#06a_1},
  timestamp = {2009.11.03}
}

@INPROCEEDINGS{DBLP:conf/sat/ZhangM03,
  author = {Lintao Zhang and Sharad Malik},
  title = {Cache Performance of {SAT} Solvers: a Case Study for Efficient Implementation
	of Algorithms},
  booktitle = SAT-2003,
  year = {2003},
  pages = {287--298},
  ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2919{\&}spage=287},
  timestamp = {2009.11.03}
}

@MISC{DIMACS,
  title = {DIMACS Challenge---Satisfiability: Suggested Format},
  howpublished = {{\tt ftp://dimacs.rutgers.edu\slash pub\slash challenge\slash satisfiability/}},
  timestamp = {2009.11.05}
}

@MISC{SATLIB,
  title = {{SATLIB}---The Satisfiability Library},
  howpublished = {{\tt http://www.satlib.org}},
  timestamp = {2009.11.05}
}

@PROCEEDINGS{DBLP:series/faia/2009-185,
  title = HOS,
  year = {2009},
  editor = {Armin Biere and Marijn Heule and Hans van Maaren and Toby Walsh},
  volume = {185},
  series = {Frontiers in Artificial Intelligence and Applications (FAIA)},
  publisher = {{IOS} Press},
  booktitle = HOS,
  isbn = {978-1-58603-929-5},
  timestamp = {2009.11.03}
}

@PROCEEDINGS{CSC06,
  title = {Proceedings of the Second International {CSP} Solver Competition},
  year = {2008},
  editor = {M. R. C. van Dongen and Christophe Lecoutre and Olivier Roussel},
  booktitle = {Proceedings of the Second International {CSP} Solver Competition},
  timestamp = {2009.11.03}
}

@article{DBLP:journals/jair/AdjimanCGRS06,
  author    = {Philippe Adjiman and
               Philippe Chatalic and
               Fran\c{c}ois Goasdou{\'e} and
               Marie-Christine Rousset and
               Laurent Simon},
  title     = {Distributed Reasoning in a Peer-to-Peer Setting: Application
               to the Semantic Web},
  journal   = JAIR,
  volume    = {25},
  year      = {2006},
  pages     = {269--314},
  ee        = {http://www.jair.org/papers/paper1785.html},
  timestamp = {2009.11.05}
}

@article{DBLP:journals/ai/AmirM05,
  author    = {Eyal Amir and
               Sheila A. McIlraith},
  title     = {Partition-based Logical Reasoning for First Order and Propositional
               Theories},
  journal   = AI,
  volume    = {162},
  number    = {1-2},
  year      = {2005},
  pages     = {49--88},
  ee        = {http://dx.doi.org/10.1016/j.artint.2004.11.004},
  timestamp = {2009.11.05}
}

@inproceedings{DBLP:conf/sat/AnsoteguiBL09,
  author    = {Carlos Ans{\'o}tegui and
               Maria Luisa Bonet and
               Jordi Levy},
  title     = {Solving (Weighted) Partial {MaxSAT} through Satisfiability
               Testing},
  booktitle = SAT-2009,
  year      = {2009},
  pages     = {427--440},
  ee        = {http://dx.doi.org/10.1007/978-3-642-02777-2_39},
  timestamp = {2009.11.05}
}

@article{DBLP:journals/jsat/ArgelichLMP08,
  author    = {Josep Argelich and
               Chu Min Li and
               Felip Many{\`a} and
               Jordi Planes},
  title     = {The First and Second Max-SAT Evaluations},
  journal   = JSAT,
  volume    = {4},
  number    = {2-4},
  year      = {2008},
  pages     = {251--278},
  ee        = {http://jsat.ewi.tudelft.nl/content/volume4/JSAT4_13_Argelich.pdf},
  timestamp = {2009.11.05}
}


@inproceedings{DBLP:conf/cp/BailleuxB03,
  author    = {Olivier Bailleux and
               Yacine Boufkhad},
  title     = {Efficient {CNF} Encoding of Boolean Cardinality Constraints},
  booktitle = CP-2003,
  year      = {2003},
  pages     = {108--122},
  ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2833{\&}spage=108},
  timestamp = {2009.11.05}
}

@inproceedings{DBLP:conf/cade/Benedetti05,
  author    = {Marco Benedetti},
  title     = {{sKizzo}: A Suite to Evaluate and Certify {QBFs}},
  booktitle = CADE-2005,
  year      = {2005},
  pages     = {369--376},
  ee        = {http://dx.doi.org/10.1007/11532231_27},
  timestamp = {2009.11.05}
}

@MISC{WWW:SAT4J,
  author = {Daniel Le Berre},
  title = {{SAT4J}: Bringing the Power of {SAT} Technology to the {Java} Platform},
  howpublished = {{\tt http://www.sat4j.org}},
  timestamp = {2009.11.05}
}

@inproceedings{DBLP:conf/sat/Biere04a,
  author    = {Armin Biere},
  title     = {Resolve and Expand},
  booktitle = SAT-2004,
  year      = {2004},
  pages     = {59--70},
  ee        = {http://dx.doi.org/10.1007/11527695_5},
  timestamp = {2009.11.05}
}

@article{DBLP:journals/iandc/BuningKF95,
  author    = {Hans Kleine B{\"u}ning and
               Marek Karpinski and
               Andreas Fl{\"o}gel},
  title     = {Resolution for Quantified Boolean Formulas},
  journal   = {Information and Computation},
  volume    = {117},
  number    = {1},
  year      = {1995},
  pages     = {12--18},
  timestamp = {2009.11.05}
}

@article{DBLP:journals/pc/ChrabakhW06,
  author    = {Wahid Chrabakh and
               Richard Wolski},
  title     = {{GridSAT}: a System for Solving Satisfiability Problems Using
               a Computational Grid},
  journal   = {Parallel Computing},
  volume    = {32},
  number    = {9},
  year      = {2006},
  pages     = {660--687},
  ee        = {http://dx.doi.org/10.1016/j.parco.2006.01.004},
  timestamp = {2009.11.05}
}

@ARTICLE{SCIENCE:ClearwaterHH91,
author = {S. H. Clearwater and B. A. Huberman and T. Hogg},
title = {Cooperative Solution of
  Constraint Satisfaction Problems},
  journal   = {Science},
  volume    = {254},
  number    = {5035},
  year      = {1991},
  pages     = {1181--1183},
  timestamp = {2009.11.05}
}

@article{DBLP:journals/entcs/FeldmanDH05,
  author    = {Yulik Feldman and
               Nachum Dershowitz and
               Ziyad Hanna},
  title     = {Parallel Multithreaded Satisfiability Solver: Design and
               Implementation},
  journal   = ENTCS,
  volume    = {128},
  number    = {3},
  year      = {2005},
  pages     = {75--90},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2004.10.020},
  timestamp = {2009.11.05}
}

@inproceedings{DBLP:conf/sat/FuM06,
  author    = {Zhaohui Fu and
               Sharad Malik},
  title     = {On Solving the Partial {MAX-SAT} Problem},
  booktitle = SAT-2006,
  year      = {2006},
  pages     = {252--265},
  ee        = {http://dx.doi.org/10.1007/11814948_25},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/jsat/GilFS08,
  author = {Lu\'{\i}s Gil and Paulo Flores and Lu\'{\i}s Miguel Silveira},
  title = {{PMSat}: a Parallel Version of {MiniSAT}},
  journal = JSAT,
  year = {2008},
  volume = {6},
  pages = {71--98},
  timestamp = {2009.11.05}
}

@inproceedings{DBLP:conf/cade/GiunchigliaNT01,
  author    = {Enrico Giunchiglia and
               Massimo Narizzano and
               Armando Tacchella},
  title     = {{QUBE}: A System for Deciding Quantified Boolean Formulas
               Satisfiability},
  booktitle = IJCAR-2001,
  year      = {2001},
  pages     = {364--369},
  ee        = {http://link.springer.de/link/service/series/0558/bibs/2083/20830364.htm},
  timestamp = {2009.11.05}
}

@article{DBLP:journals/ai/GiunchigliaNT03,
  author    = {Enrico Giunchiglia and
               Massimo Narizzano and
               Armando Tacchella},
  title     = {Backjumping for Quantified Boolean Logic satisfiability},
  journal   = AI,
  volume    = {145},
  number    = {1-2},
  year      = {2003},
  pages     = {99--120},
  ee        = {http://dx.doi.org/10.1016/S0004-3702(02)00373-9},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/jsat/HamadiJS08,
  author = {Youssef Hamadi and Said Jabbour and Lakhdar Sais},
  title = {{ManySAT}: a Parallel {SAT} Solver},
  journal = JSAT,
  year = {2008},
  volume = {6},
  pages = {245--262},
  timestamp = {2009.11.05}
}

@article{DBLP:journals/jsat/HerasLGS08,
  author    = {Federico Heras and
               Javier Larrosa and
               Simon de Givry and
               Thomas Schiex},
  title     = {2006 and 2007 Max-SAT Evaluations: Contributed Instances},
  journal   = JSAT,
  volume    = {4},
  number    = {2-4},
  year      = {2008},
  pages     = {239--250},
  ee        = {http://jsat.ewi.tudelft.nl/content/volume4/JSAT4_12_Heras.pdf},
  timestamp = {2009.11.05}
}

@article{DBLP:journals/jair/HerasLO08,
  author    = {Federico Heras and
               Javier Larrosa and
               Albert Oliveras},
  title     = {{MiniMaxSAT}: An Efficient Weighted {Max-SAT} solver},
  journal   = JAIR,
  volume    = {31},
  year      = {2008},
  pages     = {1--32},
  ee        = {http://jair.org/papers/paper2347.html},
  timestamp = {2009.11.05}
}

@inproceedings{DBLP:conf/atal/HirayamaY02,
  author    = {Katsutoshi Hirayama and
               Makoto Yokoo},
  title     = {Local Search for Distributed {SAT} with Complex Local Problems},
  booktitle = {AAMAS},
  year      = {2002},
  pages     = {1199--1206},
  ee        = {http://doi.acm.org/10.1145/545056.545099},
  timestamp = {2009.11.05}
}


@article{DBLP:journals/ai/HirayamaY05,
  author    = {Katsutoshi Hirayama and
               Makoto Yokoo},
  title     = {The Distributed Breakout Algorithms},
  journal   = AI,
  volume    = {161},
  number    = {1-2},
  year      = {2005},
  pages     = {89--115},
  ee        = {http://dx.doi.org/10.1016/j.artint.2004.08.004},
  timestamp = {2009.11.05}
}

@inproceedings{DBLP:conf/aaai/Hogg93,
  author    = {Tad Hogg and
               Colin P. Williams},
  title     = {Solving the Really Hard Problems with Cooperative Search},
  booktitle = AAAI-1993,
  year      = {1993},
  pages     = {231--236},
  timestamp = {2009.11.05}
}

@inproceedings{DBLP:conf/focs/KarloffZ97,
  author    = {Howard J. Karloff and
               Uri Zwick},
  title     = {A 7/8-Approximation Algorithm for {MAX} {3SAT}?},
  booktitle = FOCS-1997,
  year      = {1997},
  pages     = {406--415},
  ee        = {http://computer.org/proceedings/focs/8197/81970406abs.htm},
  timestamp = {2009.11.05}
}

@inproceedings{DBLP:conf/ijcai/KrocSGS09,
  author    = {Lukas Kroc and
               Ashish Sabharwal and
               Carla P. Gomes and
               Bart Selman},
  title     = {Integrating Systematic and Local Search Paradigms: A New
               Strategy for {MaxSAT}},
  booktitle = IJCAI-2009,
  year      = {2009},
  pages     = {544--551},
  ee        = {http://ijcai.org/papers09/Papers/IJCAI09-097.pdf},
  timestamp = {2009.11.05}
}
@article{DBLP:journals/ai/LarrosaHG08,
  author    = {Javier Larrosa and
               Federico Heras and
               Simon de Givry},
  title     = {A Logical Approach to Efficient {Max-SAT} Solving},
  journal   = AI,
  volume    = {172},
  number    = {2-3},
  year      = {2008},
  pages     = {204--233},
  ee        = {http://dx.doi.org/10.1016/j.artint.2007.05.006},
  timestamp = {2009.11.05}
}

@article{DBLP:journals/jair/LiMP07,
  author    = {Chu Min Li and
               Felip Many{\`a} and
               Jordi Planes},
  title     = {New Inference Rules for {Max-SAT}},
  journal   = JAIR,
  volume    = {30},
  year      = {2007},
  pages     = {321--359},
  ee        = {http://www.jair.org/papers/paper2215.html},
  timestamp = {2009.11.05}
}

@inproceedings{DBLP:conf/date/Marques-SilvaP08,
  author    = {Jo{\~a}o Marques-Silva and
               Jordi Planes},
  title     = {Algorithms for Maximum Satisfiability using Unsatisfiable
               Cores},
  booktitle = DATE-2008,
  year      = {2008},
  pages     = {408--413},
  ee        = {http://dx.doi.org/10.1109/DATE.2008.4484715},
  timestamp = {2009.11.05}
}

@ARTICLE{IEICETR-AI:OkamotoI04,
  author = {岡本 孝之 and 井上 克巳},
  title = {メッセージ通信を用いた分散型結論発見},
  journal = IEICETR-AI,
  year = {2004},
  volume = {104},
  pages = {25--30},
  number = {726},
  timestamp = {2009.11.05},
  yomi = {Takayuki Okamoto and Katsumi Inoue}
}

@inproceedings{DBLP:conf/sat/SabharwalAGHS06,
  author    = {Ashish Sabharwal and
               Carlos Ans{\'o}tegui and
               Carla P. Gomes and
               Justin W. Hart and
               Bart Selman},
  title     = {{QBF} Modeling: Exploiting Player Symmetry for Simplicity
               and Efficiency},
  booktitle = SAT-2006,
  year      = {2006},
  pages     = {382--395},
  ee        = {http://dx.doi.org/10.1007/11814948_35},
  timestamp = {2009.11.05}
}

@ARTICLE{DBLP:journals/jsat/SchubertLB09,
  author = {Tobias Schubert and Matthew Lewis and Bernd Becker},
  title = {{PaMiraXT}: Parallel SAT Solving with Threads and Message Passing},
  journal = JSAT,
  year = {2009},
  volume = {6},
  pages = {203--222},
  timestamp = {2009.11.05}
}

@article{DBLP:journals/endm/SinzBK01,
  author    = {Carsten Sinz and
               Wolfgang Blochinger and
               Wolfgang K{\"u}chlin},
  title     = {{PaSAT} - Parallel {SAT}-Checking with Lemma Exchange: Implementation
               and Applications},
  journal   = {Electronic Notes in Discrete Mathematics},
  volume    = {9},
  year      = {2001},
  pages     = {205--216},
  ee        = {http://dx.doi.org/10.1016/S1571-0653(04)00323-3},
  timestamp = {2009.11.05}
}

@inproceedings{DBLP:conf/cp/Sinz05,
  author    = {Carsten Sinz},
  title     = {Towards an Optimal {CNF} Encoding of Boolean Cardinality Constraints},
  booktitle = CP-2005,
  year      = {2005},
  pages     = {827--831},
  ee        = {http://dx.doi.org/10.1007/11564751_73},
  timestamp = {2009.11.05}
}

@article{DBLP:journals/tkde/YokooDIK98,
  author    = {Makoto Yokoo and
               Edmund H. Durfee and
               Toru Ishida and
               Kazuhiro Kuwabara},
  title     = {The Distributed Constraint Satisfaction Problem: Formalization
               and Algorithms},
  journal   = IEEE-TKDE,
  volume    = {10},
  number    = {5},
  year      = {1998},
  pages     = {673--685},
  ee        = {db/journals/tkde/YokooDIK98.html},
  timestamp = {2009.11.05}
}

@article{DBLP:journals/aamas/YokooH00,
  author    = {Makoto Yokoo and
               Katsutoshi Hirayama},
  title     = {Algorithms for Distributed Constraint Satisfaction: A Review},
  journal   = {Autonomous Agents and Multi-Agent Systems},
  volume    = {3},
  number    = {2},
  year      = {2000},
  pages     = {185--207},
  timestamp = {2009.11.05}
}

@ARTICLE{JSAI:YokooH00,
  author = {横尾 真 and 平山 勝敏},
  title = {複雑な局所問題に対応する分散制約充足アルゴリズム},
  journal = JSAI,
  year = {2000},
  volume = {15},
  number = {2},
  pages = {348--354},
  yomi = {Makoto Yokoo and Katsutoshi Hirayama},
  timestamp = {2009.11.05}
}

@article{DBLP:journals/jsc/ZhangBH96,
  author    = {Hantao Zhang and
               Maria Paola Bonacina and
               Jieh Hsiang},
  title     = {{PSATO}: a Distributed Propositional Prover and its Application
               to Quasigroup Problems},
  journal   = {Journal of Symbolic Computation},
  volume    = {21},
  number    = {4},
  year      = {1996},
  pages     = {543--560},
  timestamp = {2009.11.05}
}

@inproceedings{DBLP:conf/iccad/ZhangM02,
  author    = {Lintao Zhang and
               Sharad Malik},
  title     = {Conflict Driven Learning in a Quantified {Boolean} Satisfiability
               Solver},
  booktitle = ICCAD-2002,
  year      = {2002},
  pages     = {442--449},
  ee        = {http://doi.acm.org/10.1145/774572.774637},
  timestamp = {2009.11.05}
}