Stem qbf$ (all stems)

48 papers:

ICALP-v1-2015-BeyersdorffCMS #calculus

Feasible Interpolation for QBF Resolution Calculi (OB, LC, MM, AS), pp. 180–192.

SAT-2015-TuHJ #learning #named #reasoning #satisfiability

QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving (KHT, TCH, JHRJ), pp. 343–359.

IJCAR-2014-HeuleSB #preprocessor #proving

A Unified Proof System for QBF Preprocessing (MH, MS, AB), pp. 91–106.

IJCAR-2014-Zhang #encoding #verification

QBF Encoding of Temporal Properties and QBF-Based Verification (WZ), pp. 224–239.

SAT-2014-BalabanovWJ #proving

QBF Resolution Systems and Their Proof Complexities (VB, MW, JHRJ), pp. 154–169.

SAT-2014-HeymanSMLA #using

Dominant Controllability Check Using QBF-Solver and Netlist Optimizer (TH, DS, YM, LL, HAH), pp. 227–242.

SAT-2014-JordanKLS #named #parallel #towards

MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing (CJ, LK, FL, MS), pp. 430–437.

DATE-2013-GoultiaevaSB

Bridging the gap between dual propagation and CNF-based QBF solving (AG, MS, AB), pp. 811–814.

DATE-2013-HillebrechtKEWB #generative

Accurate QBF-based test pattern generation in presence of unknown values (SH, MAK, DE, HJW, BB), pp. 436–441.

SAT-2013-GoultiaevaB

Recovering and Utilizing Partial Duality in QBF (AG, FB), pp. 83–99.

SAT-2013-JanotaM #on the

On Propositional QBF Expansions and Q-Resolution (MJ, JMS), pp. 67–82.

SAT-2013-LonsingEG #learning #performance #pseudo #quantifier

Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation (FL, UE, AVG), pp. 100–115.

DATE-2012-MarinMLB #design #incremental #using #verification

Verification of partial designs using incremental QBF solving (PM, CM, MDTL, BB), pp. 623–628.

SAT-2012-BaylessH #algorithm

Single-Solver Algorithms for 2QBF — (Poster Presentation) (SB, AJH), pp. 487–488.

SAT-2012-JanotaKMC #refinement

Solving QBF with Counterexample Guided Refinement (MJ, WK, JMS, EMC), pp. 114–128.

SAT-2012-MarinMB #design #incremental #preprocessor #verification

Incremental QBF Preprocessing for Partial Design Verification — (Poster Presentation) (PM, CM, BB), pp. 473–474.

SAT-2012-NiemetzPLSB

Resolution-Based Certificate Extraction for QBF — (Tool Presentation) (AN, MP, FL, MS, AB), pp. 430–435.

DATE-2011-ReimerPSB #integration #orthogonal

Integration of orthogonal QBF solving techniques (SR, FP, CS, BB), pp. 149–154.

CADE-2011-BiereLS

Blocked Clause Elimination for QBF (AB, FL, MS), pp. 101–115.

CAV-2011-BalabanovJ #evaluation #proving

Resolution Proofs and Skolem Functions in QBF Evaluation and Applications (VB, JHRJ), pp. 149–164.

SAT-2011-JanotaS #algorithm

Abstraction-Based Algorithm for 2QBF (MJ, JPMS), pp. 230–244.

SAT-2011-LonsingB #detection

Failed Literal Detection for QBF (FL, AB), pp. 259–272.

DAC-2010-PigorschS #preprocessor #satisfiability #using

An AIG-Based QBF-solver using SAT for preprocessing (FP, CS), pp. 170–175.

DATE-2010-MangassarianLGVB #preprocessor

Leveraging dominators for preprocessing QBF (HM, BL, AG, AGV, FB), pp. 1695–1700.

SAT-2010-BrummayerLB #automation #debugging #satisfiability #testing

Automated Testing and Debugging of SAT and QBF Solvers (RB, FL, AB), pp. 44–57.

SAT-2010-GoultiaevaB

Exploiting Circuit Representations in QBF Solving (AG, FB), pp. 333–339.

SAT-2010-KlieberSGC #learning

A Non-prenex, Non-clausal QBF Solver with Game-State Learning (WK, SS, SG, EMC), pp. 128–142.

SAT-2010-LonsingB #dependence #search-based

Integrating Dependency Schemes in Search-Based QBF Solvers (FL, AB), pp. 158–171.

SAT-2010-PeschieraPTBKL #evaluation

The Seventh QBF Solvers Evaluation (QBFEVAL’10) (CP, LP, AT, UB, OK, IL), pp. 237–250.

DATE-2009-PigorschS

Exploiting structure in an AIG based QBF solver (FP, CS), pp. 1596–1601.

SAT-2009-GoultiaevaIB

Beyond CNF: A Circuit-Based QBF Solver (AG, VI, FB), pp. 412–426.

SAT-2009-LewisMSNBG #distributed #named

PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing (MDTL, PM, TS, MN, BB, EG), pp. 509–523.

SAT-2008-LonsingB #named

Nenofex: Expanding NNF for QBF Solving (FL, AB), pp. 196–210.

SAT-2007-BubeckB #bound #preprocessor

Bounded Universal Expansion for Preprocessing QBF (UB, HKB), pp. 244–257.

SAT-2007-JussilaBSKW #proving #towards

A First Step Towards a Unified Proof Checker for QBF (TJ, AB, CS, DK, CMW), pp. 201–214.

SAT-2007-SamulowitzB #clustering

Dynamically Partitioning for Solving QBF (HS, FB), pp. 215–229.

SAT-2007-StaberB #fault #locality

Fault Localization and Correction with QBF (SS, RB), pp. 355–368.

SAT-2006-SabharwalAGHS #modelling #performance #symmetry

QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency (AS, CA, CPG, JWH, BS), pp. 382–395.

SAT-2006-SamulowitzB #reasoning

Binary Clause Reasoning in QBF (HS, FB), pp. 353–367.

SAT-J-2004-BerreNST05 #comparative #evaluation

The Second QBF Solvers Comparative Evaluation (DLB, MN, LS, AT), pp. 376–392.

SAT-J-2004-GiunchigliaNT05 #reasoning

QBF Reasoning on Real-World Instances (EG, MN, AT), pp. 105–121.

SAT-2005-DershowitzHK #bound #model checking

Bounded Model Checking with QBF (ND, ZH, JK), pp. 408–414.

SAT-2005-GentR #learning

Local and Global Complete Solution Learning Methods for QBF (IPG, AGDR), pp. 91–106.

SAT-2004-GiunchigliaNT #reasoning

QBF Reasoning on Real-World Instances (EG, MN, AT), pp. 247–254.

SAT-2003-BerreST #challenge #evaluation #satisfiability

Challenges in the QBF Arena: the SAT’03 Evaluation of QBF Solvers (DLB, LS, AT), pp. 468–485.

SAT-2003-GentGNRT #data type

Watched Data Structures for QBF Solvers (IPG, EG, MN, AGDR, AT), pp. 25–36.

SAT-2003-MneimnehS #graph #scalability

Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution (MNM, KAS), pp. 411–425.

KR-2002-DoniniLMS

Solving QBF by SMV (FMD, PL, FM, MS), pp. 578–592.