Antichain-based QBF Solving

Marc Ducobu
University of Mons
Friday, 11 February, 2011 - 16:00
Forum F

QBF solving can be viewed as finding a strategy in a two players game whose
game board can be exponential in the size of the formula. In this talk, we
show how to use antichains for pruning the exploration of the game board. We
show, also, that efficient exploration of the reduced game board essentially
relies on solving variants of Max-SAT and Min-SAT. Preliminary stand-alone
experiments of this algorithm and some optimizations show that the approach is
promising.