forked from motib/LearnSAT
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathlearnsat.bib
122 lines (109 loc) · 2.85 KB
/
learnsat.bib
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
@unpublished{miller-lang,
author={J.E. Miller},
title={{Langford's Problem}},
note={\url{http://dialectrix.com/langford.html}},
}
@book{knuth-sat,
author={D.E. Knuth},
title={The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability},
publisher={Pearson},
note={ISBN 978-0-1343-9760-3},
year={2015}
}
@article{brute,
author = {Heule, Marijn J. H. and Kullmann, Oliver},
title = {The Science of Brute Force},
journal = {Commun. ACM},
volume = {60},
number = {8},
year = {2017},
doi={10.1145/3107239},
pages = {70--79},
}
@book{SAT,
title={Handbook of Satisfiability},
editor={A. Biere and M. Heule and H. Van Maaren and T. Walsh},
year=2009,
note={ISBN 978-1-60750-376-7},
publisher={{IOS} Press},
}
@book{mlcs,
title={Mathematical Logic for Computer Science (Third Edition)},
author={M. Ben-Ari},
publisher={Springer},
note={ISBN 978-1-4471-4129-7},
year=2012,
}
@inbook{mlm,
Author = {Marques-Silva, J. P. and Lynce, I. and Malik, S.},
Title = {Conflict-Driven Clause Learning SAT Solvers},
Chapter = {4},
Pages = {131--153},
doi={10.3233/978-1-58603-929-5-131},
Crossref = {SAT}
}
@inbook{look,
author = {Heule, Marijn J. H. and {van Maaren, H.}},
Title = {Look-Ahead Based SAT Solvers},
Chapter = {5},
Pages = {155--184},
doi={10.3233/978-1-58603-929-5-155},
Crossref = {SAT}
}
@inbook{bmc,
Author = {Biere, A.},
Title = {Bounded Model Checking},
Chapter = {14},
Pages = {457--481},
doi={10.3233/978-1-58603-929-5-457},
Crossref = {SAT}
}
@inbook{cnf,
Author = {Prestwich, S.},
Title = {CNF Encodings},
Chapter = {2},
Pages = {75--97},
doi={10.3233/978-1-58603-929-5-75},
Crossref = {SAT}
}
@article{mz,
author = {Malik, S. and Zhang, L.},
title = {Boolean satisfiability from theoretical hardness to practical success},
journal = {Commun. ACM},
volume = {52},
number = {8},
year = {2009},
doi = {10.1145/1536616.1536637},
pages = {76--82},
}
@article{ms,
author = {Marques-Silva, J. P. and Sakallah, K. A.},
title = {GRASP: A search algorithm for propositional satisfiability},
journal= {IEEE Transactions on Computers},
volume=48,
number=5,
year = {1999},
doi={10.1109/12.769433},
pages = {506--521},
}
@article{nadel,
author = {Nadel, B.A.},
title = {Representation Selection for Constraint Satisfaction: A Case Study Using n-Queens},
journal = {IEEE Expert: Intelligent Systems and Their Applications},
volume = {5},
issue = {3},
month = {June},
year = {1990},
doi={10.1109/64.54670},
pages = {16--23},
}
@article{primer,
author = {Ben-Ari, M.},
title = {A primer on model checking},
journal = {ACM Inroads},
issue_date = {March 2010},
volume = {1},
number = {1},
doi={10.1145/1721933.1721950},
pages = {40--47},
}