| Indietro | ||
1.
Michael
N. Barber. Finitesize
scaling. In Phase Transitions and Critical Phenomena, Volume 8, pages 145-266.
Academic Press, 1983
2.
P. Barth. A DavisPutnam based enumeration algorithm
for linear pseudoboolean optimization.
Research report mpii952003, Max Plack Institut fur Informatik,
Saarbrucken, 1995
3.
R. Battiti and M. Protasi. Reactive Search, a history
based heuristic for MAXSAT. Technical
report, Dipartimento di Matematica, Univ. of Trento, Italy
4.
Roberto Bayardo and Robert Schrag. Using CSP lookback techniques to
solve exceptionally hard SAT instances. In Proceedings of Second International
Conference on Principles and Practice of Constraint Programming (CP96),
1996
5.
R. J. Bayardo and D. P. Miranker. A
Complexity Analysis of SpaceBounded Learning Algorithms for the Constraint
Satisfaction Problem. In Proceedings 13th National Conference on Artificial
Intelligence, 558562, 1996
6.
Roberto Bayardo and Robert Schrag. Using
CSP lookback techniques to solve
realworld SAT instances. In Proceedings of the 14th National Conference on AI.
American Association for Artificial Intelligence, 1997
7.
R.
Beigel and D. Eppstein. 3coloring
in time O(1.3446n):
a NoMIS algorithm. Technical
report, ECCC, 1995. TR9533
8.
R.E. Bryant. Symbolic
Boolean manipulation with ordered binarydecision diagrams. ACM Computing
Surveys, 24(3):293-318, 1992
9.
M. Buro and H. Buning. Report on a SAT competition. Technical Report,
Dept. of Mathematics and Informatics, University of Paderborn, Germany, 1992
10.
M.
Cadoli, A. Giovanardi, and M. Schaerf. Experimental analysis of the computational cost of evaluation quantified
Boolean formulae. In Proceedings of the AI*IA97, pages 207-218. SpringerVerlag, LNAI1321, 1997
11.
P. Cheeseman, B. Kanefsky, and W.M. Taylor. Where the really hard
problems are. In Proceedings of the 12th IJCAI, pages 331-337. International
Joint Conference on Artificial Intelligence, 1991
12.
V. Chvatal and B. Reed. Mick gets some (the odds are on his side). In
Proceedings of the 33rd Annual Symposium on Foundations of Computer Science,
pages 620-627. IEEE, 1992
14.
S.A. Cook and D.G. Mitchell. Finding hard instances of the satisfiability
problem: A survey. In Satisfiability Problem: Theory and Applications.
Dimacs Series in Discrete Mathematics and Theoretical Computer Science,
Volume 35, 1997
15.
J.M. Crawford and L.D. Auton. Experimental Results on the CrossOver
Point in Satisfiability Problemes. In Proceedings of AAAI 1993 Spring Symposium
on AI and NPHard Problems, 1993
19.
M. Davis, G. Logemann, and D. Loveland. A machine program for theorem
proving. Comms. ACM, 5:394-397, 1962
20.
M. Davis and H. Putnam. A computing procedure for quantification theory.
Journal of the Association for Computing Machinery, pages 201-215, 1960
21.
R. Dechter and I. Rish. Directional resolution: The DavisPutnam
procedure, revisited. In Proceedings of KR94, pages 134-145, 1994. A longer
version is available from http://www.ics.uci.edu/irinar
22.
O. Dubois, P. Andre, Y. Boufkhad, and J. Carlier. SAT
versus UNSAT. In
Proceedings of the Second DIMACS Challenge, 1993
24.
G.W.
Ernst. A
definitiondriven theorem prover. In Proceedings of the 3rd IJCAI, pages 51-55.
International Joint Conference on Artificial Intelligence, 1973
25.
J. Frank. Learning short term weights for GSAT. In Proceedings of the
14th IJCAI. International Joint Conference on Artificial Intelligence, 1995
26.
J. W. Freeman. Improvements to
Propositional Satisfiability Search Algorithms. Ph.D. Dissertation, U.
Pennsylvania Dept. of Computer and Information Science, 1995
27.
E. Friedgut. Sharp thresholds for graph properties and the kSAT
problem, 1998
28.
Frieze and S. Suen. Analysis of two simple
heuristics on a random instance of kSAT. Journal of Algorithms, 20:312-355,
1996
29.
D. Frost, I. Rish, and L. Vila. Summarizing
CSP hardness with continuous probability distributions. In Proceedings of the
14th National Conferenceon AI, pages 327--333. American Association for
Artificial Intelligence, 1997
30.
Masayuki Fujita, John Slaney and Frank
Bennett. Automatic generation of some results in finite algebra. In Proceedings
of the 13th IJCAI, pages 52-57. International Joint Conference on Artificial
Intelligence, 1993
31.
M.R. Garey and D.S. Johnson. Computers and
intractability: a guide to the theory of NPcompleteness. W.H. Freeman, 1979
32. I.P. Gent. On the stupid algorithm for satisfiability. Technical report, APES031998, 1998, available from http://www.cs.strath.ac.uk/apes/reports/apes031998.ps.gz
33.
I.P.Gent, E. MacIntyre, P. Prosser, and T.
Walsh. The constrainedness of search. In Proceedings of AAAI96, pages 246-252,
1996
34.
I.P. Gent, E. MacIntyre, P. Prosser, and T. Walsh. The scaling of search
cost. In Proceedings of the 14th National Conference on AI, pages 315-320.
American Association for Artificial Intelligence, 1997
35.
Gent
and T. Walsh. The Enigma of SAT Hillclimbing Procedures. Technical Report 605,
Dept. of Artificial Intelligence, University of Edinburgh, 1992
36.
Gent and T. Walsh.
Towards an Understanding of Hillclimbing Procedures for SAT. In Proceedings of
the 11th National Conference on AI.American Association for Artificial
Intelligence, 1993
37.
I.P. Gent and T. Walsh. An empirical analysis of search in GSAT. Journal
of Artificial Intelligence Research, 1:23-57, 1993
38.
I.P.
Gent and T. Walsh. Easy problems are sometimes hard. Artificial
Intelligence, pages 335-345, 1994
39.
I.P.Gent and T. Walsh.
The hardest random SAT problems. In Proceedings of KI94, Saarbrucken, 1994
40.
I.P. Gent and T. Walsh. The SAT phase
transition. In A G Cohn, editor, Proceedings of 11th ECAI, pages 105-109. John
Wiley & Sons, 1994
41.
I.P. Gent and T. Walsh. Unsatisfied variables in local search. Research
Paper 721, Dept. of Artificial Intelligence, University of Edinburgh, 1994.
Presented at AISB95
42.
I.P. Gent and T. Walsh. The satisfiability constraint gap. Artificial
Intelligence, 81(1-2), 1996
43. I.P. Gent and T. Walsh. Beyond np: the QSAT phase transition. Technical report APES051998, 1998, available from http://www.cs.strath.ac.uk/apes/reports/apes051998.ps.gz
44.
I.P. Gent and T. Walsh. The Search for Satisfaction, Department of
Computer Science, University of Strathclyde, Glasgow, 1999
45.
M. Ginsberg and D. McAllester. GSAT and
Dynamic Backtracking, Principles of Knowledge Representation and Reasoning:
Proceedings of the Fourth International Conference, 226237, 1994
46.
F. Giunchiglia and R. Sebastiani. Building
decision procedures for modal logics from propositional decision procedures
the case study of modal k. In Proceedings of the 13th International Conference
on Automated Deduction (CADE13). Springer
Verlag, 1996
47.
F. Giunchiglia and R. Sebastiani. A
SATbased decision procedure for alc. In Proceedings of the 5th International
Conference on Principles of Knowledge. Representation and Reasoning KR'96,
1996
48.
F.
Giunchiglia and R. Sebastiani. A new method for testing decision procedures in modal logics. In
Proceedings of the 14th International Conference on Automated Deduction (CADE14).
Springer Verlag, 1997
49.
P.Y. Gloess. ULog
- a Unified Object Logic, Revue d'intelligence artificielle, Vol. 5, No. 3, pp.
33-66, 1991
50.
F. Glover. Tabu Search - Part I. ORSA
Journal on Computing, 1(3):190-206, 1989
51.
F. Glover. Future path for integer programming and
links to artificial intelligence. Computers & Ops. Res. , 5:533-549, 1993
52.
F. Glover and M. Laguna. Tabu search. In Modern
Heuristic Techniques for Combinatorial Problems, C.R. Reeves (E.), John Wiley
& Sons, 70-150, 1996.
53.
Goerdt. A threshold for unsatisfiability.
In I. Havel and V. Koubek editors, Mathematical Foundations of Computer Science,
Lecture Notes in Computer Science, pages 264-274. Springer
Verlag, 1992
54.
Gomes, B. Selman, and H. Kautz. Boosting
combinatorial search through randomization. In Proceedings of 15th National
Conference on Artificial Intelligence, pages 431-437. AAAI Press - The MIT
Press, 1998
55.
J. Gu. Efficient local search for very largescale satisfiability
problems. SIGART Bulletin, 3(1):8-12, 1992
56.
J. Gu. Global Optimisation for
satisfiability (SAT) problem. IEEE Transactions on Data and Knowledge
Engineering, 6(3):361-381,1994
57.
J. Hansen and B. Jaumard. Algorithms for the maximum satisfiability
problem. Computing, 44, 279-303, 1990
58.
P.Hayes. The naive physics manifesto. In D.
Michie, editor, Expert Systems in the Microelectronic Age. Edinburgh University
Press, 1979
59.
A. Hertz and D. De Werra. Using
tabu search techniques for Graph Coloring. Computing, pages 345-351, 1987
60.
T. Hogg. Quantum computing and phase transitions in combinatorial search.
Journal of Artificial Intelligence Research, 4:91-128, 1996
61.
J. N. Hooker. Resolution vs. cutting plane solution of inference problems:
some computational experience. Operations Research Letters, 7(1):1-7, 1988
62.
J. N. Hooker and C. Fedjki. Branchandcut solution of inference
problems in propositional logic. Annals of Mathematics and Artificial
Intelligence, 1:123--139, 1990
63.
J.N. Hooker. Branchandcut solution of inference problems in
propositional logic. Annals of Mathematics and Artificial Intelligence,
1:123-139, 1990
64.
J.N. Hooker. Solving the incremental satisfiability problem. Journal of
Logic Programming, 15:177-186, 1993
65.
J.N. Hooker and V. Vinay. Branching Rules for Satisfiability. Journal of
Automated Reasoning, 15:359-383, 1995
66.
H. Hoos. Stochastic Local Search Methods, Models, Applications. PhD
thesis, TU Darmstadt, 1998. Available from
http://www.cs.ubc.ca/spider/hoos/publai.html
67.
H. Hoos and T. Stutzle. Evaluating Las Vegas algorithms pitfalls and
remedies. In Proceedings of 14th Annual Conference on Uncertainty in Artificial
Intelligence (UAI98), 1998. Available from
http://www.sis.pitt.edu/~dsl/uai98.html
68.
R.
E. Jeroslow and J. Wang. Solving satisfiability propositional problems. Annals
of Mathematics and Artificial Intelligence, 1:167-187, 1990
69.
D.S. Johnson. Optimization algorithms for combinatorial problems. J. of
Comp. and Sys. Sci., 9:256-279, 1974
71.
Y. Jiang, H. Kautz, and B. Selman. Solving
problems with hard and soft constraints using a stochastic algorithm for MAXSAT.
In First International Joint
Workshop on Artificial Intelligence and Operations Research, 1995
72.
K.A. De Jong and W.M. Spears. Using Genetic Algorithms to Solve
NP-Complete Problems. In Third International Conference on Genetic Algorithms.
Morgan Kaufmann, 1989
74.
A.P.
Kamath, R. Motwani, K. Palem, and P. Spirakis. Tail
bounds for occupancy and the satisfiability threshold conjecture. Randomized
Structure and Algorithms, 7:59-80,
1995
75.
A.P. Kamath, N.K. Karmarkar, K.G. Ramakrishnan, and M.G.C. Resende. An
interior point approach to Boolean vector function synthesis. In Proceedings of
the 36th MSCAS, 1993
76.
K. Kask and R. Dechter. GSAT and local
consistency. In Proceedings of the 14th IJCAI, pages 616-622. International
Joint Conference on Artificial Intelligence, 1995
77.
H.
Kautz and B. Selman. Planning
as Satisfiability. In Proceedings of the 10th ECAI, pages 359-363. European
Conference on Artificial Intelligence, 1992
78.
H. Kautz and B. Selman. Pushing the envelope: planning, propositional
logic, and stochastic search. In Proceedings of the 13th National Conference on
AI, pages 1194-1201. American Association for Artificial Intelligence, 1996
79.
H.
Kautz and B. Selman. BLACKBOX:
A new approach to the application of theorem proving to problem solving. In
Working notes of the Workshop on Planning as Combinatorial Search, 1998. Held in
conjunction with AIPS98, Pittsburgh, PA, 1998
80.
H. Kautz and B. Selman. The
role of domainspecific knowledge in the planning as satisfiability framework.
In Proceedings of AIPS98, Pittsburgh, PA,
1998
81.
S.
Kim, H. Zhang. ModGen: Theorem proving by model generation,
Proceedings of the 12th National Conference on Artificial Intelligence (AAAI94),
pp. 162-167, 1994
82.
S.
Kirkpatrick, C.D. Gelatt Jr., and M.P.Vecchi. Optimisation by Simulated
Annealing. Science, 220:671-680, 1983
83.
S. Kirkpatrick and B. Selman. Criticial comportamento in the
satisfiability of random boolean expressions. Science, 264:1297-1301, 1994
84.
L.M. Kirousis, E. Kranakis, and D. Krizanc. Approximating
the unsatisfiability threshold of random formulas. In Proceedings of the 4th
Annual European Symposium on Algorithms (ESA'96), pages 27-38, 1996
85.
E. Koutsoupias and C.H. Papadimitriou. On the greedy algorithm for
satisfiability. Information Processing Letters, 43:53-55, 1992
86.
T. Larrabee. Test pattern generation using
Boolean satisfiability. IEEE Transactions on ComputerAided Design, pages 4-15,
1992
87.
C.M. Li, Exploiting yet more the power of unit clause
propagation to solve 3SAT problem, Proceedings of the ECAI'96 Workshop on
Advances in propositional deduction, Budapest,
Hungary, pp. 1116, August 1996
88.
C.M. Li and Anbulagan. Heuristics based on
unit propagation for satisfiability problems. In Proceedings of the 15th IJCAI,
pages 366-371. International Joint Conference on Artificial Intelligence, 1997
89.
C.M. Li
and Anbulagan, Look-ahead versus look-back for satisfiability problems, in
preceedings of third international conference on Principles and Practice of
Constraint Programming - CP97, Springer-Verlag, LNCS 1330, Page 342-356,
Autriche, 1997.
90.
R.J.
Lipton. Using
DNA to solve NPcomplete problems. Science, 268:542-545, 1995
91.
M. Mazure, L. Sais and E. Gregoire.
Detecting Logical Inconsistencies. In Proc. of the Fourth International
Symposium on Artificial Intelligence and Mathematics, 116121, 1996
92.
M. Mazure, L. Sais, and E. Gregoire. Tabu search for SAT. In Proceedings
of 14th National Conference on Artificial Intelligence, pages 281-285. American
Association for Artificial Intelligence, AAAI Press/The MIT Press, 1997
93.
McAllester, B. Selman, and H. Kautz. Evidence for invariants in local
search. In Proceedings of the 14th National Conference on AI, pages 321-327.
American Association for Artificial Intelligence, 1997
94.
W.
W. McCune. Otter
user’s guide 0.91. Maths and CS Division, Argonne National Laboratory, Argonne,
Illinois, 1988
95.
P. Meseguer and T. Walsh. Interleaved and discrepancy based search. In
Proceedings of the 13th ECAI. European Conference on Artificial Intelligence,
Wiley, 1998
96.
S.
Minton, M.D. Johnston, A.B. Philips, and P. Laird. Solving largescale
constraint satisfaction and scheduling problems using a heuristic repair method.
In Proceedings of AAAI'90, pages 17-24, 1990
97.
S. Minton, M.D. Johnston, A.B. Philips, and P. Laird. Minimizing
Conflicts: A Heuristic Repair Method for Constraint Satisfaction and Scheduling
Problems. Artificial Intelligence, 52:161-205, 1992
98.
D. Mitchell, B. Selman, and H. Levesque.
Hard and Easy Distributions of SAT Problems. In Proceedings of the 10th National
Conference on AI, pages 459-465. American Association for Artificial
Intelligence, 1992
99.
P. Morris. The Breakout method for escaping from local minima. In
Proceedings of the 11th National Conference on AI. American Association for
Artificial Intelligence, 1993
100.
Jens
Otten. On the Advantage of a NonClausal DavisPutnam Procedure. Technical
Report AIDA-97-01, FG Intellektik, FB Informatik, TH Darmstadt, January 1997
101.
C.H. Papadimitriou and K. Steiglitz. Combinatorial
optimization. Englewood Cliffs, NJ: PrenticeHall Inc, 1982
102.
C.H. Papadimitriou. On selecting a satisfying truth assigment. In
Proceedings of the Conference on the Foundations of Computer Science, pages
163-169, 1991
103.
C.H. Papadimitriou. Computational Complexity. AddisonWesley, 1994
104.
P. Pandurang Nayak and B.C. Williams. Fast context switching in realtime
propositional reasoning. In Proceedings of the 14th National Conference on AI.
American Association for Artificial Intelligence, 1997
105.
A.J. Parkes and J.P. Walser. Tuning local
search for satisfiability testing. In Proceedings of AAAI96, pages 356-362,
1996
106.
D.
Pretolani. Satisfiability and hypergraphs,
Ph.D. Thesis, Dipartimento di Informatica, Universita di Pisa, 1993
107.
P. Prosser. Hybrid Algorithms for the
Constraint Satisfaction Problem. Computational Intelligence 9(3):268299, 1993
108.
Paul Walton Purdom Jr. and Cynthia A.
Brown. The pure literal rule and polynomial average time. SIAM Journal of
Computing, 14(4):943--953, November
1985
109. R.
Reiter and A. Mackworth. A logical framework for depiction and image
interpretation. Artificial Intelligence, 42(2):125-155, 1989
110.
R. Rodosek. A new approach on solving 3Satisfiability. In Proceedings
of the 3rd International Conference on Artificial Intelligence and Symbolic
Mathematical Computation, pages 197-212. Springer, LNCS 1138, 1996
111.
R. Schrag and J. M. Crawford. Implicates
and Prime Implicates in Random 3SAT. Artificial Intelligence 81(12), 199222,
1996
112.
B. Selman and H. Kautz. Domainindependent extensions to GSAT: Solving
large structured satisfiability problems. In Proceedings of the 13th IJCAI.
International Joint Conference on Artificial Intelligence, 1993
113.
B. Selman and H. Kautz. An empirical study of greedy local search for
satisfiability testing. In Proceedings of the 11th National Conference on AI,
pages 46-51. American Association for Artificial Intelligence, 1993
114.
B.
Selman, H. Kautz, and B. Cohen. Noise
Strategies for Improving Local Search. In Proceedings of the 12th National
Conference on AI, pages 337- 343. American Association for Artificial
Intelligence, 1994
115.
B. Selman and S. Kirkpatrick. Critical behaviour in the computational
cost of satisfiability testing. Artificial Intelligence, 81:273-295, 1996
116.
B.
Selman, H. Levesque, and D. Mitchell. A New Method for Solving Hard
Satisfiability Problems. In Proceedings of the 10th National Conference on AI,
pages 440-446. American Association for Artificial Intelligence, 1992
117.
J.P. Silva., K.A. Sakallah. Conflict Analysis in Search Algorithms for propositional
satisfiability, Proceedings of the International Conference on
Tools with Artificial Intelligence, November 1996
118.
J. Slaney, M. Fujita, and M. Stickel. Automated reasoning and exhaustive
search: quasigroup existence problems. Computers and Mathematics with
Apllications, 29:115-132, 1995
119.
Raymond
M Smullyan. First Order Logic. SpringerVerlag,
Berlin, 1968
120.
W.M. Spears. A nn algorithm for boolean satisfiability problems. In
Proceedings of the 1996 International Conference on Neural Networks, pages
1121-1126, 1996
121.
W.M. Spears. Simulated annealing for hard
satisfiability problems. In D.S. Johnson and M.A. Trick editors, In Cliques,
Coloring, and Satisfiability: Second DIMACS Implementation Challenge, pages
533-558. DIMACS Series in Discrete Mathematics and Theoretical Computer Science,
Volume 26, American Mathematical Society,
1996
122.
P. R.
Stephan, R. K.Brayton, A. L. SangiovanniVincentelli. Combinational
Test Generation Using satisfiability,
Memorandum No. UCB/ERL M92/112, EECS Department, University of California at
Berkeley, October 1992
123.
T.E. Uribe and M.E. Stickel. Ordered binary decision diagrams and the
DavisPutnam procedure. In Proceedings of the First International Conference on
Constraints in Computational Logics, Munich, Germany, pages
34-49, 1994
124.
van Gelder and Y.K. Tsuji. Satisfiability
testing with more reasoning and less guessing. In D.S. Johnson and M.A. Trick
editors, In Cliques, Coloring, and Satisfiability: Second DIMACS Implementation
Challenge. DIMACS Series in Discrete Mathematics and Theoretical Computer
Science, Volume 26, American Mathematical Society,
1996
125.
J.P. Walser. Solving linear pseudoboolean
constraints with local search. In Proceedings of the 14th National Conference on
AI, pages 269--274. American Association for Artificial Intelligence, 1997
126.
B.C. Willians and P. Pandurang Nayak. A
modelbased approach to reactive selfconfiguring systems. In Proceedings of
the 13th National Conference on AI. American Association for Artificial
Intelligence, 1996
127.
N. Yugami. Theoretical analysis of DavisPutnam
procedure and propositional satisfiability. In Proceedings of IJCAI95, pages
282-288, 1995
128.
H. Zhang. SATO: An efficient propositional prover. In Proceedings of 14th
Conference on Automated Deduction, pages 272-275, 1997
129. H. Zhang. Specifying Latin squares in propositional logic. In R. Veroff, editor, Automated Reasoning and Its Applications, Essays in honor of Larry Wos, chapter 6. MIT Press, 1997
130.
H. Zhang, M.P. Bonacina, and J. Hsiang. Psato: A distributed
propositional prover and its application to quasigroup problems. Journal of
Symbolic Computation, 11:1-18, 1996
131.
H. Zhang and Stickel M. Implementing the DavisPutnam Algorithm by Tries.
Technical report, University of Iowa, 1994
132.
H. Zhang and M.E. Stickel. An efficient
algorithm for unit propagation. In Working
Notes of the Fourth International Symposium on Artificial Intelligence and
Mathematics, Fort Lauderdale, Florida, 1996
133. J.
Zhang and H. Zhang. SEM: a System for Enumerating Models. In Proceedings of
IJCAI95, volume 1,
pages 298-303. International Joint Conference on Artificial Intelligence, 1995
134.
J. Zhang and H. Zhang. Combining local search and backtracking techniques
for constraint Satisfaction. In Proceedings of 13th National Conference on
Artificial Intelligence, pages 369-374. American Association for Artificial
Intelligence, AAAI Press/The MIT Press, 1996
| Indietro | ||
| Links benchmark |
SAT solver |
Download |