203 citations · 322 across the 18 of their papers we have counts for
4 papers · 1 filter
A framework for good SAT translations, with applications to CNF representations of XOR constraints
Matthew Gwynne, Oliver Kullmann
We present a general framework for good CNF-representations of boolean constraints, to be used for translating decision problems into SAT problems (i.e., deciding satisfiability fo…
Trading inference effort versus size in CNF Knowledge Compilation
Matthew Gwynne, Oliver Kullmann
Knowledge Compilation (KC) studies compilation of boolean functions f into some formalism F, which allows to answer all queries of a certain kind in polynomial time. Due to its rel…
Hardness measures and resolution lower bounds
Olaf Beyersdorff, Oliver Kullmann
Various "hardness" measures have been studied for resolution, providing theoretical insight into the proof complexity of resolution and its fragments, as well as explanations for t…
On SAT representations of XOR constraints
Matthew Gwynne, Oliver Kullmann
We study the representation of systems S of linear equations over the two-element field (aka xor- or parity-constraints) via conjunctive normal forms F (boolean clause-sets). First…