12 citations · 38 across the 5 of their papers we have counts for
5 papers
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…
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…
Towards a theory of good SAT representations
Matthew Gwynne, Oliver Kullmann
We aim at providing a foundation of a theory of "good" SAT representations F of boolean functions f. We argue that the hierarchy UC_k of unit-refutation complete clause-sets of lev…
Generalising unit-refutation completeness and SLUR via nested input resolution
Matthew Gwynne, Oliver Kullmann
We introduce two hierarchies of clause-sets, SLUR_k and UC_k, based on the classes SLUR (Single Lookahead Unit Refutation), introduced in 1995, and UC (Unit refutation Complete), i…