Comparison with SAT
The Scenario
- N trolleys, all pushed and pulled together, all spin
- Increasing N gives increasing problem size
- Compare Mueller's SAT reasoner with ATP solution
- ATP clauses as counted by E (but times by Vampire)
Results
|
|
| SAT reasoner
| ATP reasoner
|
| N
| Clauses
| Time
| Clauses
| Time
|
|
| 1
| 70
| 0.2
| 845
| 1.0
|
| 2
| 328
| 0.3
| 864
| 1.1
|
| 4
| 1084
| 0.7
| 1124
| 1.4
|
| 8
| 3562
| 2.4
| 66468
| 7.8
|
| 9
| 4446
| 3.0
| 263097
| 26.0
|
| 10
| 5428
| 3.9
| 1049553
| Timeout
|
|