|
|
Fadi A. Aloul and Karem A. Sakallah |
| I. | Introduction | |
| II. | Data Formats | |
| III. | Publicly available instances, solutions and reference performance results | |
| IV. | Executables | |
| V. | Common in-memory representations, parsers and other source codes |
GRASP is premised on the inevitability of conflicts during search and its most distinguishing feature is the augmentation of basic backtracking search with a powerful conflict analysis procedure. Analyzing conflicts to determine their causes enables GRASP to backtrack non-chronologically to earlier levels in the search tree, potentially pruning large portions of the search space. In addition, by "recording' the causes of conflicts, GRASP can recognize and preempt the occurrence of similar conflicts later in the search. Finally, straightforward bookkeeping of the causality chains leading up to conflicts allows GRASP to identify assignments that are necessary for a solution to be found.
Experimental results obtained from a large number of benchmarks, including many
from the field of test pattern generation, indicate that application of the
proposed conflict analysis techniques to SAT algorithms can be extremely effective
for a large number of representative classes of SAT instances.
The GRASP engine reads input in DIMACS format. The following is an example of a data file in DIMACS format:
All programs were compiled with GCC 2.7.2 and run on SUN SPARC 5/85 machine with
64
MByte of RAM.
Two set of benchmarks were tested:
For the table of results the following definitions apply:
II. Data Formats
The common data format for GRASP is conjunctive normal form (CNF). A CNF formula f
on n binary variables x1,..., xn is the conjunction (AND) of m clauses w1,...,wm
each of which is the disjunction (OR) of one or more literals, where a literal is
the occurrence of a variable or its complement. A formula f denotes a unique
n-variable Boolean function f(x1,...,xn) and each of its clauses corresponds to an
implicate f.
c Example SAT format file in DIMACS format
c It contains a formula in cnf formulation.
c
c
p cnf 4 3
2 3 -4 0
-4 0
2 3 4 0
A line starting with 'c' indicates a comment. The line represented as 'p cnf #var #cl' indicates the number of variables and
clauses in the CNF formula. A single number '0' at the end of the line identifies the end of the clause.
III. Publicly available instances, solutions and reference performance
results
GRASP is experimented with several benchmarks. It is compared with other
state-of-the-art and publicly available SAT programs. In particular, GRASP is
compared with TEGUS (available at University of California at Berkeley) and POSIT (available at University of Pennsylvania). TEGUS is included in SIS. It was adapted to read
CNF formulas and augmented to continue searching when all its default options are
exhausted. No changes were required with POSIT.
- UCSC benchmarks
- DIMACS challenge benchmarks
#M : the total number of class members
#S : the number of class members for which program terminated in less than 10,000 CPU seocnds.
TIME : total CPU time, in seconds, taken to process all members of the class.
UCSC Benchmarks
|
Benchmark Class |
#M |
GRASP |
TEGUS |
POSIT |
|||
|
#S |
Time |
#S |
Time |
#S |
Time |
||
|
BF-0432 |
21 |
21 |
47.6 |
19 |
53,852 |
21 |
55.8 |
|
BF-1355 |
149 |
149 |
125.7 |
53 |
993,915 |
64 |
946,127 |
|
BF-2670 |
53 |
53 |
68.3 |
25 |
295,410 |
53 |
2971 |
|
SSA-0432 |
7 |
7 |
1.1 |
7 |
1593 |
7 |
0.2 |
|
SSA-2670 |
12 |
12 |
51.5 |
0 |
120,000 |
12 |
2,826 |
|
SSA-6288 |
3 |
3 |
.2 |
3 |
17.5 |
3 |
0.0 |
|
SSA-7552 |
80 |
80 |
19.8 |
80 |
3,406 |
80 |
60 |
DIMACS Challenge Benchmarks
|
Benchmark Class |
#M |
GRASP |
TEGUS |
POSIT |
|||
|
#S |
Time |
#S |
Time |
#S |
Time |
||
|
AIM-100 |
24 |
24 |
1.8 |
24 |
107.9 |
24 |
1,290 |
|
AIM-200 |
24 |
24 |
10.8 |
23 |
14,059 |
13 |
117,991 |
|
BF |
4 |
4 |
7.2 |
2 |
26,654 |
2 |
20,037 |
|
DUBOIS |
13 |
13 |
34.4 |
5 |
90,333 |
7 |
77,189 |
|
II-32 |
17 |
17 |
7.0 |
17 |
1,231 |
17 |
650.1 |
|
PRET |
8 |
8 |
18.2 |
4 |
42,579 |
4 |
40,691 |
|
SSA |
8 |
8 |
6.5 |
6 |
20,230 |
8 |
85.3 |
|
AIM-50 |
24 |
24 |
0.4 |
24 |
2.2 |
24 |
0.4 |
|
II-8 |
14 |
14 |
23.4 |
14 |
11.8 |
14 |
2.3 |
|
JNH |
50 |
50 |
21.3 |
50 |
6,055 |
50 |
0.8 |
|
PAR-8 |
10 |
10 |
0.4 |
10 |
1.5 |
10 |
0.1 |
|
PAR-16 |
10 |
10 |
9,844 |
10 |
9,983 |
10 |
72.1 |
|
II-16 |
10 |
9 |
10,311 |
10 |
269.6 |
9 |
10,120 |
|
H |
7 |
5 |
27,184 |
4 |
32,942 |
6 |
11,540 |
|
F |
3 |
0 |
30,000 |
0 |
30,000 |
0 |
30,000 |
|
G |
4 |
0 |
40,000 |
0 |
40,000 |
0 |
40,000 |
|
PAR-32 |
10 |
0 |
100,000 |
0 |
100,000 |
0 |
100,000 |