## Chart: Verification Performance Comparison
### Overview
The image presents two line charts comparing the performance of different verification methods on SAT (Satisfiable) and UNSAT (Unsatisfiable) properties. The charts display the percentage of properties verified against computation time in seconds. Each line represents a different verification method.
### Components/Axes
**Both Charts Share the Following:**
* **Y-axis:** "% of properties verified", ranging from 0 to 100. Increments are shown at 20, 40, 60, 80, and 100.
* **X-axis:** "Computation time (in s)", ranging from 0 to 6000. Increments are shown at 0, 2000, 4000, and 6000.
* **Legend:** Located on the right side of each chart, listing the verification methods:
* BaBSB (Blue)
* BaB (Orange)
* reluBaB (Green)
* reluplex (Red)
* MIPplanet (Purple)
* planet (Brown)
* BlackBox (Pink)
* A dashed horizontal line is present at the 100% mark.
**Chart (a): On SAT properties**
* Title: "(a) On SAT properties"
**Chart (b): On UNSAT properties**
* Title: "(b) On UNSAT properties"
### Detailed Analysis
**Chart (a): On SAT properties**
* **BaBSB (Blue):** Quickly reaches approximately 92% verified within the first few seconds and remains constant.
* **BaB (Orange):** Starts at 0%, quickly rises to approximately 92% verified within the first few seconds, and remains constant.
* **reluBaB (Green):** Starts at 0%, quickly rises to approximately 92% verified within the first few seconds, and remains constant.
* **reluplex (Red):** Increases in a step-wise fashion, reaching approximately 82% verified at 6000 seconds.
* **MIPplanet (Purple):** Remains constant at approximately 5% verified.
* **planet (Brown):** Remains constant at 0% verified.
* **BlackBox (Pink):** Remains constant at approximately 2% verified.
**Chart (b): On UNSAT properties**
* **BaBSB (Blue):** Increases rapidly to approximately 95% verified by 2000 seconds, then continues to increase slowly to approximately 99% verified by 6000 seconds.
* **BaB (Orange):** Increases to approximately 70% verified by 6000 seconds.
* **reluBaB (Green):** Increases to approximately 78% verified by 6000 seconds.
* **reluplex (Red):** Increases to approximately 60% verified by 6000 seconds.
* **MIPplanet (Purple):** Remains constant at approximately 55% verified.
* **planet (Brown):** Increases to approximately 55% verified by 6000 seconds.
* **BlackBox (Pink):** Increases slowly to approximately 15% verified by 6000 seconds.
### Key Observations
* On SAT properties, BaBSB, BaB, and reluBaB perform similarly and achieve high verification rates quickly.
* On UNSAT properties, BaBSB outperforms the other methods, achieving the highest verification rate.
* reluplex shows a gradual increase in verification rate for both SAT and UNSAT properties.
* MIPplanet, planet, and BlackBox generally have lower verification rates compared to the other methods.
### Interpretation
The charts illustrate the performance of different verification methods on SAT and UNSAT properties. The results suggest that BaBSB, BaB, and reluBaB are highly effective for SAT properties, achieving high verification rates quickly. However, on UNSAT properties, BaBSB demonstrates superior performance compared to the other methods. The gradual increase in verification rate for reluplex indicates a different approach or optimization strategy. The lower verification rates of MIPplanet, planet, and BlackBox suggest that these methods may be less suitable for the given properties or require further optimization. The difference in performance between SAT and UNSAT properties highlights the challenges in verifying different types of logical statements.
