MARCO GSRC Calibrating Achievable Design: Bookshelf

GRASP - SAT Solver

	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

I. Introduction

The GRASP algorithm is among the best known methods of solving the problem of Propositional Satisfiability (SAT). Developed by Joao Paulo Marques Silva as part of his doctoral dissertation at the University of Michigan, the algorithm has been successfully applied to problems in the field of Electronic CAD, such as automatic test pattern generation (ATPG), timing analysis, delay fault testing, logic verification, and Path Sensitization.

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.

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.

The GRASP engine reads input in DIMACS format. The following is an example of a data file in DIMACS format:

   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.

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:

  - UCSC benchmarks
  - DIMACS challenge benchmarks

For the table of results the following definitions apply:

  #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

IV. Executables

nsat (Solaris/Sparc) (Intel Linux): Returns "Satisfiable" with a valid truth assignment if problem is satisfiable, or "Unsatisfiable" if the problem is unsatisfiable. nsat help - for usage.

V. Common in-memory representations, parsers and other source codes

cnf2sat.c

Converts from the DIMACS standard .cnf format to the .sat format
sat2cnf.c

Converts a conjunctive normal form formula in DIMACS standard .sat format to .cnf format

Maintained by faloul@umich.edu
Last updated Sun Dec 5 1999

Benchmark Class	#M	GRASP		TEGUS		POSIT
Benchmark Class	#M	#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

MARCO GSRC Calibrating Achievable Design: Bookshelf

GRASP - SAT Solver

Contents