OFFSET
1,2
COMMENTS
LINKS
Ed Wynn, A comparison of encodings for cardinality constraints in a SAT solver, arXiv:1810.12975 [cs.LO], 2018.
EXAMPLE
For n=4, this sequence has the same value a(4)=4 as A227116 and A319158, but if we look at the three solutions to those sequences (unique up to symmetry), representing selected points by O:
O O O
O , . , . .
, . O , O . . O .
. O , . O . , O . O O .
We see that only the last of these is a solution here -- the others have rotated triangles not including any selected point (for example, as shown with commas). The last selection is therefore the unique solution (up to symmetry) for a(4)=4.
CROSSREFS
KEYWORD
nonn,more,hard
AUTHOR
Ed Wynn, Sep 12 2018
STATUS
approved