sat_aptg -- Copyright (c) 2008 Jiri Cervak, cervaj1@fel.cvut.cz

///////////////////////////////////////////////////////////////////////////////

Tento program byl vytvoren jako soucast diplomove prace:

`Automatický generátor testovacích vektorů (ATPG) založený na testu 
splnitelnosti booleovské formule'

Práce se zabývá implementací ATPG nástroje využívající řešení SAT
problému open-source řešičem. Jako řešič je použit Minisat 2.0, dále
jsou zkoumány možnosti generování neurčitých hodnot v testovacích
vektorech. Vstupem aplikace jsou soubory ve formátu ISCAS 89, výsledné
sady vektorů jsou porovnány s ATPG nástrojem Atalanta. Dále jsou
analyzovány parametry instancí SAT řešených při generování vektorů.
Nástroj může být použit jako generátor instancí SAT problémů ve
formátu DIMACS.



This program was developed as a part of Master Thesis:

`Automatic test pattern generator'

In this thesis ATPG aplication based on solving SAT problem by
open-source solver. SAT solver Minisat 2.0 is used, Ways of generating
don´t cares in test patterns are explored. Files in format ISCAS 89
are input of aplication, resulted test patterns are compared with ATPG
tool Atalanta. Parameters of SAT instances solved during ATPG are
analyzed. ATPG tool can by used as generator of SAT instances in
DIMACS format.

///////////////////////////////////////////////////////////////////////////////

Directory structure:

|-- lib				// used library and header sources
|   |-- minisat
|   `-- minisat_dc
`-- src				// sat_aptg program source codes

