Abbass H.A.
A Single Queen Single Worker Honey Bees Approach to
3-SAT.
Genetic and Evolutionary Computation
Conference, GECCO2001, San Francisco, USA, 2001.
[
3-SAT, swarm algorithms
]
Abbass H.A.
Marriage in Honey Bees Optimisation: A Haplometrosis Polygynous Swarming
Approach.. Congress on Evolutionary Computation, CEC2001,
Seoul, Korea, 2001.
[
3-SAT, swarm algorithms
]
Bayardo Jr., R. J.; Schrag, R. C.
Using CSP look-back techniques to solve real world SAT instances.
In: Proc. of the 14th National Conf. on Artificial Intelligence,
pp. 203-208, 1997.
[
SAT, complete algorithms, learning.
]
Barth, P.
A Davis-Putnam Based Enumeration Algorithm for Linear pseudo-Boolean Optimization.
MPI Technical Report, MPI-I-95-2-003, 1995.
[
SAT, complete algorithms, Davis Putnam, constraint programming, 0-1 problems.
]
Barth, P.; Bockmayr, A.
Modelling 0-1 problems in CLP(PB).
MPI Technical Report, 1996.
[
Constraint programming, 0-1 problems.
]
Bockmayr, A.; Kasper, T.
Pseudo-Boolean and Finite Domain Constraint Programming: A Case Study.
MPI Technical Report, 1996.
[
Constraint programming, 0-1 problems.
]
Bayardo Jr., R. J.; Schrag, R. C.
Using CSP look-back techniques to solve exceptionally hard SAT instances.
In: Proc. of the Second Int'l Conf. on Principles
and Practice of Constraint Programming (Lecture Notes in Computer
Science 1118), pp. 46-60, Springer, 1996.
[
SAT, complete algorithms, learning.
]
Beringer, A.; Aschemann, G.; Hoos, Holger H.; Metzger, M.; Weiß, A.
GSAT versus Simulated Annealing.
In: Proc. of ECAI'94, pp. 130-134, John Wiley \& Sons, 1994.
[SAT, local search, random 3-sat, simulated annealing.
]
Biere, A.; Cimatti, A.; Clarke, E.; Zhu, Y.
Symbolic Model Checking without BDDs.
In: Proc. of the Workshop on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS99), lncs, Springer, 1999.
[SAT, bounded model checking]
Cadoli, M.; Giovanardi, A.; Schaerf, M.
Experimental Analysis of the Computational Cost of Evaluating Quantified Boolean Formulae.
Proc. of AI*IA-97, Springer LNAI, 1997.
[
QSAT, algorithms, empirical analysis.
]
Cadoli, M.; Giovanardi, A.; Schaerf, M.
An Algorithm to Evaluate Quantified Boolean Formulae.
Proceedings of AAAI-98, July, 1998.
[
QSAT, algorithms.
]
Cadoli, M.; Schaerf, M.; Giovanardi, A.; Giovanardi, M.
An Algorithm to Evaluate Quantified Boolean Formulae and its
Experimental Evaluation.
Technical report DIS 08-99, March 1999. Significantly extended version
of AI*IA-97 and AAAI-98.
[
QSAT, algorithms, empirical analysis.
]
Clark, Dave; Frank, Jeremy; Gent, Ian; MacIntyre, Ewan;
Tomov, Neven; Walsh, Toby.
Local Search and the Number of Solutions.
Proceedings of CP-96, 1996.
[
SAT, local search, search behaviour, search space analysis,
empirical analysis.
]
Cook, S.A.; Mitchell, D.G.
Finding Hard Instances of the Satisfiability Problem: A Survey.
In: "Satisfiability Problem: Theory and Applications",
DIMACS Series in Discrete Mathematics and Theoretical Computer Science,
American Mathematical Society, 1997.
[
SAT, survey article, applications, hard instances.
]
Frank, J.
Weighting for Godot: Learning heuristics for GSAT.
J. Frank, Proc. AAAI-96.
[
SAT, local search algorithms, GSAT, clause weighting.
]
Freeman, J.W.
Improvements to Propositional Satisfiability Search Algorithms
. PhD thesis, The University of Pennsylvania, 1995.
[
SAT, complete algorithms, Davis Putnam.
]
Gent, I.; Walsh, T.
An Empirical Analysis of Search in GSAT.
Journal of Artificial Intelligence Research,
Vol. 1, September 1993.
[
SAT, local search algorithms, GSAT.
]
Gent, Ian; MacIntyre, Ewan; Prosser, Patrick; Walsh, Toby.
The Constrainedness of Search.
Proceedings of AAAI-96, pages 246-252, 1996.
[
SAT, search, constrainedness, phase transition.
]
Gent, I.; Walsh, T.
Towards an Understanding of Hill-climbing Procedures for SAT.
Proceedings of AAAI-93.
[
SAT, local search algorithms, GenSAT.
]
Gent, I.; Walsh, T.
Unsatisfied Variables in Local Search.
In `Hybrid Problems, Hybrid Solutions' (Proceedings of AISB-95),
Ed. J. Hallam, IOS Press, Amsterdam, 1995, pages 73-85.
[
SAT, local search algorithms, random walk.
]
Gent, Ian; Walsh, Toby.
The SAT Phase Transition.
Proceedings of ECAI-94, ed. A G Cohn, John Wiley & Sons, 105-109, 1994.
[
SAT, phase transition, random 3-sat.
]
Gent, Ian; Walsh, Toby.
Easy Problems are Sometimes Hard.
Artificial Intelligence, 70, 335-345, 1994.
[
SAT, phase transition, constant probability model.
]
Gent, Ian; Walsh, Toby.
The Satisfiability Constraint Gap.
Artificial Intelligence, 81 (1-2), 1996.
[
SAT, phase transition, random 3-sat.
]
Gent, Ian; Walsh, Toby.
Beyond NP: the QSAT phase transition.
Technical report, APES-05-1998, July 1998. To appear in
Proceedings of AAAI-99.
[
QSAT, phase transition, empirical analysis.
]
Gent, Ian; Walsh, Toby.
The Search for Satisfaction.
Draft paper, 1999.
[
SAT, survey article.
]
Giunchiglia, F.; Sebastiani, R.
Building decision procedures for modal logics from propositional
decision procedures - the case study of modal K.
Proceedings of 13th International Conference on Automated Deduction (CADE-13),
Lecture Notes on Artificial Intelligence series. New Brunswick, New Jersey,
USA, 1996.
[
SAT, modal logic, complete algorithms.
]
Giunchiglia, F.; Sebastiani, R.
A SAT-based decision procedure for ALC.
Proceedings of the 5th International Conference on Principles
of Knowledge Representation and Reasoning - KR'96, 1996.
[
SAT, modal logic, complete algorithms.
]
Giunchiglia, F; Roveri, M.; Sebastiani, R.
A new method for testing decision
procedures in modal and terminological logics.
1996 International Workshop on Description Logics - DL'96.
Boston, MA, USA, 1996. Short version also published in Proceedings 14th International Conference on Automated Deduction (CADE-14) with the title
"A new method for testing decision procedures in modal logics".
[
SAT, modal logic, complete algorithms.
]
Guerra e Silva, Luís; Marques-Silva, João P.;
Silveira, Luís M.; Sakallah, Karem A.
Timing Analysis Using Propositional Satisfiability.
Proceedings of the IEEE International Conference on Electronics,
Circuits and Systems (ICECS), September 1998.
[
SAT, applications, hardware.
]
Gu, J.; Purdom, P.W.; Franco, J.; Wah, B.W.
Algorithms for the Satisfiability (SAT) Problem: A Survey.
In: "Satisfiability Problem: Theory and Applications",
DIMACS Series in Discrete Mathematics and Theoretical Computer Science,
American Mathematical Society, pp. 19-152, 1997.
[
SAT, survey article, algorithms.
]
Guerra e Silva, Luís; Marques-Silva, João P.;
Silveira, Luís M.; Sakallah, Karem A.
Realistic Delay Modeling in Satisfiability-Based Timing Analysis,
Proceedings of the IEEE International Symposium on Circuits and
Systems (ISCAS), May 1998.
[
SAT, applications, hardware.
]
Hogg, T.; Huberman, B. A.; Williams, C.
Phase Transitions and the Search Problem.
Tutorial paper, 1996.
[
SAT, search, phase transition.
]
Hoos, Holger H.
SAT-Encodings, Search Space Structure, and Local Search Performance.
In: Proc. of IJCAI'99, pp. 296-302, Morgan Kaufmann, 1999.
[SAT, local search, encodings, empirical analysis, search space analysis.
]
Hoos, Holger H.
On the Run-time Behaviour of Stochastic Local Search Algorithms for SAT.
In: Proc. of AAAI, pp. 661-666, MIT Press, 1999.
[SAT, local search, encodings, search behaviour, empirical analysis.
]
Hoos, Holger H.
Stochastic Local Search - Methods, Models, Applications.
PhD thesis, TU Darmstadt, 1998.
[
SAT, local search, random 3-sat, search behaviour,
empirical analysis, parallel algorithms, applications, planning,
search space analysis.
]
Hoos, Holger H.; Stützle, Thomas.
Towards a Characterisation of the Behaviour of Stochastic Local Search Algorithms for SAT..
Artificial Intelligence, 112, 213-232, 1999.
[
SAT, phase transition, constant probability model.
]
Hoos, Holger H.; Stützle, Thomas
Local Search Algorithms for SAT: An Empirical Evaluation..
To appear in Journal of Automated Reasoning, 2000.
[SAT, local search, search behaviour, empirical analysis.]
Hoos, Holger H.; Stützle, Thomas
SATLIB: An Online Resource for Research on SAT..
In: SAT 2000, Ian Gent, Hans van Maaren, and
Toby Walsh, editors, IOS Press. 2000.
[SAT, benchmark libraries, research resources.]
Hoos, Holger H.
Solving Hard Combinatorial Problems with GSAT - A Case Study..
In: Proceedings of the German Conference on Artificial Intelligence (KI'96),
pp. 197-212, LNCS 1138, 1996.
[SAT, local search, graph colouring.]
Jiang, Yueyun; Kautz, Henry; Selman, Bart.
Solving Problems with Hard and Soft Constraints Using A
Stochastic Algorithm for MAX-SAT".
1st International Joint Workshop on Artificial
Intelligence and Operations Research, 1995.
[
MAX-SAT, applications, steiner trees.
]
Kautz, Henry; McAllester, David; Selman, Bart.
Encoding Plans in Propositional Logic.
Proceedings KR-96, 1996.
[
SAT, applications, planning.
]
Kautz, Henry; Selman, Bart.
Planning as Satisfiability.
Proceedings ECAI-92, 1992.
[
SAT, applications, planning.
]
Kautz, Henry; Selman, Bart.
Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search.
Proceedings AAAI-96, 1996
[
SAT, applications, planning.
]
Kautz, Henry; Selman, Bart.
BLACKBOX: A New Approach to the Application of Theorem Proving
to Problem Solving.
Working notes of the Workshop on Planning as Combinatorial Search,
held in conjunction with AIPS-98, Pittsburgh, PA, 1998.
[
SAT, applications, planning.
]
Kautz, Henry; Selman, Bart.
The Role of Domain-Specific Knowledge in the Planning as
Satisfiability Framework.
Proceedings of AIPS-98, Pittsburgh, PA, 1998.
[
SAT, applications, planning.
]
Kautz, Henry; Selman, Bart; Jiang, Yueyun.
General Stochastic Approach to Solving Problems with Hard and Soft
Constraints".
In The Satisfiability Problem: Theory and Applications,
Dingzhu Gu, Jun Du, and Panos Pardalos (Eds.), DIMACS Series in Discrete
Mathematics and Theoretical Computer Science, vol. 35, American
Mathematical Society, 1997, pages 573-586.
[
MAX-SAT, applications, steiner trees.
]
Kim, S.; Zhang, H.
ModGen: Theorem proving by model generation.
Proc. of National Conference of American Association on
Artificial Intelligence (AAAI-94), Seattle, WA.
MIT Press, pp. 162-167.
[
SAT, First order logic, theorem proving, model generation.
]
Kirousis, L. M.; Kranakis, E.; Krizanc. D.
A Better Upper Bound for the Unsatisfiability Threshold.
Technical report TR-96-09,
School of Computer Science,
Carleton University, 1996.
[
SAT, phase transition, random 3-sat.
]
van Maaren, Hans.
Highlights of Satisfiability Research in the Year 2000 - Preface.
In: SAT 2000 - Highlights of Satisfiability Research in the Year 2000,
Ian Gent, Hans van Maaren, and Toby Walsh, editors, IOS Press. 2000.
[
SAT, survey article.
]
Marques-Silva, João P.
Search Algorithms for Satisfiability Problems in
Combinational Switching Circuits.
Ph.D. Dissertation, EECS Department, University of Michigan, May 1995.
[
SAT, applications, hardware.
]
Marques-Silva, João P.
An Overview of Backtrack Search Satisfiability Algorithms.
In: Fifth International Symposium on Artificial Intelligence and
Mathematics, January 1998.
[
SAT, complete algorithms, Davis Putnam.
]
Marques-Silva, João P.; Sakallah, Karem A.
Conflict Analysis in Search Algorithms for Propositional Satisfiability.
In: Proceedings of the IEEE International Conference on Tools with
Artificial Intelligence, November 1996.
[
SAT, complete algorithms, learning.
]
Marques-Silva, João P.; Sakallah, Karem A.
Robust Search Algorithms for Test Pattern Generation.
Proceedings of the IEEE Fault-Tolerant Computing Symposium,
June 1997.
[
SAT, applications, hardware.
]
McAllester, D.; Selman, B.; Kautz, H.
Evidence for Invariants in Local Search.
Proc. AAAI-97, Providence, RI, 1997.
[
SAT, local search algorithms, WalkSAT.
]
Mitchell, David; Selman, Bart; Levesque, Hector.
Hard and Easy Distribution of SAT Problems.
Proceedings AAAI-92, 1992.
[
SAT, phase transition, random 3-sat.
]
Parkes, A.J.; Walser, J.
Tuning Local Search for Satisfiability Testing.
Proceedings of the 13th National Conference on Artificial Intelligence,
Portland, OR, 1996.
[
SAT, local search, WalkSAT, empirical analysis, random-3-sat.
]
Rintanen, J.
Improvements to the evaluation of quantified Boolean formulae.
Proceedings of the 16th International Joint Conference in Artificial Intelligence,
Stockholm, Sweden, August 1999.
[
QSAT, algorithms.
]
Rodosek, R.
A New Approach on Solving 3-Satisfiability.
In: Proceedings of the 3rd International
Conference on Artificial Intelligence and Symbolic Mathematical Computation,
pp. 197-212, LNCS 1138, Steyr, 1996.
[
SAT, complete algorithms, complexity analysis.
]
Selman, B.; Kautz, H.
An Empirical Study of Greedy Local Search for Satisfiability Testing.
Proc. AAAI-93.
[
SAT, local search algorithms, GSAT, clause weighting.
]
Selman, B.; Kautz, H.
Domain-Independent Extensions to GSAT: Solving Large Structured
Satisfiability Problems.
Proc. IJCAI-93.
[
SAT, local search algorithms, GSAT, random walk.
]
Selman, B.; Kautz, H.; Cohen, B.
Local Search Strategies for Satisfiability Testing.
Proceedings of 2nd DIMACS Challenge on Cliques, Coloring and Satisfiability,
1994.
[
SAT, local search algorithms, WalkSAT.
]
Selman, B.; Levesque, H.; Mitchell, D.
GSAT - A New Method for Solving Hard Satisfiability Problems.
Proceedings AAAI-92.
[
SAT, local search algorithms, GSAT.
]
Singer, Josh; Gent, Ian; Smaill, Alan.
Backbone Fragility and the Local Search Cost Peak.
Journal of Artificial Intelligence
Research, Vol. 12, pp. 235-270, 2000.
[
SAT, local search, search behaviour, search space analysis,
empirical analysis, phase transition, random 3-sat, WalkSAT.
]
Slaney, J.; Fujita, M.; Stickel, M.
Automated reasoning and exhaustive search: quasigroup existence problems.
Computers and Mathematics with Applications 29, 115-132, 1995.
[
SAT, applications, quasigroup existence.
]
Steinmann, Olaf; Strohmeier, Antje; Stützle, Thomas.
Tabu Search vs. Random Walk.
KI-97: Advances in Artificial Intelligence, Springer Verlag, LNCS, Vol. 1303, 1997
[
SAT, local search, tabu search, random walk, constraint satisfaction.
]
Shtrichman, O.
Tuning SAT checkers for Bounded Model Checking.
In: E.A. Emerson and A.P. Sistla Eds, Proc. of Computer Aided Verification
2000 (CAV2000), LNCS, Springer, 2000
[
SAT, bounded model checking
]
Uribe, T.E.; Stickel, M.E.
Ordered binary decision diagrams and the Davis-Putnam procedure.
Proceedings of the First International Conference on Constraints in
Computational Logics, Munich, Germany, September 1994, 34-49.
[
SAT, complete algorithms, Davis Putnam, OBDDs.
]
Walser, Joachim.
Solving Linear Pseudo-Boolean Constraint Problems with Local Search.
Proceedings of the 14th National Conference on Artificial Intelligence,
AAAI-97, Providence, RI, 1997.
[
SAT, local search, WalkSAT, constraint programming, 0-1 problems.
]
Zhang, H.
SATO: An Efficient Propositional Prover.
Proc. of International Conference on Automated Deduction (CADE-97), 1997.
[
SAT, complete algorithms, Davis Putnam.
]
Zhang, Hantao.
Specifying Latin Square Problems in Propositional Logics.
[
SAT, applications, quasigroup existence.
]
Zhang, H.; Bonacina, Maria Paola.
Cumulating Search in a Distributed Computing Environment:
A Case Study in Parallel Satisfiability..
In: Proceedings of First Int. Symp. on Parallel Symbolic
Computation, 1994.
[
SAT, complete algorithms, parallel algorithms.
]
Zhang, Hantao; Bonacina, Maria Paola; Hsiang, Jieh.
PSATO: A Distributed Propositional Prover and Its
Application to Quasigroup Problems.
Journal of Symbolic Computation, 11, 1-18, 1996.
[
SAT, complete algorithms, parallel algorithms.
]
Zhang, Hantao; Hsiang, Jieh.
Solving Open Quasigroup Problems by Propositional Reasoning.
[
SAT, applications, quasigroup existence.
]
Zhang, H.; Stickel, M.
Implementing Davis-Putnam's method by tries.
Technical Report, The University of Iowa, 1994.
[
SAT, complete algorithms, Davis Putnam.
]
Zhang, H.; Stickel, M.
An efficient algorithm for unit-propagation.
In: Proc. of the Fourth International Symposium on Artificial
Intelligence and Mathematics. Ft. Lauderdale, Florida, 1996.
[
SAT, complete algorithms, Davis Putnam.
]