Yannet Interian
Back to Codes

WalkMinQBF   

WalkMinQBF and WalkMinSAT are described in the paper: Finding small unsat cores to prove unsatisfiability of QBF's.  [abstract] Submitted

Authors: Yannet Interian and Gabriel Corvera

Quick Access: WalkMinQBF WalkMinSAT Downloads

WalkMinQBF

WalkMinQBF Module

WalkMinQBF is an incomplete algorithm that tries solve unsatisfiable two-alternation (very hard) Random QBF Formulas.  Given a two-alternation QBF formula the algorithm outputs unsat or unknown.

A two alternation QBF formula looks like :
, it is easy to check that is satisfiable.  This is an unsatisfiable  one:
 
that is, there exits assignments to x1,x2 (x1=0,x2=1) such that
for all values of y1 the formula is false.

WalkMinQBF  attempts to solve  such unsatisfiable formulas by finding assignments to the universals (x variables) such that the remaining   formula is unsat.

It is constructed by taking into consideration the statistical properties of the random QBF formulas and using three special components: A MIN SAT solver (WakMinSAT), a SAT solver and the main QBF algorithm.

WalkMinSAT Module

  WalkMinSAT, an  algorithm that given a SAT formula attempts to find an assignment that minimizes the number of satisfied clauses (MIN-SAT problem). The idea of the algorithm was is inspired by the heuristics found on WalkSAT (a state-of-the-art local search solver for MAX-SAT).  The code used as part of WalkMinQBF but can be used independently to solve MIN-SAT problems.

Downloads

 
Yannet Interian