Weakening Cardinality Constraints Creates Harder Satisfiability Benchmarks


Autoria(s): Spence, Ivor
Data(s)

01/05/2015

Resumo

For some time, the satisfiability formulae that have been the most difficult to solve for their size have been crafted to be unsatisfiable by the use of cardinality constraints. Recent solvers have introduced explicit checking of such constraints, rendering previously difficult formulae trivial to solve. A family of unsatisfiable formulae is described that is derived from the sgen4 family but cannot be solved using cardinality constraints detection and reasoning alone. These formulae were found to be the most difficult during the SAT2014 competition by a significant margin and include the shortest unsolved benchmark in the competition, sgen6-1200-5-1.cnf.

Formato

application/pdf

Identificador

http://pure.qub.ac.uk/portal/en/publications/weakening-cardinality-constraints-creates-harder-satisfiability-benchmarks(c2770eca-1199-4f04-aaa4-d677c3acc058).html

http://dx.doi.org/10.1145/2746239

http://pure.qub.ac.uk/ws/files/14448749/spence2014_v3.pdf

Idioma(s)

eng

Direitos

info:eu-repo/semantics/openAccess

Fonte

Spence , I 2015 , ' Weakening Cardinality Constraints Creates Harder Satisfiability Benchmarks ' ACM Journal of Experimental Algorithmics , vol 20 , 1.4 . DOI: 10.1145/2746239

Palavras-Chave #SAT-solvers, Small Hard Benchmarks
Tipo

article