SATによるプランニングとスケジューリング   DBLP  Google Scholar  CiNii
鍋島 英知   DBLP  Google Scholar  CiNii
人工知能学会誌, Vol.25, No.1, 2010

CNF充足可能性判定問題の計算複雑さ   DBLP  Google Scholar  CiNii
岩間 一雄   DBLP  Google Scholar  CiNii
人工知能学会誌, Vol.16, No.5, pp.636-647, 2001

プランニングとスケジューリング   DBLP  Google Scholar  CiNii
宮下 和雄   DBLP  Google Scholar  CiNii
人工知能学会誌, Vol.16, No.5, pp.611-616, 9, 2001

ソフトウェア科学のための論理学   DBLP  Google Scholar  CiNii
萩谷 昌己   DBLP  Google Scholar  CiNii
岩波書店, 1994

SATによるシステム検証   DBLP  Google Scholar  CiNii
番原 睦則 and 田村 直之   DBLP  Google Scholar  CiNii
人工知能学会誌, Vol.25, No.1, 2010

$*$-SAT: SATの拡張   DBLP  Google Scholar  CiNii
平山 勝敏 and 横尾 真   DBLP  Google Scholar  CiNii
人工知能学会誌, Vol.25, No.1, 2010

SATソルバーの基礎   DBLP  Google Scholar  CiNii
井上 克巳 and 田村 直之   DBLP  Google Scholar  CiNii
人工知能学会誌, Vol.25, No.1, 2010

SMT: 個別理論を取り扱うSAT技術   DBLP  Google Scholar  CiNii
岩沼 宏治 and 鍋島 英知   DBLP  Google Scholar  CiNii
人工知能学会誌, Vol.25, No.1, 2010

高速SATソルバーの原理   DBLP  Google Scholar  CiNii
鍋島 英知 and 宋 剛秀   DBLP  Google Scholar  CiNii
人工知能学会誌, Vol.25, No.1, 2010

論理プログラミングから解集合プログラミングへ   DBLP  Google Scholar  CiNii
井上 克巳 and 坂間 千秋   DBLP  Google Scholar  CiNii
コンピュータソフトウェア, Vol.25, No.3, pp.20-32, 2008

メッセージ通信を用いた分散型結論発見   DBLP  Google Scholar  CiNii
岡本 孝之 and 井上 克巳   DBLP  Google Scholar  CiNii
電子情報通信学会技術研究報告，AI, Vol.104, No.726, pp.25-30, 2004

プランニンググラフとSATプランニング   DBLP  Google Scholar  CiNii
鍋島 英知 and 井上 克巳   DBLP  Google Scholar  CiNii
人工知能学会誌, Vol.16, No.5, pp.605-610, 2001

複雑な局所問題に対応する分散制約充足アルゴリズム   DBLP  Google Scholar  CiNii
横尾 真 and 平山 勝敏   DBLP  Google Scholar  CiNii
人工知能学会誌, Vol.15, No.2, pp.348-354, 2000

述語論理と論理プログラミング   DBLP  Google Scholar  CiNii
有川 節夫 and 原口 誠   DBLP  Google Scholar  CiNii
オーム社, 1988

一階論理上の等号推論：理論と実際   DBLP  Google Scholar  CiNii
岩沼 宏治 and 鍋島 英知 and 井上 克巳   DBLP  Google Scholar  CiNii
コンピュータソフトウェア,

モデル列挙とモデル計数   DBLP  Google Scholar  CiNii
長谷川 隆三 and 藤田 博 and 越村 三幸   DBLP  Google Scholar  CiNii
人工知能学会誌, Vol.25, No.1, 2010

制約最適化問題とSAT符号化   DBLP  Google Scholar  CiNii
田村 直之 and 丹生 智也 and 番原 睦則   DBLP  Google Scholar  CiNii
人工知能学会誌, Vol.25, No.1, 2010

モデル生成型定理証明と要素技術   DBLP  Google Scholar  CiNii
長谷川 隆三 and 藤田 博 and 越村 三幸   DBLP  Google Scholar  CiNii
コンピュータソフトウェア, Vol.25, No.3, pp.2-10, 2008

タブロー法とモデル生成型定理証明   DBLP  Google Scholar  CiNii
長谷川 隆三 and 藤田 博 and 越村 三幸   DBLP  Google Scholar  CiNii
人工知能学会誌, Vol.16, No.5, pp.661-667, 2001

分岐補題の抽出による極小モデル生成の効率化   DBLP  Google Scholar  CiNii
長谷川 隆三 and 藤田 博 and 越村 三幸   DBLP  Google Scholar  CiNii
人工知能学会論文誌, Vol.16, No.2, pp.234-245, 2001

SAT変換による未解決ジョブショップスケジューリング問題への挑戦   DBLP  Google Scholar  CiNii
越村 三幸 and 鍋島 英知 and 藤田 博 and 長谷川 隆三   DBLP  Google Scholar  CiNii
スケジューリング・シンポジウム2009講演論文集, pp.209-213, 2009

極小モデル生成とジョブショップスケジューリング問題の解法   DBLP  Google Scholar  CiNii
越村 三幸 and 鍋島 英知 and 藤田 博 and 長谷川 隆三   DBLP  Google Scholar  CiNii
日本ソフトウェア科学会第25回大会 講演論文集, 2008

グリッド計算環境上でのショップ・スケジューリング問題のSAT変換による解法   DBLP  Google Scholar  CiNii
多賀 明子 and 田村 直之 and 北川 哲 and 番原 睦則   DBLP  Google Scholar  CiNii
スケジューリング・シンポジウム2007講演論文集, pp.109-114, 2007

効率的なSATプランニングとSATスケジューリングのための補題再利用   DBLP  Google Scholar  CiNii
鍋島 英知 and 宋 剛秀 and 井上 克巳 and 岩沼 宏治   DBLP  Google Scholar  CiNii
電子情報通信学会技術研究報告，AI, Vol.106, No.38, pp.18-24, 2006

ショップ・スケジューリング問題のSAT変換による解法   DBLP  Google Scholar  CiNii
田村 直之 and 多賀 明子 and 番原 睦則 and 宋 剛秀 and 鍋島 英知 and 井上 克巳   DBLP  Google Scholar  CiNii
スケジューリング・シンポジウム2007講演論文集, pp.97-102, 2007

A Comparison of ATMS and CSP Techniques   DBLP  Google Scholar  CiNii
Johan de Kleer   DBLP  Google Scholar  CiNii
Proceedings of the 11th International Joint Conference on Artificial Intelligence (IJCAI 1989), pp.290-296, 1989

Distributed Reasoning in a Peer-to-Peer Setting: Application to the Semantic Web   DBLP  Google Scholar  CiNii
Philippe Adjiman and Philippe Chatalic and François Goasdoué and Marie-Christine Rousset and Laurent Simon   DBLP  Google Scholar  CiNii
Journal of Artificial Intelligence Research, Vol.25, pp.269-314, 2006

Partition-based Logical Reasoning for First Order and Propositional Theories   DBLP  Google Scholar  CiNii
Eyal Amir and Sheila A. McIlraith   DBLP  Google Scholar  CiNii
Artificial Intelligence, Vol.162, No.1-2, pp.49-88, 2005

Solving (Weighted) Partial MaxSAT through Satisfiability Testing   DBLP  Google Scholar  CiNii
Carlos Ansótegui and Maria Luisa Bonet and Jordi Levy   DBLP  Google Scholar  CiNii
Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT 2009), LNCS 5584, pp.427-440, 2009

The First and Second Max-SAT Evaluations   DBLP  Google Scholar  CiNii
Josep Argelich and Chu Min Li and Felip Manyà and Jordi Planes   DBLP  Google Scholar  CiNii
Journal on Satisfiability, Boolean Modeling and Computation, Vol.4, No.2-4, pp.251-278, 2008

SAT-Based Procedures for Temporal Reasoning   DBLP  Google Scholar  CiNii
Alessandro Armando and Claudio Castellini and Enrico Giunchiglia   DBLP  Google Scholar  CiNii
Proceedings of the 5th European Conference on Planning (ECP 1999), LNCS 1809, pp.97-108, 1999

A Generalized Framework for Conflict Analysis   DBLP  Google Scholar  CiNii
Gilles Audemard and Lucas Bordeaux and Youssef Hamadi and Sad Jabbour and Lakhdar Sais   DBLP  Google Scholar  CiNii
Proceedings of the 11th International Conference on Theory and Applications of Satisfiability Testing (SAT 2008), LNCS 4996, pp.21-27, 2008

Predicting Learnt Clauses Quality in Modern SAT Solvers   DBLP  Google Scholar  CiNii
Gilles Audemard and Laurent Simon   DBLP  Google Scholar  CiNii
Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009), pp.399-404, 2009

GAC via Unit Propagation   DBLP  Google Scholar  CiNii
Fahiem Bacchus   DBLP  Google Scholar  CiNii
Proceedings of the 13th International Joint Conference on Principles and Practice of Constraint Programming (CP 2007), LNCS 4741, pp.133-147, 2007

Algorithms and Complexity Results for SAT and Bayesian Inference   DBLP  Google Scholar  CiNii
Fahiem Bacchus and Shannon Dalmao and Toniann Pitassi   DBLP  Google Scholar  CiNii
Proceedings of the 44th Annual Symposium on Foundations of Computer Science (FOCS 2003), pp.340-351, 2003

Efficient CNF Encoding of Boolean Cardinality Constraints   DBLP  Google Scholar  CiNii
Olivier Bailleux and Yacine Boufkhad   DBLP  Google Scholar  CiNii
Proceedings of the 9th International Joint Conference on Principles and Practice of Constraint Programming (CP 2003), LNCS 2833, pp.108-122, 2003

New Encodings of Pseudo-Boolean Constraints into CNF   DBLP  Google Scholar  CiNii
Olivier Bailleux and Yacine Boufkhad and Olivier Roussel   DBLP  Google Scholar  CiNii
Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT 2009), LNCS 5584, pp.181-194, 2009

A Translation of Pseudo Boolean Constraints to SAT   DBLP  Google Scholar  CiNii
Olivier Bailleux and Yacine Boufkhad and Olivier Roussel   DBLP  Google Scholar  CiNii
Journal on Satisfiability, Boolean Modeling and Computation, Vol.2, No.1-4, pp.191-200, 2006

The Modelling Language Zinc   DBLP  Google Scholar  CiNii
Maria J. Garca de la Banda and Kim Marriott and Reza Rafeh and Mark Wallace   DBLP  Google Scholar  CiNii
Proceedings of the 12th International Joint Conference on Principles and Practice of Constraint Programming (CP 2006), LNCS 4204, pp.700-705, 2006

International Satisfiability Modulo Theories Competition   DBLP  Google Scholar  CiNii
B. Barrett and M. Deters and A. Oliveras and A. Stump   DBLP  Google Scholar  CiNii

A Generalization of Shostak's Method for Combining Decision Procedures   DBLP  Google Scholar  CiNii
Clark W. Barrett and David L. Dill and Aaron Stump   DBLP  Google Scholar  CiNii
Proceedings of the 4th International Workshop on Frontiers of Combining System (FroCoS 2002), LNCS 2309, pp.132-146, 2002

Satisfiability Modulo Theories   DBLP  Google Scholar  CiNii
Clark W. Barrett and Roberto Sebastiani and Sanjit A. Seshia and Cesare Tinelli   DBLP  Google Scholar  CiNii
Handbook of Satisfiability, IOS Press, pp.825-885, 2009

On-line Guide to Constraint Programming   DBLP  Google Scholar  CiNii
Roman Barták   DBLP  Google Scholar  CiNii
1998

The Model Evolution Calculus as a First-order DPLL Method   DBLP  Google Scholar  CiNii
Peter Baumgartner and Cesare Tinelli   DBLP  Google Scholar  CiNii
Artificial Intelligence, Vol.172, No.4-5, pp.591-632, 2008

Counting Models Using Connected Components   DBLP  Google Scholar  CiNii
Roberto J. Bayardo Jr. and Joseph Daniel Pehoushek   DBLP  Google Scholar  CiNii
Proceedings of the 17th National Conference on Artificial Intelligence (AAAI 2000), pp.157-162, 2000

Using CSP Look-Back Techniques to Solve Real-World SAT Instances   DBLP  Google Scholar  CiNii
Roberto J. Bayardo Jr. and Robert Schrag   DBLP  Google Scholar  CiNii
Proceedings of the 14th National Conference on Artificial Intelligence (AAAI 1997), pp.203-208, 1997

OR-Library: Distributing Test Problems by Electronic Mail   DBLP  Google Scholar  CiNii
J. E. Beasley   DBLP  Google Scholar  CiNii
Operational Research Society, Vol.41, pp.1069-1072, 1990

sKizzo: A Suite to Evaluate and Certify QBFs   DBLP  Google Scholar  CiNii
Marco Benedetti   DBLP  Google Scholar  CiNii
Proceedings of the 20th International Conference on Automated Deduction (CADE-20), LNCS 3632, pp.369-376, 2005

SAT4J: Bringing the Power of SAT Technology to the Java Platform   DBLP  Google Scholar  CiNii
Daniel Le Berre   DBLP  Google Scholar  CiNii

Local Consistencies in SAT   DBLP  Google Scholar  CiNii
Christian Bessière and Emmanuel Hebrard and Toby Walsh   DBLP  Google Scholar  CiNii
Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), LNCS 2919, pp.299-314, 2003

Bounded Model Checking   DBLP  Google Scholar  CiNii
Armin Biere   DBLP  Google Scholar  CiNii
Handbook of Satisfiability, IOS Press, pp.457-481, 2009

Resolve and Expand   DBLP  Google Scholar  CiNii
Armin Biere   DBLP  Google Scholar  CiNii
Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), LNCS 3542, pp.59-70, 2004

Symbolic Model Checking without BDDs   DBLP  Google Scholar  CiNii
Armin Biere and Alessandro Cimatti and Edmund M. Clarke and Yunshan Zhu   DBLP  Google Scholar  CiNii
Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 1999), LNCS 1579, pp.193-207, 1999

The Good Old Davis-Putnam Procedure Helps Counting Models   DBLP  Google Scholar  CiNii
Elazar Birnbaum and Eliezer L. Lozinskii   DBLP  Google Scholar  CiNii
Journal of Artificial Intelligence Research, Vol.10, pp.457-477, 1999

Fast Planning Through Planning Graph Analysis   DBLP  Google Scholar  CiNii
Avrim Blum and Merrick L. Furst   DBLP  Google Scholar  CiNii
Artificial Intelligence, Vol.90, No.1-2, pp.281-300, 1997

Planning as Heuristic Search   DBLP  Google Scholar  CiNii
Blai Bonet and Hector Geffner   DBLP  Google Scholar  CiNii
Artificial Intelligence, Vol.129, No.1-2, pp.5-33, 2001

Propositional Satisfiability and Constraint Programming: A Comparative Survey   DBLP  Google Scholar  CiNii
Lucas Bordeaux and Youssef Hamadi and Lintao Zhang   DBLP  Google Scholar  CiNii
ACM Computing Surveys, Vol.38, No.4, 2006

On Reachability, Relevance, and Resolution in the Planning as Satisfiability Approach   DBLP  Google Scholar  CiNii
Ronen I. Brafman   DBLP  Google Scholar  CiNii
Journal of Artificial Intelligence Research, Vol.14, pp.1-28, 2001

Survey Propagation: An Algorithm for Satisfiability   DBLP  Google Scholar  CiNii
Alfredo Braunstein and Marc Mézard and Riccardo Zecchina   DBLP  Google Scholar  CiNii
Random Structures & Algorithms, Vol.27, No.2, pp.201-226, 2005

Minimal Model Generation with Positive Unit Hyper-Resolution Tableaux   DBLP  Google Scholar  CiNii
François Bry and Adnan H. Yahya   DBLP  Google Scholar  CiNii
Proceedings of the 5th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX 1996), LNCS 1071, pp.143-159, 1996

Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic   DBLP  Google Scholar  CiNii
Randal E. Bryant and Steven M. German and Miroslav N. Velev   DBLP  Google Scholar  CiNii
ACM Transactions on Computational Logic, Vol.2, No.1, pp.93-134, 2001

A Fast Parallel SAT-Solver - Efficient Workload Balancing   DBLP  Google Scholar  CiNii
Max Böhm and Ewald Speckenmeyer   DBLP  Google Scholar  CiNii
Annals of Mathematics and Artificial Intelligence, Vol.17, No.3-4, pp.381-400, 1996

Resolution for Quantified Boolean Formulas   DBLP  Google Scholar  CiNii
Hans Kleine Büning and Marek Karpinski and Andreas Flögel   DBLP  Google Scholar  CiNii
Information and Computation, Vol.117, No.1, pp.12-18, 1995

Symbolic Logic and Mechanical Theorem Proving   DBLP  Google Scholar  CiNii
Chin-Liang Chang and Richard Char-Tung Lee   DBLP  Google Scholar  CiNii
Academic Press, 1971

On the State of Strength-Three Covering Arrays   DBLP  Google Scholar  CiNii
M. A. Chateauneuf and Donald L. Kreher   DBLP  Google Scholar  CiNii
Journal of Combinatorial Designs, Vol.10, No.4, pp.217-238, 2002

Long-distance Mutual Exclusion for Planning   DBLP  Google Scholar  CiNii
Yixin Chen and Ruoyun Huang and Zhao Xing and Weixiong Zhang   DBLP  Google Scholar  CiNii
Artificial Intelligence, Vol.173, No.2, pp.365-391, 2009

Plan-A: A Cost Optimal Planner Based on SAT-Constrained Optimization   DBLP  Google Scholar  CiNii
Yixin Chen and Qiang Lv   DBLP  Google Scholar  CiNii
Proceedings of the 6th International Planning Competition (IPC-6), 2008

Finite Domain Bounds Consistency Revisited   DBLP  Google Scholar  CiNii
Chiu Wo Choi and Warwick Harvey and J. H. M. Lee and Peter J. Stuckey   DBLP  Google Scholar  CiNii
Proceedings of the 19th Australian Joint Conference on Artificial Intelligence, LNCS 4304, pp.49-58, 2006

GridSAT: a System for Solving Satisfiability Problems Using a Computational Grid   DBLP  Google Scholar  CiNii
Wahid Chrabakh and Richard Wolski   DBLP  Google Scholar  CiNii
Parallel Computing, Vol.32, No.9, pp.660-687, 2006

Cache Conscious Data Structures for Boolean Satisfiability Solvers   DBLP  Google Scholar  CiNii
Geoffrey Chu and Aaron Harwood and Peter J. Stuckey   DBLP  Google Scholar  CiNii
Journal on Satisfiability, Boolean Modeling and Computation, Vol.6, pp.99-120, 2009

Cooperative Solution of Constraint Satisfaction Problems   DBLP  Google Scholar  CiNii
S. H. Clearwater and B. A. Huberman and T. Hogg   DBLP  Google Scholar  CiNii
Science, Vol.254, No.5035, pp.1181-1183, 1991

Compiling Constraints in clp(FD)   DBLP  Google Scholar  CiNii
Philippe Codognet and Daniel Diaz   DBLP  Google Scholar  CiNii
Journal of Logic Programming, Vol.27, No.3, pp.185-226, 1996

The AETG System: An Approach to Testing Based on Combinatiorial Design   DBLP  Google Scholar  CiNii
David M. Cohen and Siddhartha R. Dalal and Michael L. Fredman and Gardner C. Patton   DBLP  Google Scholar  CiNii
IEEE Transactions on Software Engineering, Vol.23, No.7, pp.437-444, 1997

Constructing Test Suites for Interaction Testing   DBLP  Google Scholar  CiNii
Myra B. Cohen and Peter B. Gibbons and Warwick B. Mugridge and Charles J. Colbourn   DBLP  Google Scholar  CiNii
Proceedings of the 25th International Conference on Software Engineering (ICSE 2003), pp.38-48, 2003

Covering Array Tables for t=2,3,4,5,6   DBLP  Google Scholar  CiNii
Charles J. Colbourn   DBLP  Google Scholar  CiNii
2009

Combinatorial Aspects of Covering Arrays   DBLP  Google Scholar  CiNii
Charles J. Colbourn   DBLP  Google Scholar  CiNii
Le Matematiche (Catania), Vol.58, pp.121-167, 2004

The Complexity of Theorem-Proving Procedures   DBLP  Google Scholar  CiNii
Stephen A. Cook   DBLP  Google Scholar  CiNii
Proceedings of the 3rd Annual ACM Symposium on Theory of Computing (STOC 1971), pp.151-158, 1971

Experimental Results on the Crossover Point in Random 3-SAT   DBLP  Google Scholar  CiNii
James M. Crawford and Larry D. Auton   DBLP  Google Scholar  CiNii
Artificial Intelligence, Vol.81, No.1-2, pp.31-57, 1996

Experimental Results on the Application of Satisfiability Algorithms to Scheduling Problems   DBLP  Google Scholar  CiNii
James M. Crawford and Andrew B. Baker   DBLP  Google Scholar  CiNii
Proceedings of the 12th National Conference on Artificial Intelligence (AAAI 1994), pp.1092-1097, 1994

Worst-Case Upper Bounds   DBLP  Google Scholar  CiNii
Evgeny Dantsin and Edward A. Hirsch   DBLP  Google Scholar  CiNii
Handbook of Satisfiability, IOS Press, pp.403-424, 2009

New Advances in Compiling CNF into Decomposable Negation Normal Form   DBLP  Google Scholar  CiNii
Adnan Darwiche   DBLP  Google Scholar  CiNii
Proceedings of the 16th European Conference on Artificial Intelligence (ECAI 2004), pp.328-332, 2004

Decomposable Negation Normal Form   DBLP  Google Scholar  CiNii
Adnan Darwiche   DBLP  Google Scholar  CiNii
Journal of the ACM, Vol.48, No.4, pp.608-647, 2001

Using More Reasoning to Improve SAT Solving   DBLP  Google Scholar  CiNii
Jessica Davies and Fahiem Bacchus   DBLP  Google Scholar  CiNii
Proceedings of the 22nd National Conference on Artificial Intelligence (AAAI 2007), pp.185-190, 2007

A Machine Program for Theorem-Proving   DBLP  Google Scholar  CiNii
Martin Davis and George Logemann and Donald W. Loveland   DBLP  Google Scholar  CiNii
Communications of the ACM, Vol.5, No.7, pp.394-397, 1962

A Computing Procedure for Quantification Theory   DBLP  Google Scholar  CiNii
Martin Davis and Hilary Putnam   DBLP  Google Scholar  CiNii
Journal of the ACM, Vol.7, No.3, pp.201-215, 1960

Backjump-based Backtracking for Constraint Satisfaction Problems   DBLP  Google Scholar  CiNii
Rina Dechter and Daniel Frost   DBLP  Google Scholar  CiNii
Artificial Intelligence, Vol.136, No.2, pp.147-188, 2002

An Efficient Approach to Solving Random k-sat Problems   DBLP  Google Scholar  CiNii
Gilles Dequen and Olivier Dubois   DBLP  Google Scholar  CiNii
Journal of Automated Reasoning, Vol.37, No.4, pp.261-276, 2006

Encoding Planning Problems in Nonmonotonic Logic Programs   DBLP  Google Scholar  CiNii
Yannis Dimopoulos and Bernhard Nebel and Jana Koehler   DBLP  Google Scholar  CiNii
Proceedings of the 4th European Conference on Planning (ECP 1997), LNCS 1348, pp.169-181, 1997

Propagation in CSP and SAT   DBLP  Google Scholar  CiNii
Yannis Dimopoulos and Kostas Stergiou   DBLP  Google Scholar  CiNii
Proceedings of the 12th International Joint Conference on Principles and Practice of Constraint Programming (CP 2006), LNCS 4204, pp.137-151, 2006

Results of the Second CSP Solver Competition   DBLP  Google Scholar  CiNii
M. R. C. van Dongen and Christophe Lecoutre and Olivier Roussel   DBLP  Google Scholar  CiNii
Proceedings of the 2nd International CSP Solver Competition, pp.1-10, 2008

Assignment Commands with Array References   DBLP  Google Scholar  CiNii
Peter J. Downey and Ravi Sethi   DBLP  Google Scholar  CiNii
Journal of the ACM, Vol.25, No.4, pp.652-666, 1978

Variations on the Common Subexpression Problem   DBLP  Google Scholar  CiNii
Peter J. Downey and Ravi Sethi and Robert Endre Tarjan   DBLP  Google Scholar  CiNii
Journal of the ACM, Vol.27, No.4, pp.758-771, 1980

Test Pattern Generation using Boolean Proof Engines   DBLP  Google Scholar  CiNii
Rolf Drechsler and Stephan Eggersglüß and Görschwin Fey and Daniel Tille   DBLP  Google Scholar  CiNii
Springer, 2009

Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas   DBLP  Google Scholar  CiNii
Uwe Egly and Thomas Eiter and Hans Tompits and Stefan Woltran   DBLP  Google Scholar  CiNii
Proceedings of the 17th National Conference on Artificial Intelligence (AAAI 2000), pp.417-422, 2000

Automatic SAT-Compilation of Planning Problems   DBLP  Google Scholar  CiNii
Michael D. Ernst and Todd D. Millstein and Daniel S. Weld   DBLP  Google Scholar  CiNii
Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI 1997), pp.1169-1177, 1997

Translating Pseudo-Boolean Constraints into SAT   DBLP  Google Scholar  CiNii
Niklas Eén and Niklas Sörensson   DBLP  Google Scholar  CiNii
Journal on Satisfiability, Boolean Modeling and Computation, Vol.2, No.1-4, pp.1-26, 2006

MiniSat: A SAT Solver with Conflict-Clause Minimization   DBLP  Google Scholar  CiNii
Niklas Eén and Niklas Sörensson   DBLP  Google Scholar  CiNii
Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT 2005), LNCS 3569, pp.502-518, 2005

An Extensible SAT-solver   DBLP  Google Scholar  CiNii
Niklas Eén and Niklas Sörensson   DBLP  Google Scholar  CiNii
Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), LNCS 2919, pp.502-518, 2003

Temporal Induction by Incremental SAT Solving   DBLP  Google Scholar  CiNii
Niklas Eén and Niklas Sörensson   DBLP  Google Scholar  CiNii
Electronic Notes in Theoretical Computer Science, Vol.89, No.4, 2003

Parallel Multithreaded Satisfiability Solver: Design and Implementation   DBLP  Google Scholar  CiNii
Yulik Feldman and Nachum Dershowitz and Ziyad Hanna   DBLP  Google Scholar  CiNii
Electronic Notes in Theoretical Computer Science, Vol.128, No.3, pp.75-90, 2005

Theorem Proving Using Lazy Proof Explication   DBLP  Google Scholar  CiNii
Cormac Flanagan and Rajeev Joshi and Xinming Ou and James B. Saxe   DBLP  Google Scholar  CiNii
Proceedings of the 15th International Conference on Computer Aided Verification (CAV 2003), LNCS 2725, pp.355-367, 2003

Improvements to Propositional Satisfiability Search Algorithms   DBLP  Google Scholar  CiNii
Jon William Freeman   DBLP  Google Scholar  CiNii
1995

On Solving the Partial MAX-SAT Problem   DBLP  Google Scholar  CiNii
Zhaohui Fu and Sharad Malik   DBLP  Google Scholar  CiNii
Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT 2006), LNCS 4121, pp.252-265, 2006

Shostak Light   DBLP  Google Scholar  CiNii
Harald Ganzinger   DBLP  Google Scholar  CiNii
Proceedings of the 18th International Conference on Automated Deduction (CADE-18), LNCS 2392, pp.332-346, 2002

New Directions in Instantiation-Based Theorem Proving   DBLP  Google Scholar  CiNii
Harald Ganzinger and Konstantin Korovin   DBLP  Google Scholar  CiNii
Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), pp.55-64, 2003

Computers and Intractability: A Guide to the Theory of NP-Completeness   DBLP  Google Scholar  CiNii
Michael R. Garey and David S. Johnson   DBLP  Google Scholar  CiNii
W. H. Freeman and Company, 1979

The Log-Support Encoding of CSP into SAT   DBLP  Google Scholar  CiNii
Marco Gavanelli   DBLP  Google Scholar  CiNii
Proceedings of the 13th International Joint Conference on Principles and Practice of Constraint Programming (CP 2007), LNCS 4741, pp.815-822, 2007

Conflict-Driven Answer Set Solving   DBLP  Google Scholar  CiNii
Martin Gebser and Benjamin Kaufmann and André Neumann and Torsten Schaub   DBLP  Google Scholar  CiNii
Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007), pp.386-, 2007

Another Look at Graph Coloring via Propositional Satisfiability   DBLP  Google Scholar  CiNii
Allen Van Gelder   DBLP  Google Scholar  CiNii
Discrete Applied Mathematics, Vol.156, No.2, pp.230-243, 2008

Arc Consistency in SAT   DBLP  Google Scholar  CiNii
Ian P. Gent   DBLP  Google Scholar  CiNii
Proceedings of the 15th European Conference on Artificial Intelligence (ECAI 2002), pp.121-125, 2002

Generalised Arc Consistency for the AllDifferent Constraint: An Empirical Survey   DBLP  Google Scholar  CiNii
Ian P. Gent and Ian Miguel and Peter Nightingale   DBLP  Google Scholar  CiNii
Artificial Intelligence, Vol.172, No.18, pp.1973-2000, 2008

A New Encoding of Alldifferent into SAT   DBLP  Google Scholar  CiNii
I. P. Gent and P. Nightingale   DBLP  Google Scholar  CiNii
Proceedings of the 3rd International Workshop on Modelling and Reformulating Constraint Satisfaction Problems, 2004

Inferring State Constraints for Domain-Independent Planning   DBLP  Google Scholar  CiNii
Alfonso Gerevini and Lenhart K. Schubert   DBLP  Google Scholar  CiNii
Proceedings of the 15th National Conference on Artificial Intelligence (AAAI 1998), pp.905-912, 1998

PMSat: a Parallel Version of MiniSAT   DBLP  Google Scholar  CiNii
Lus Gil and Paulo Flores and Lus Miguel Silveira   DBLP  Google Scholar  CiNii
Journal on Satisfiability, Boolean Modeling and Computation, Vol.6, pp.71-98, 2008

SAT-Based Planning with Minimal-actions Plans and ``soft'' Goals   DBLP  Google Scholar  CiNii
Enrico Giunchiglia and Marco Maratea   DBLP  Google Scholar  CiNii
Proceedings of the 10th Congress of the Italian Association for Artificial Intelligence (AI*IA 2007), LNCS 4733, pp.422-433, 2007

Solving Optimization Problems with DLL   DBLP  Google Scholar  CiNii
Enrico Giunchiglia and Marco Maratea   DBLP  Google Scholar  CiNii
Proceedings of the 17th European Conference on Artificial Intelligence (ECAI 2006), FAIA 141, pp.377-381, 2006

optsat: A Tool for Solving SAT Related Optimization Problems   DBLP  Google Scholar  CiNii
Enrico Giunchiglia and Marco Maratea   DBLP  Google Scholar  CiNii
Proceedings of the 10th European Conference on Logics in Artificial Intelligence (JELIA 2006), LNCS 4160, pp.485-489, 2006

Backjumping for Quantified Boolean Logic satisfiability   DBLP  Google Scholar  CiNii
Enrico Giunchiglia and Massimo Narizzano and Armando Tacchella   DBLP  Google Scholar  CiNii
Artificial Intelligence, Vol.145, No.1-2, pp.99-120, 2003

QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability   DBLP  Google Scholar  CiNii
Enrico Giunchiglia and Massimo Narizzano and Armando Tacchella   DBLP  Google Scholar  CiNii
Proceedings of the 1st International Joint Conference on Automated Reasoning (IJCAR 2001), LNCS 2083, pp.364-369, 2001

Approximate Counting by Sampling the Backtrack-free Search Space   DBLP  Google Scholar  CiNii
Vibhav Gogate and Rina Dechter   DBLP  Google Scholar  CiNii
Proceedings of the 22nd National Conference on Artificial Intelligence (AAAI 2007), pp.198-203, 2007

BerkMin: A Fast and Robust SAT-solver   DBLP  Google Scholar  CiNii
Eugene Goldberg and Yakov Novikov   DBLP  Google Scholar  CiNii
Discrete Applied Mathematics, Vol.155, No.12, pp.1549-1561, 2007

From Sampling to Model Counting   DBLP  Google Scholar  CiNii
Carla P. Gomes and Jörg Hoffmann and Ashish Sabharwal and Bart Selman   DBLP  Google Scholar  CiNii
Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007), pp.2293-2299, 2007

Short XORs for Model Counting: From Theory to Practice   DBLP  Google Scholar  CiNii
Carla P. Gomes and Jörg Hoffmann and Ashish Sabharwal and Bart Selman   DBLP  Google Scholar  CiNii
Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007), LNCS 4501, pp.100-106, 2007

Satisfiability Solvers   DBLP  Google Scholar  CiNii
Carla P. Gomes and Henry Kautz and Ashish Sabharwal and Bart Selman   DBLP  Google Scholar  CiNii
Handbook of Knowledge Representation, Elsevier, Vol.3, pp.89-134, 2008

Model Counting   DBLP  Google Scholar  CiNii
Carla P. Gomes and Ashish Sabharwal and Bart Selman   DBLP  Google Scholar  CiNii
Handbook of Satisfiability, IOS Press, pp.633-654, 2009

Algorithm Portfolios   DBLP  Google Scholar  CiNii
Carla P. Gomes and Bart Selman   DBLP  Google Scholar  CiNii
Artificial Intelligence, Vol.126, No.1-2, pp.43-62, 2001

Heavy-Tailed Distributions in Combinatorial Search   DBLP  Google Scholar  CiNii
Carla P. Gomes and Bart Selman and Nuno Crato   DBLP  Google Scholar  CiNii
Proceedings of the 3rd International Joint Conference on Principles and Practice of Constraint Programming (CP 1997), LNCS 1330, pp.121-135, 1997

Heavy-Tailed Phenomena in Satisfiability and Constraint Satisfaction Problems   DBLP  Google Scholar  CiNii
Carla P. Gomes and Bart Selman and Nuno Crato and Henry A. Kautz   DBLP  Google Scholar  CiNii
Journal of Automated Reasoning, Vol.24, No.1/2, pp.67-100, 2000

Boosting Combinatorial Search Through Randomization   DBLP  Google Scholar  CiNii
Carla P. Gomes and Bart Selman and Henry A. Kautz   DBLP  Google Scholar  CiNii
Proceedings of the 15th National Conference on Artificial Intelligence (AAAI 1998), pp.431-437, 1998

Random Worlds and Maximum Entropy   DBLP  Google Scholar  CiNii
Adam J. Grove and Joseph Y. Halpern and Daphne Koller   DBLP  Google Scholar  CiNii
Journal of Artificial Intelligence Research, Vol.2, pp.33-88, 1994

A New Lower Bound for the Open-shop Problem   DBLP  Google Scholar  CiNii
Christelle Guéret and Christian Prins   DBLP  Google Scholar  CiNii
Annals of Operations Research, Vol.92, pp.165-183, 1999

ManySAT: a Parallel SAT Solver   DBLP  Google Scholar  CiNii
Youssef Hamadi and Said Jabbour and Lakhdar Sais   DBLP  Google Scholar  CiNii
Journal on Satisfiability, Boolean Modeling and Computation, Vol.6, pp.245-262, 2008

Problems and Algorithms for Covering Arrays   DBLP  Google Scholar  CiNii
Alan Hartman and Leonid Raskin   DBLP  Google Scholar  CiNii
Discrete Mathematics, Vol.284, No.1-3, pp.149-156, 2004

Efficient Minimal Model Generation Using Branching Lemmas   DBLP  Google Scholar  CiNii
Ryuzo Hasegawa and Hiroshi Fujita and Miyuki Koshimura   DBLP  Google Scholar  CiNii
CADE, pp.184-199, 2000

The OPL Optimization Programming Language   DBLP  Google Scholar  CiNii
Pascal van Hentenryck   DBLP  Google Scholar  CiNii
MIT Press, 1999

2006 and 2007 Max-SAT Evaluations: Contributed Instances   DBLP  Google Scholar  CiNii
Federico Heras and Javier Larrosa and Simon de Givry and Thomas Schiex   DBLP  Google Scholar  CiNii
Journal on Satisfiability, Boolean Modeling and Computation, Vol.4, No.2-4, pp.239-250, 2008

MiniMaxSAT: An Efficient Weighted Max-SAT solver   DBLP  Google Scholar  CiNii
Federico Heras and Javier Larrosa and Albert Oliveras   DBLP  Google Scholar  CiNii
Journal of Artificial Intelligence Research, Vol.31, pp.1-32, 2008

SmArT solving: Tools and Techniques for Satisfiability Solvers   DBLP  Google Scholar  CiNii
Marijn Heule   DBLP  Google Scholar  CiNii
2008

Look-Ahead Based SAT Solvers   DBLP  Google Scholar  CiNii
Marijn Heule and Hans van Maaren   DBLP  Google Scholar  CiNii
Handbook of Satisfiability, IOS Press, pp.155-184, 2009

The Distributed Breakout Algorithms   DBLP  Google Scholar  CiNii
Katsutoshi Hirayama and Makoto Yokoo   DBLP  Google Scholar  CiNii
Artificial Intelligence, Vol.161, No.1-2, pp.89-115, 2005

Local Search for Distributed SAT with Complex Local Problems   DBLP  Google Scholar  CiNii
Katsutoshi Hirayama and Makoto Yokoo   DBLP  Google Scholar  CiNii
AAMAS, pp.1199-1206, 2002

Constraint-Based Approaches to the Covering Test Problem   DBLP  Google Scholar  CiNii
Brahim Hnich and Steven David Prestwich and Evgeny Selensky   DBLP  Google Scholar  CiNii
Proceedings of the International Workshop on Constraint Solving and Constraint Logic Programming (CSCLP 2004), LNCS 3419, pp.172-186, 2004

Constraint Models for the Covering Test Problem   DBLP  Google Scholar  CiNii
Brahim Hnich and Steven David Prestwich and Evgeny Selensky and Barbara M. Smith   DBLP  Google Scholar  CiNii
Constraints, Vol.11, No.2-3, pp.199-219, 2006

SAT Encodings of State-Space Reachability Problems in Numeric Domains   DBLP  Google Scholar  CiNii
Jörg Hoffmann and Carla P. Gomes and Bart Selman and Henry A. Kautz   DBLP  Google Scholar  CiNii
Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007), pp.1918-1923, 2007

Solving the Really Hard Problems with Cooperative Search   DBLP  Google Scholar  CiNii
Tad Hogg and Colin P. Williams   DBLP  Google Scholar  CiNii
Proceedings of the 11th National Conference on Artificial Intelligence (AAAI 1993), pp.231-236, 1993

SAT-Encodings, Search Space Structure, and Local Search Performance   DBLP  Google Scholar  CiNii
Holger H. Hoos   DBLP  Google Scholar  CiNii
Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI 1999), pp.296-303, 1999

Universal Booleanization of Constraint Models   DBLP  Google Scholar  CiNii
Jinbo Huang   DBLP  Google Scholar  CiNii
Proceedings of the 14th International Joint Conference on Principles and Practice of Constraint Programming (CP 2008), LNCS 5202, pp.144-158, 2008

The Effect of Restarts on the Efficiency of Clause Learning   DBLP  Google Scholar  CiNii
Jinbo Huang   DBLP  Google Scholar  CiNii
Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007), pp.2318-2323, 2007

An Economics Approach to Hard Computational Problems   DBLP  Google Scholar  CiNii
Bernardo A. Huberman and Rajan M. Lukose and Tad Hogg   DBLP  Google Scholar  CiNii
Science, Vol.275, pp.51-54, 1997

A Competitive and Cooperative Approach to Propositional Satisfiability   DBLP  Google Scholar  CiNii
Katsumi Inoue and Takehide Soh and Seiji Ueda and Yoshito Sasaura and Mutsunori Banbara and Naoyuki Tamura   DBLP  Google Scholar  CiNii
Discrete Applied Mathematics, Vol.154, No.16, pp.2291-2306, 2006

SAT-Variable Complexity of Hard Combinatorial Problems   DBLP  Google Scholar  CiNii
Kazuo Iwama and Shuichi Miyazaki   DBLP  Google Scholar  CiNii
Proceedings of the IFIP 13th World Computer Congress, pp.253-258, 1994

Improved upper bounds for 3-SAT   DBLP  Google Scholar  CiNii
Kazuo Iwama and Suguru Tamaki   DBLP  Google Scholar  CiNii
Proceedings of the 15th ACM-SIAM Symposium on Discrete Algorithms (SODA 04), pp.328, 2004

Constraint Logic Programming: A Survey   DBLP  Google Scholar  CiNii
Joxan Jaffar and Michael J. Maher   DBLP  Google Scholar  CiNii
Journal of Logic Programming, Vol.19/20, pp.503-581, 1994

Efficient SAT Solving for Non-Clausal Formulas using DPLL, Graphs, and Watched Cuts   DBLP  Google Scholar  CiNii
Himanshu Jain and Edmund M. Clarke   DBLP  Google Scholar  CiNii
Proceedings of the 46th Design Automation Conference (DAC 2009), pp.563-568, 2009

Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit   DBLP  Google Scholar  CiNii
HoonSang Jin and HyoJung Han and Fabio Somenzi   DBLP  Google Scholar  CiNii
Proceedings of the 11th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2005), LNCS 3440, pp.287-300, 2005

A 7/8-Approximation Algorithm for MAX 3SAT?   DBLP  Google Scholar  CiNii
Howard J. Karloff and Uri Zwick   DBLP  Google Scholar  CiNii
Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS 1997), pp.406-415, 1997

A New Polynomial-time Algorithm for Linear Programming   DBLP  Google Scholar  CiNii
Narendra Karmarkar   DBLP  Google Scholar  CiNii
Combinatorica, Vol.4, No.4, pp.373-396, 1984

On the Parallel Complexity of Discrete Relaxation in Constraint Satisfaction Networks   DBLP  Google Scholar  CiNii
Simon Kasif   DBLP  Google Scholar  CiNii
Artificial Intelligence, Vol.45, No.3, pp.275-286, 1990

Dynamic Restart Policies   DBLP  Google Scholar  CiNii
Henry A. Kautz and Eric Horvitz and Yongshao Ruan and Carla P. Gomes and Bart Selman   DBLP  Google Scholar  CiNii
Proceedings of the 18th National Conference on Artificial Intelligence (AAAI 2002), pp.674-681, 2002

Unifying SAT-based and Graph-based Planning   DBLP  Google Scholar  CiNii
Henry A. Kautz and Bart Selman   DBLP  Google Scholar  CiNii
Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI 1999), pp.318-325, 1999

The Role of Domain-Specific Knowledge in the Planning as Satisfiability Framework   DBLP  Google Scholar  CiNii
Henry A. Kautz and Bart Selman   DBLP  Google Scholar  CiNii
Proceedings of the 4th International Conference on Artificial Intelligence Planning Systems (AIPS 1998), pp.181-189, 1998

Pushing the Envelope: Planning, Propositional Logic and Stochastic Search   DBLP  Google Scholar  CiNii
Henry A. Kautz and Bart Selman   DBLP  Google Scholar  CiNii
Proceedings of the 13th National Conference on Artificial Intelligence (AAAI 1996), pp.1194-1201, 1996

Planning as Satisfiability   DBLP  Google Scholar  CiNii
Henry A. Kautz and Bart Selman   DBLP  Google Scholar  CiNii
Proceedings of the 10th European Conference on Artificial Intelligence (ECAI 1992), pp.359-363, 1992

BLACKBOX: A New Approach to the Application of Theorem Proving to Problem Solving   DBLP  Google Scholar  CiNii
Henry Kautz and Bart Selman   DBLP  Google Scholar  CiNii
AIPS98 Workshop on Planning as Combinatorial Search, pp.58-60, 1998

SatPlan: Planning as Satisfiability   DBLP  Google Scholar  CiNii
Henry Kautz and Bart Selman and Jöerg Hoffmann   DBLP  Google Scholar  CiNii
Proceedings of the 5th International Planning Competition (IPC-5), 2006

Minimal Model Generation with Factorization and Constrained Search   DBLP  Google Scholar  CiNii
Miyuki Koshimura and Megumi Iwaki and Ryuzo Hasegawa   DBLP  Google Scholar  CiNii
情報処理学会論文誌, Vol.44, No.4, pp.1163-1172, 2003

Integrating Systematic and Local Search Paradigms: A New Strategy for MaxSAT   DBLP  Google Scholar  CiNii
Lukas Kroc and Ashish Sabharwal and Carla P. Gomes and Bart Selman   DBLP  Google Scholar  CiNii
Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009), pp.544-551, 2009

Leveraging Belief Propagation, Backtrack Search, and Statistics for Model Counting   DBLP  Google Scholar  CiNii
Lukas Kroc and Ashish Sabharwal and Bart Selman   DBLP  Google Scholar  CiNii
CPAIOR, pp.127-141, 2008

Investigating the Behaviour of a SAT Solver on Random Formulas   DBLP  Google Scholar  CiNii
Oliver Kullmann   DBLP  Google Scholar  CiNii
2002

The UCLID Decision Procedure   DBLP  Google Scholar  CiNii
Shuvendu K. Lahiri and Sanjit A. Seshia   DBLP  Google Scholar  CiNii
Proceedings of the 16th International Conference on Computer Aided Verification (CAV 2004), LNCS 3114, pp.475-478, 2004

A Logical Approach to Efficient Max-SAT Solving   DBLP  Google Scholar  CiNii
Javier Larrosa and Federico Heras and Simon de Givry   DBLP  Google Scholar  CiNii
Artificial Intelligence, Vol.172, No.2-3, pp.204-233, 2008

In-Parameter-Order: A Test Generation Strategy for Pairwise Testing   DBLP  Google Scholar  CiNii
Yu Lei and Kuo-Chung Tai   DBLP  Google Scholar  CiNii
Proceedings of 3rd IEEE International Symposium on High-Assurance Systems Engineering (HASE 1998), pp.254-261, 1998

Cotrolled Integration of the Cut Rule into Connection Tableaux Calculi   DBLP  Google Scholar  CiNii
Reinhold Letz and Klaus Mayr and Christoph Goller   DBLP  Google Scholar  CiNii
Journal of Automated Reasoning, Vol.13, No.3, pp.297-337, 1994

Look-Ahead Versus Look-Back for Satisfiability Problems   DBLP  Google Scholar  CiNii
Chu Min Li and Anbulagan   DBLP  Google Scholar  CiNii
Proceedings of the 3rd International Joint Conference on Principles and Practice of Constraint Programming (CP 1997), LNCS 1330, pp.341-355, 1997

Heuristics Based on Unit Propagation for Satisfiability Problems.   DBLP  Google Scholar  CiNii
Chu Min Li and Anbulagan   DBLP  Google Scholar  CiNii
Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI 1997), pp.366-371, 1997

New Inference Rules for Max-SAT   DBLP  Google Scholar  CiNii
Chu Min Li and Felip Manyà and Jordi Planes   DBLP  Google Scholar  CiNii
Journal of Artificial Intelligence Research, Vol.30, pp.321-359, 2007

Optimal Speedup of Las Vegas Algorithms   DBLP  Google Scholar  CiNii
Michael Luby and Alistair Sinclair and David Zuckerman   DBLP  Google Scholar  CiNii
Information Processing Letters, Vol.47, No.4, pp.173-180, 1993

Boolean Satisfiability from Theoretical Hardness to Practical Success   DBLP  Google Scholar  CiNii
Sharad Malik and Lintao Zhang   DBLP  Google Scholar  CiNii
Communications of the ACM, Vol.52, No.8, pp.76-82, 2009

Combining Decision Procedures   DBLP  Google Scholar  CiNii
Zohar Manna and Calogero G. Zarba   DBLP  Google Scholar  CiNii
Formal Methods at the Crossroads. From Panacea to Foundational Support, LNCS 2757, pp.381-422, 2002

Formalization and Implementation of Modern SAT Solvers   DBLP  Google Scholar  CiNii
Filip Maric   DBLP  Google Scholar  CiNii
Journal of Automated Reasoning, Vol.43, No.1, pp.81-119, 2009

Algorithms for Maximum Satisfiability using Unsatisfiable Cores   DBLP  Google Scholar  CiNii
João Marques-Silva and Jordi Planes   DBLP  Google Scholar  CiNii
Proceedings of Design, Automation and Test in Europe (DATE 2008), pp.408-413, 2008

GRASP: A Search Algorithm for Propositional Satisfiability   DBLP  Google Scholar  CiNii
João P. Marques-Silva and Karem A. Sakallah   DBLP  Google Scholar  CiNii
IEEE Transactions on Computers, Vol.48, No.5, pp.506-521, 1999

Applying SAT Methods in Unbounded Symbolic Model Checking   DBLP  Google Scholar  CiNii
Kenneth L. McMillan   DBLP  Google Scholar  CiNii
Proceedings of the 14th International Conference on Computer Aided Verification (CAV 2002), LNCS 2404, pp.250-264, 2002

Group Construction of Covering Arrays   DBLP  Google Scholar  CiNii
Karen Meagher and Brett Stevens   DBLP  Google Scholar  CiNii
Journal of Combinatorial Designs, Vol.13, No.1, pp.70-77, 2005

Good Learning and Implicit Model Enumeration   DBLP  Google Scholar  CiNii
António Morgado and João P. Marques Silva   DBLP  Google Scholar  CiNii
Proceedings of the 17th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2005), pp.131-136, 2005

Chaff: Engineering an Efficient SAT Solver   DBLP  Google Scholar  CiNii
Matthew W. Moskewicz and Conor F. Madigan and Ying Zhao and Lintao Zhang and Sharad Malik   DBLP  Google Scholar  CiNii
Proceedings of the 38th Design Automation Conference (DAC 2001), pp.530-535, 2001

Analytic and Algorithmic Solution of Random Satisfiability Problems   DBLP  Google Scholar  CiNii
M. Mézard and G. Parisi and R. Zecchina   DBLP  Google Scholar  CiNii
Science, Vol.297, pp.812-815, 2002

Effective SAT Planning by Speculative Computation   DBLP  Google Scholar  CiNii
Hidetomo Nabeshima and Koji Iwanuma and Katsumi Inoue   DBLP  Google Scholar  CiNii
Proceedings of the 15th Australian Joint Conference on Artificial Intelligence, LNCS 2557, pp.726-727, 2002

Lemma Reusing for SAT based Planning and Scheduling   DBLP  Google Scholar  CiNii
Hidetomo Nabeshima and Takehide Soh and Katsumi Inoue and Koji Iwanuma   DBLP  Google Scholar  CiNii
Proceedings of the International Conference on Automated Planning and Scheduling 2006 (ICAPS 2006), pp.103-112, 2006

Combining Satisfiability Procedures by Equality Sharing   DBLP  Google Scholar  CiNii
G. Nelson   DBLP  Google Scholar  CiNii
Automated Theorem Proving: After 25 years, American Mathematical Society, Vol.29, pp.201-211, 1984

Fast Decision Procedures Based on Congruence Closure   DBLP  Google Scholar  CiNii
Greg Nelson and Derek C. Oppen   DBLP  Google Scholar  CiNii
Journal of the ACM, Vol.27, No.2, pp.356-364, 1980

Simplification by Cooperating Decision Procedures   DBLP  Google Scholar  CiNii
Greg Nelson and Derek C. Oppen   DBLP  Google Scholar  CiNii
ACM Transactions on Programming Languages and Systems, Vol.1, No.2, pp.245-257, 1979

A Tableau Calculus for Minimal Model Reasoning   DBLP  Google Scholar  CiNii
Ilkka Niemelä   DBLP  Google Scholar  CiNii
Proceedings of the 5th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX 1996), LNCS 1071, pp.278-294, 1996

DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic   DBLP  Google Scholar  CiNii
Robert Nieuwenhuis and Albert Oliveras   DBLP  Google Scholar  CiNii
Proceedings of the 17th International Conference on Computer Aided Verification (CAV 2005), LNCS 3576, pp.321-334, 2005

Proof-Producing Congruence Closure   DBLP  Google Scholar  CiNii
Robert Nieuwenhuis and Albert Oliveras   DBLP  Google Scholar  CiNii
Proceedings of the 16th International Conference on Term Rewriting and Applications (RTA 2005), LNCS 3467, pp.453-468, 2005

Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)   DBLP  Google Scholar  CiNii
Robert Nieuwenhuis and Albert Oliveras and Cesare Tinelli   DBLP  Google Scholar  CiNii
Journal of the ACM, Vol.53, No.6, pp.937-977, 2006

Paramodulation-Based Theorem Proving   DBLP  Google Scholar  CiNii
Robert Nieuwenhuis and Albert Rubio   DBLP  Google Scholar  CiNii
Handbook of Automated Reasoning, Elsevier and MIT Press, pp.371-443, 2001

Upper Bounds for Covering Arrays by Tabu Search   DBLP  Google Scholar  CiNii
Kari J. Nurmela   DBLP  Google Scholar  CiNii
Discrete Applied Mathematics, Vol.138, No.1-2, pp.143-152, 2004

Reasoning About Recursively Defined Data Structures   DBLP  Google Scholar  CiNii
Derek C. Oppen   DBLP  Google Scholar  CiNii
Journal of the ACM, Vol.27, No.3, pp.403-411, 1980

Complexity, Convexity and Combinations of Theories   DBLP  Google Scholar  CiNii
Derek C. Oppen   DBLP  Google Scholar  CiNii
Theoretical Computer Science, Vol.12, pp.291-302, 1980

A $2^2^2^pn$ Upper Bound on the Complexity of Presburger Arithmetic   DBLP  Google Scholar  CiNii
Derek C. Oppen   DBLP  Google Scholar  CiNii
Journal of Computer and System Sciences, Vol.16, No.3, pp.323-332, 1978

On the Complexity of Integer Programming   DBLP  Google Scholar  CiNii
Christos H. Papadimitriou   DBLP  Google Scholar  CiNii
Journal of the ACM, Vol.28, No.4, pp.765-768, 1981

Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference   DBLP  Google Scholar  CiNii
Judea Pearl   DBLP  Google Scholar  CiNii
Morgan Kaufmann, 1988

Building Structure into Local Search for SAT   DBLP  Google Scholar  CiNii
Duc Nghia Pham and John Thornton and Abdul Sattar   DBLP  Google Scholar  CiNii
Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007), pp.2359-2364, 2007

RSat 2.0: SAT Solver Description   DBLP  Google Scholar  CiNii
Knot Pipatsrisawat and Adnan Darwiche   DBLP  Google Scholar  CiNii
No.D-153, 2007

Ordered Semantic Hyper-Linking   DBLP  Google Scholar  CiNii
David A. Plaisted and Yunshan Zhu   DBLP  Google Scholar  CiNii
Journal of Automated Reasoning, Vol.25, No.3, pp.167-217, 2000

CNF Encodings   DBLP  Google Scholar  CiNii
Steven David Prestwich   DBLP  Google Scholar  CiNii
Handbook of Satisfiability, IOS Press, pp.75-97, 2009

Variable Dependency in Local Search: Prevention Is Better Than Cure   DBLP  Google Scholar  CiNii
Steven David Prestwich   DBLP  Google Scholar  CiNii
Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007), LNCS 4501, pp.107-120, 2007

Trends in Constraint Programming   DBLP  Google Scholar  CiNii
Steven David Prestwich   DBLP  Google Scholar  CiNii
ISTE, pp.269-274, 2007

Local Search on SAT-encoded Colouring Problem   DBLP  Google Scholar  CiNii
Steven David Prestwich   DBLP  Google Scholar  CiNii
Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), LNCS 2919, pp.105-119, 2003

Efficiency and Stability of Hypergraph SAT Algorithms   DBLP  Google Scholar  CiNii
Daniele Pretolani   DBLP  Google Scholar  CiNii
Proceedings of the Second DIMACS Implementation Challenge, 1993

Encodings of Bounded LTL Model Checking in Effectively Propositional Logic   DBLP  Google Scholar  CiNii
Juan Antonio Navarro Pérez and Andrei Voronkov   DBLP  Google Scholar  CiNii
Proceedings of the 21st International Conference on Automated Deduction (CADE-21), LNCS 4603, pp.346-361, 2007

Satisfiability Modulo Theories   DBLP  Google Scholar  CiNii
Silvio Ranise and Cesare Tinelli   DBLP  Google Scholar  CiNii
Trends and Controversies - IEEE Intelligence Systems Magazine, Vol.21, No.6, pp.71-81, 2006

Planning and SAT   DBLP  Google Scholar  CiNii
Jussi Rintanen   DBLP  Google Scholar  CiNii
Handbook of Satisfiability, IOS Press, pp.483-504, 2009

Regression for Classical and Nondeterministic Planning   DBLP  Google Scholar  CiNii
Jussi Rintanen   DBLP  Google Scholar  CiNii
Proceedings of the 18th European Conference on Artificial Intelligence (ECAI 2008), FAIA 178, pp.568-572, 2008

A Planning Algorithm not based on Directional Search   DBLP  Google Scholar  CiNii
Jussi Rintanen   DBLP  Google Scholar  CiNii
Proceedings of the 6th nternational Conference on Principles of Knowledge Representation and Reasoning (KR 1998), pp.617-625, 1998

Planning as Satisfiability: Parallel Plans and Algorithms for Plan Search   DBLP  Google Scholar  CiNii
Jussi Rintanen and Keijo Heljanko and Ilkka Niemelä   DBLP  Google Scholar  CiNii
Artificial Intelligence, Vol.170, No.12-13, pp.1031-1080, 2006

A Machine-Oriented Logic Based on the Resolution Principle   DBLP  Google Scholar  CiNii
John Alan Robinson   DBLP  Google Scholar  CiNii
Journal of the ACM, Vol.12, No.1, pp.23-41, 1965

CO-PLAN: Combining SAT-Based Planning with Forward-Search   DBLP  Google Scholar  CiNii
Nathan Robinson and Charles Gretton and Duc-Nghia Pham   DBLP  Google Scholar  CiNii
Proceedings of the 6th International Planning Competition (IPC-6), 2008

On the Hardness of Approximate Reasoning   DBLP  Google Scholar  CiNii
Dan Roth   DBLP  Google Scholar  CiNii
Artificial Intelligence, Vol.82, No.1-2, pp.273-302, 1996

Generalized Arc Consistency for Global Cardinality Constraint   DBLP  Google Scholar  CiNii
Jean-Charles Régin   DBLP  Google Scholar  CiNii
Proceedings of the 13th National Conference on Artificial Intelligence (AAAI 1996), Vol.1, pp.209-215, 1996

A Filtering Algorithm for Constraints of Difference in CSPs   DBLP  Google Scholar  CiNii
Jean-Charles Régin   DBLP  Google Scholar  CiNii
Proceedings of the 12th National Conference on Artificial Intelligence (AAAI 1994), pp.362-367, 1994

QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency   DBLP  Google Scholar  CiNii
Ashish Sabharwal and Carlos Ansótegui and Carla P. Gomes and Justin W. Hart and Bart Selman   DBLP  Google Scholar  CiNii
Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT 2006), LNCS 4121, pp.382-395, 2006

Combining Component Caching and Clause Learning for Effective Model Counting   DBLP  Google Scholar  CiNii
Tian Sang and Fahiem Bacchus and Paul Beame and Henry A. Kautz and Toniann Pitassi   DBLP  Google Scholar  CiNii
Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), LNCS 3542, 2004

Solving Bayesian Networks by Weighted Model Counting   DBLP  Google Scholar  CiNii
Tian Sang and Paul Beame and Henry Kautz   DBLP  Google Scholar  CiNii
Proceedings of the 20th National Conference on Artificial Intelligence (AAAI 2005), pp.475-482, 2005

PaMiraXT: Parallel SAT Solving with Threads and Message Passing   DBLP  Google Scholar  CiNii
Tobias Schubert and Matthew Lewis and Bernd Becker   DBLP  Google Scholar  CiNii
Journal on Satisfiability, Boolean Modeling and Computation, Vol.6, pp.203-222, 2009

Noise Strategies for Improving Local Search   DBLP  Google Scholar  CiNii
Bart Selman and Henry A. Kautz and Bram Cohen   DBLP  Google Scholar  CiNii
Proceedings of the 12th National Conference on Artificial Intelligence (AAAI 1994), pp.337-343, 1994

Local Search Strategies for Satisfiability Testing   DBLP  Google Scholar  CiNii
Bart Selman and Henry Kautz and Bram Cohen   DBLP  Google Scholar  CiNii
Cliques, Coloring, and Satisfiability: the Second DIMACS Implementation Challenge, American Mathematical Society, Vol.26, pp.521-532, 1996

A New Method for Solving Hard Satisfiability Problems   DBLP  Google Scholar  CiNii
Bart Selman and Hector J. Levesque and David G. Mitchell   DBLP  Google Scholar  CiNii
Proceedings of the 10th National Conference on Artificial Intelligence (AAAI 1992), pp.440-446, 1992

Generating Hard Satisfiability Problems   DBLP  Google Scholar  CiNii
Bart Selman and David G. Mitchell and Hector J. Levesque   DBLP  Google Scholar  CiNii
Artificial Intelligence, Vol.81, No.1-2, pp.17-29, 1996