USC-ISI's ATTEND PROJECT

SAT Encoding of SNAP's single time-slot Model Problem

Problem Description and Encoding Document

[ PDF ]

Downlodable XML Marbles Problems

So far, using walksat35, we've only manage to solve formulas with K <= 55, formulas in the pink zone were not yet solved

These runs were done running the "at least K" implementation for the value of K indicated in the header of each table
WSAT was run using the values of "number of tries" and "number of solutions" given in the table. The Otimization value and number of missions filled correspond to the best solution found among all solutions returned by WSAT (most of the time the number of returned solutions was equal to the entered "number of solutions")
The SAT results are compared to those from a Simulated Annealing implementation
The values in "Solved In" account only for the time it took WSAT to find the solutions for the formula in the "input formula.cnf" file

Problem 1: 100 Resources \| 100 Tasks \| k=20
input formula cnf file	[CNF]
results cnf file	[CNF]
Number of Clauses=	95808
Number of Variables=	5345
Number of Tries=	1000
Number of Solutions=	1000
Optimization Value=	12504
Solved in (secs)=	197.3
Number of missions filled=	37
Simulated Annealing Optimization Value=	18135
Simulated Annealing Solved in (secs)=	11.8
Simulated Annealing Number of missions filled=	53

Problem 2: 100 Resources \| 30 Tasks \| k=27
input formula cnf file	[CNF]
results cnf file	[CNF]
Number of Clauses=	20521
Number of Variables=	1675
Number of Tries=	1000
Number of Solutions=	1000
Optimization Value=	8720
Solved in (secs)=	62.47
Number of missions filled=	27
Simulated Annealing Optimization Value=	8684
Simulated Annealing Solved in (secs)=	5.73
Simulated Annealing Number of missions filled=	27

Problem 3: 50 Resources \| 50 Tasks \| k=33
input formula cnf file	[CNF]
results cnf file	[CNF]
Number of Clauses=	31358
Number of Variables=	2126
Number of Tries=	500
Number of Solutions=	500
Optimization Value=	10902
Solved in (secs)=	257.95
Number of missions filled=	33
Simulated Annealing Optimization Value=	10859
Simulated Annealing Solved in (secs)=	6.281
Simulated Annealing Number of missions filled=	32

Problem 4: 30 Resources \| 30 Tasks \| k=24
input formula cnf file	[CNF]
results cnf file	[CNF]
Number of Clauses=	10200
Number of Variables=	940
Number of Tries=	1000
Number of Solutions=	1000
Optimization Value=	8352
Solved in (secs)=	46.5
Number of missions filled=	24
Simulated Annealing Optimization Value=	8319
Simulated Annealing Solved in (secs)=	3.67
Simulated Annealing Number of missions filled=	24

Problem 5: 14 Resources \| 15 Tasks \| k=7
input formula cnf file	[CNF]
results cnf file	[CNF]
Number of Clauses=	1391
Number of Variables=	258
Number of Tries=	1000
Number of Solutions=	1000
Optimization Value=	2030
Solved in (secs)=	4.166
Number of missions filled=	7
Simulated Annealing Optimization Value=	2100 (optimal value)
Simulated Annealing Solved in (secs)=	1.742
Simulated Annealing Number of missions filled=	7

Problem 6: 8 Resources \| 4 Tasks \| k=3
input formula cnf file	[CNF]
results cnf file	[CNF]
Number of Clauses=	320
Number of Variables=	65
Number of Tries=	1000
Number of Solutions=	1000
Optimization Value=	405 (optimal value)
Solved in (secs)=	1.172
Number of missions filled=	3
Simulated Annealing Optimization Value=	405 (optimal value)
Simulated Annealing Solved in (secs)=	1.222
Simulated Annealing Number of missions filled=	3

Problem 7: 100 Resources \| 100 Tasks \| k=40
input formula cnf file	[CNF]
results cnf file	[CNF]
Number of Clauses=	156828
Number of Variables=	7345
Number of Tries=	1000
Number of Solutions=	1
Optimization Value=	0
Solved in (secs)=	219.055
Number of missions filled=	0
Simulated Annealing Optimization Value=	18208
Simulated Annealing Solved in (secs)=	12038
Simulated Annealing Number of missions filled=	51