3.1.7. cnfgen.families.pitfall module

Implementation of the Pitfall formula by Marc Vinyals, according to the paper [MV20].

[MV20]

Marc Vinyals. Hard examples for common variable decision heuristics. In Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI) 2020, pp. 1652–1659. https://doi.org/10.1609/aaai.v34i02.5527

PitfallFormula(v, d, ny, nz, k)

Pitfall Formula

The Pitfall formula was designed to be specifically easy for Resolution and hard for common CDCL heuristics. The formula is unsatisfiable and consists of three parts: an easy formula, a hard formula, and a pitfall misleading the solver into working with the hard part.

The hard part are several copies of an unsatisfiable Tseitin formula on a random regular graph. The pitfall part is made up of a few gadgets over (primarily) two sets of variables: pitfall variables, which point the solver towards the hard part after being assigned, and safety variables, which prevent the gadget from breaking even if a few other variables are assigned.

For more details, see the corresponding paper [1].

Parameters:

v : positive integer

number of vertices of the Tseitin graph

d : positive integer

degree of the Tseitin graph

ny : positive integer

number of pitfall variables

nz : positive integer

number of safety variables

k : positive, even integer

number of copies of the hard and pitfall parts; controls how easy the easy part is

Returns:

A CNF object

Raises:

ValueError

The is no d-regular graph when v < d or d*v are odd.

References

[1]	Marc Vinyals. Hard examples for common variable decision heuristics. In Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI) 2020, pp. 1652–1659. https://doi.org/10.1609/aaai.v34i02.5527