3 citations · 6 across the 9 of their papers we have counts for
Showing 2010Show all
3 papers · 1 filter
cs.AI2010★ 3 cited
On the CNF encoding of cardinality constraints and beyond
Olivier Bailleux
In this report, we propose a quick survey of the currently known techniques for encoding a Boolean cardinality constraint into a CNF formula, and we discuss about the relevance of…
cs.NE2010
Evolving difficult SAT instances thanks to local search
Olivier Bailleux
We propose to use local search algorithms to produce SAT instances which are harder to solve than randomly generated k-CNF formulae. The first results, obtained with rudimentary se…
cs.LO2010
Reified unit resolution and the failed literal rule
Olivier Bailleux
Unit resolution can simplify a CNF formula or detect an inconsistency by repeatedly assign the variables occurring in unit clauses. Given any CNF formula sigma, we show that there…