---
# System prepended metadata

title: QBF Solver
tags: [GV]

---

---
tags: GV
---

# QBF Solver

## Introduction

**QBF (Quantified Boolean Formula)** is a generalization to Boolean formula which consists of quantifier (universal ∀ or existential ∃) and PCNF (prenex conjunctive normal form). QBF formula can be expressed by Q1x1 Q2x2...Qnxn φ(x1, x2,...,xn).

Two-QBF formula means that contains one universal quantifier and one existential quantifier. The following content will denote X (x1, x2..., xn) as the variables in the universal quantifier scope, and Y (y1, y2..., ym) as the variables in the existential quantifier scope. 

**∀X∃Yφ = ∀x1x2...xn∃y1y2...ymφ**    ...(1)

* **Observe answer:** the X assignments that prove QBF formula **false** by finding an X assignments causing CNF φ UNSAT. 
* **Reverse answer:** the X assignments that can find at least one Y assignments causing CNF φ SAT. If all X assignments are proved to be reverse answer, the QBF formula is **true**. 

## Cegar-based QBF Solver

Counterexample-guided abstraction refinement (Cegar) iteratively finds solutions and refines the abstraction. And this method is composed of three operations: 
1. Find the solution to the abstraction
2. Find a new counterexample for this new solution
3. Refine the abstraction by the counterexample
![](https://imgur.com/28MSQyh.png)

All of the above steps can be implemented by SAT solving process
1. Solve the formula depending on only X variables in (1)
2. Add the clauses to the original CNF

RAReQS and QESTO are basically builded by this Cegar method.


## Two-QBF Solver

Their solver is composed of three solver **S**, **S_copy**, **A_S**.
* **S**: Contains CNF part φ originally and grew by adding the inverse clauses
* **S_copy** : Enable us to solve original problem without changing activity information in S (block clauses are also added here)
* **A_S** : Add blocking clauses to record the solved X assignments

### Reverse Answer
To check whether every X assignment is reverse answer, the most intuitive method is to make solver satifies all X assignment. We need to block the solved X assignments by adding their inverse clauses to the formula.
![](https://imgur.com/vGtAyBW.png)

There are two types of generalization.
* **Normal generalization**
* **Multiplexer circuit generalization**

### Observe Answer
To find a X assignment makes unsatisfiable, they observe four types of observe answer candidates (**implication/conflict/learnt clause/learnt implication**) and capture them.


## ABC command
```
qbf [-PI num] [-dvh]

-P num : number of parameters p (should be the first PIs)
-I num : quit after the given iteration even if unsolved
```
### Solve the QBF formula ∃P∀Xφ.

![](https://imgur.com/FeZb2R5.png)

**Input QBF formula:**
![](https://imgur.com/0iE4f8j.png)

**Output**:
![](https://imgur.com/G4lnMkj.png)

**[Prove]** 
f(x, y, z, w, u, v) = (xu+w)'+(x+y+uv)(z+w'y)
when (x=1, y=0, z=1) f = (u+w)'+1 = 1

### Solve the QBF formula ∀P∃Xφ

![](https://imgur.com/JK25rgG.png)

**[Prove]** 
f(x, y, z, w, u, v) = (xu+w)'+(x+y+uv)(z+w'y)
when (x=0, y=0, z=0, w=1) f = (1)'+(uv)(0) = 0
CounterExample = 0001

## Next Sprint Plan
1. Just use the ABC command to solve the current QBF problem.
2. Combine An-wei學姊's work into GV (use MiniSAT).


## Reference
https://hdl.handle.net/11296/svsq7z
