DepQBF: A Dependency-Aware QBF Solver | Zendy

Florian Lonsing | Zendy; Armin Biere | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

DepQBF: A Dependency-Aware QBF Solver

Author(s) -

Florian Lonsing,

Armin Biere

Publication year - 2010

Publication title -

journal on satisfiability boolean modeling and computation

Language(s) - English

Resource type - Journals

eISSN - 1875-5011

pISSN - 1574-0617

DOI - 10.3233/sat190077

Subject(s) - solver , dependency (uml) , prefix , conjunctive normal form , computer science , true quantified boolean formula , boolean satisfiability problem , ranking (information retrieval) , theoretical computer science , algorithm , mathematics , artificial intelligence , programming language , philosophy , linguistics

We present DepQBF 0.1, a new search-based solver for quantified boolean formulae (QBF). It integrates compact dependency graphs to overcome the restrictions imposed by linear quantifier prefixes of QBFs in prenex conjunctive normal form (PCNF). DepQBF 0.1 was placed first in the main track of QBFEVAL’10 in a score-based ranking. We provide a general system overview and describe selected orthogonal features such as restarts and removal of learnt constraints.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research