3 papers
cs.LO2016
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
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
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…