47 citations · 188 across the 18 of their papers we have counts for
Showing 2016Show all
3 papers · 1 filter
cs.LO2016★ 17 cited
Q-Resolution with Generalized Axioms
Florian Lonsing, Uwe Egly, Martina Seidl
Q-resolution is a proof system for quantified Boolean formulas (QBFs) in prenex conjunctive normal form (PCNF) which underlies search-based QBF solvers with clause and cube learnin…
cs.LO2016★ 4 cited
Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications
Roderick Bloem, Uwe Egly, Patrick Klampfl +3
Existing approaches to synthesize reactive systems from declarative specifications mostly rely on Binary Decision Diagrams (BDDs), inheriting their scalability issues. We present n…
cs.LO2016★ 8 cited
HordeQBF: A Modular and Massively Parallel QBF Solver
Tomas Balyo, Florian Lonsing
The recently developed massively parallel satisfiability (SAT) solver HordeSAT was designed in a modular way to allow the integration of any sequential CDCL-based SAT solver in its…