---
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

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.

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φ.


**Input QBF formula:**

**Output**:

**[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φ


**[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