SatSolvers Ranklist Generators Ranklist

Stats for formula: Tree Prophet-1

How to interpret the values

Each satsolver was run against each test case. Two cnf formulas were generated from each submitted generator to form the set of generators. For each run, a number of seconds were charged to the program based on the criteria described on the assignments webpage; this was the score for that run. If the program crashed or went into a loop, 150 seconds were charged. The two formulas generated by a generator are denoted by generator_name:i where i is 0 for the first cnf and 1 for the second. The table below shows the time each satsolver took for cnf Tree Prophet-1 and how many clauses it left unsatisfied. A blank symbol denotes the satsolver took more than 150 seconds for cnf Tree Prophet-1 or terminated with an exception. Some important stats are summarized at the start.The ranking scheme is described on the Generators Ranklist page. Click on the name of a satsolver to see details of that satsolver.

Summary

Cnf: Tree Prophet-1
Rank of generator: 74 / 114
Average score: 3.22
Median score: 0.04
Best solver: haoyu
Description: This generator generates Christmas shopping problems in which a set of children each specify 3 presents. The "angel" children who have been really good specify one present they really want or (up to) two second best, forming a constraint of the form P1 v (P2 ^ P3). The average child will specify one present he really wants and (up to) two he absolutely doesn't want, forming a constraint of the form P1 v (~P2 ^ ~P3). And the "naughty" child will specify one present he really doesn't want or (up to) two other presents that he really doesn't want, forming a constraint of the form ~P1 v (~P2 ^ ~P3). These clauses are converted to CNF form using the law of distribution. The number of children (200) and presents(400) are static and the percentage of angel (20%) and naughty children (30%) are stati such that the actual number of naughty and angel children change with each iteration but the total number of children and presents to select from are constant.
Solver Time taken Unsat
1haoyu 0.00 0
2Elphaba 0.00 0
3Glenn Fisher 0.01 0
4Mercury 0.01 0
513a 0.01 0
6jgs 0.01 0
7KingBach 0.01 0
8Jameh 0.01 0
9dusty 0.01 0
10Yan Wu 0.01 0
11Green "The Bean" Choi 0.01 0
12burrito 0.01 0
13jabreezy 0.01 0
14David H. 0.01 0
15NA 0.02 0
16Nikhilesh Sigatapu 0.02 0
17spl 0.02 0
18Keji Xu 0.02 0
19Charlie Shucheng Zhu 0.02 0
20bfang 0.02 0
21T. Capote 0.02 0
22Jonathan Kwok 0.02 0
23Lisa Kim 0.02 0
24Aaron H 0.02 0
25Mr. Blobby 0.02 0
26EC 0.02 0
27An Extremely Ordinary Sloth0.02 0
28Andys 0.02 0
29Deric Cheng 0.02 0
30ModifiedWalkSatBreakZero 0.02 0
31R. A. B. 0.02 0
32Mark Fillmore 0.02 0
33Linda 0.03 0
34Anon5 0.03 0
35Shaheed Chagani 0.03 0
36Solving For Clauses 0.03 0
37dfshasdsf12 0.03 0
38Ben Chen 0.03 0
39AFC 0.03 0
40John Whelchel 0.03 0
41CAPS LOCK 0.03 0
42Janie Gu 0.03 0
43Khoa 0.03 0
44bigwig 0.03 0
45Quite Satisfied 0.03 0
46Absurdity 0.03 0
47Dr Roberto 0.03 0
48Sunny 0.04 0
49RedOrangeBlue 0.04 0
50Walter Little 0.04 0
51Matt Haake 0.04 0
52Tree Prophet 0.04 0
53DeeEmEm 0.04 0
54soccer 0.04 0
55HashTagAlreadyFallBreak 0.04 0
56BH 0.04 0
57CookieMonster 0.04 0
58Yacob Y. 0.04 0
59Tao 0.04 0
60snowflakes 0.05 0
61kt4124 0.05 0
62Valya Barboy 0.05 0
63Andrew Grasso 0.05 0
64Mike Hawk 0.05 0
65Joshua Zimmer 0.06 0
66Fanny 0.06 0
67Blam 0.06 0
68Aaron Doll 0.07 0
69Matt Goldsmith 0.07 0
70Aristotle 0.07 0
71Andrew Werner 0.09 0
72The Whitman Whale 0.09 0
73ebp 0.10 0
74Sabar Dasgupta 0.10 0
75vhsiao 0.11 0
76Joel Faron 0.12 0
77Qinlan Shen 0.15 0
780108 0.15 0
79Jordan Ash 0.19 0
80Sally Smith 0.22 0
81Brendan Wright 0.25 0
82Tom T 0.26 0
83David Lackey 0.28 0
84Jessie Chen 0.30 0
85cjt 0.31 0
86Alex Fish 0.33 0
87weezy 0.43 0
88Mike Honcho 0.60 0
89Tiny Wings 0.78 0
90Gewang 1.54 0
91Mickey Mouse 2.37 0
92Ravi Tandon 2.39 0
93Samuel Jerome 15.00 1
94bchouSolver 15.00 4
95Boomshanka 15.00 5
96cat 14.99 14
97George Okeowo 0.04 30
98Bar Shabtai 15.00 47
99Anon_K_P 15.00 54
100Supahaka 0.05 58
101The Kraken 15.00 64
102BMJ 15.00 65
103Cam Porter 15.00 83
104K.L. 15.00 250
105Ytterbium 15.00 1
106SuperFan 15.00 1
107Nihar the Great 15.00 3
108cmF5a3ly 15.00 5
109LilThug 15.00 5
110Bebe Shi 15.00 6
111Sprt 15.00 7
112Miranda 15.00 9
113Happy 15.00 10
114Bob Dondero 15.00 28
115Sat Solver 2013 15.00 34
116TSATTER 15.00 100
117David Paulk - -
118Igor - -


SatSolvers Ranklist Generators Ranklist