Fetching the paper…

Reading the bibliography…

2019

Generating Difficult SAT Instances by Preventing Triangles

Escamocher, Guillaume, O'Sullivan, Barry, Prestwich, Steven David

Original
PDF
Post on X

Understand

When creating benchmarks for SAT solvers, we need SAT instances that are easy to build but hard to solve.

A recent development in the search for such methods has led to the Balanced SAT algorithm, which can create k-SAT instances with m clauses of high difficulty, for arbitrary k and m.
In this paper we introduce the No-Triangle SAT algorithm, a SAT instance generator based on the cluster coefficient graph statistic.
We empirically compare the two algorithms by fixing the arity and the number of variables, but varying the number of clauses.

Generating Difficult SAT Instances by Preventing Triangles · Around

Built on

The complexity of theorem-proving procedures
Stephen A. Cook · 1971
Earlier work this paper cites.
Reducibility among combinatorial problems
Richard M. Karp · 1972
Earlier work this paper cites.
The complexity of satisfiability problems
Thomas J. Schaefer · 1978
Earlier work this paper cites.
Where the really hard problems are
Peter C. Cheeseman, Bob Kanefsky, and William M. Taylor · 1991
Earlier work this paper cites.
Collective dynamics of ‘small-world’ networks
Original
Duncan J. Watts and Steven H. Strogatz · 1998
Earlier work this paper cites.

Similar

Formal models of heavy-tailed behavior in combinatorial search
Hubie Chen, Carla P. Gomes, and Bart Selman · 2001
Cited alongside, same era.
Threshold values of random K -sat from the cavity method
Stephan Mertens, Marc Mézard, and Riccardo Zecchina · 2006
Cited alongside, same era.
Tractable triangles
Martin C. Cooper and Stanislav Zivny · 2011
Cited alongside, same era.
The international SAT solver competitions
Matti Järvisalo, Daniel Le Berre, Olivier Roussel, and Laurent Simon · 2012
Cited alongside, same era.

Then

The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability
Donald E. Knuth · 2015
Later among the works it cites.
Weakening cardinality constraints creates harder satisfiability benchmarks
Ivor T. A. Spence · 2015
Later among the works it cites.
Balanced random SAT benchmarks
Ivor Spence · 2017
Later among the works it cites.
CaDiCaL, Lingeling, Plingeling, Treengeling and YalSAT Entering the SAT Competition 2018
Armin Biere · 2018
Later among the works it cites.

Beyond the bibliography

alphaXiv searches the wider corpus for related work and actual follow-ups.

Open on alphaXiv

alphaXiv is searching for related work…