How to read output files

How to read output files

*-results.txt

#Satisfiable. Variable values from HSS route
#Mon Nov 15 10:14:25 MSK 2010
ImplementationVersion=1.0.3
InitialFormulaLoadTime=38
InitialFormulaVarCount=8
InitialFormulaClausesCount=44
CTFCreationTime=10
CTFCount=5
CTSCreationTime=5
CTSUnificationTime=13
BasicCTSInitialClausesCount=11
BasicCTSFinalClausesCount=11
HSSCreationTime=62
NumberOfHSSTiersBuilt=6
SearchHSSRouteTime=3
1=true
2=false
3=true
4=true
5=true
6=true
7=false
8=false

Note: File contents were reformatted for better reading.

*-results.txt file contains 4 types of information:

1. Result of formula classification: Satisfiable or Unsatisfiable
2. ImplementationVersion is version number of solver that solved this formula
3. Measurements of calculation process: contains timing information about major algorithm stages (see diagram below) and some additional information about number of constructed CTF, number of HSS tiers built, etc. To understand these values, please read Romanov's paper.
4. If result of formula classification was "Satisfiable" then this file contains pairs of values that forms satisfying set for the formula: <n>=<boolean> where <n> is a variable name, and the <boolean> is its value

Major algorithm stages

*-hss-0.png

This file contains visual representation of basic graph. Red colored path represents HS route which is joint satisfying set for the formula.

Green or blue color of triplet values and rounded rectangles are debug information. See source code for details.