API tools faq
paste
Guest User

sat_vmpc.c as submitted circa 2004

a guest
Aug 5th, 2021
128
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 8.58 KB | None | 0 0
raw download clone embed print report
  1. /*
  2. This C (C++ compatible) program generates a satisfiable instance
  3. of a VMPC inversion problem, expressed as a SAT problem.
  4. Public domain. Author: François Grieu.
  5.  
  6. Credits for the VMPC problem goes to Bartosz Zoltak, who
  7. proposed it in the field of cryptography, in (among other) a paper
  8. published at the conference Fast Software Encryption Conference
  9. (FSE 2004) held in Delhi, India, 5-7 Feb. 2004. See
  10. <http://www.vmpcfunction.com>
  11.  
  12. 2004-03-24 FGR Comments further polished; simplified VMPC definitions.
  13. 2004-02-24 FGR No final comment line in the output; n default to 10.
  14. 2004-02-24 FGR Range of g is checked; comments polished.
  15. 2004-02-23 FGR Created.
  16.  
  17.  
  18. Syntax of this tool:
  19.  
  20. sat_vmpc n [g [seed]]
  21.  
  22. Parameter n determines the size of the problem.
  23. The SAT problem has n*n variables, and about 5*n*n*n clauses.
  24. All clauses (except 2*n+g) have either 2 or 3 variables.
  25. The optional parameter g makes the problem easier by giving
  26. away g variables using trivial clauses, which then trivialy
  27. expand to at least n*g given variables.
  28.  
  29. Problem is written to standard output, with initial comments.
  30. To suppress hints at the solution from comments, use negative n.
  31.  
  32. Based on experiments with ZChaff 2003.11.04, difficulty rating:
  33. sat_vmpc 10 trivial
  34. sat_vmpc 21 easy
  35. sat_vmpc 22 nice
  36. sat_vmpc 23 serious ( 69 s)
  37. sat_vmpc 23 0 1 just as serious, other seed (108 s)
  38. sat_vmpc 24 challenging
  39. sat_vmpc 25 1 easy
  40. sat_vmpc 43 4 nice
  41. sat_vmpc 50 5 nice
  42. sat_vmpc 80 10 4 serious ( 80 s)
  43. sat_vmpc 80 9 4 serious (147 s)
  44.  
  45. For the purpose of SAT competition 2004, the author suggests
  46. values of n in range 5+3*g to 40+6*g, with g in range 0 to 10.
  47. The most interesting value of g is 0; many problems with g=0
  48. have several solutions; e.g.
  49. sat_vmpc 21
  50.  
  51. Note: When n is 0, a special (huge) problem is generated;
  52. there is a $100 prize for solving it!
  53. This problem is approximately as hard as for n=256, g=24,
  54. and is believed untractable. For details see
  55. <http://www.vmpcfunction.com/trial.htm>
  56.  
  57.  
  58. Definition of the VMPC inversion problem:
  59.  
  60. Let S be the set of nonnegative integers less than n.
  61. We are given a permutation Q on S, and want a permutation P with
  62. Q[x] = P[(P[P[x]]+1)%n]
  63.  
  64. An instance of the VMPC inversion problem is satisfiable if a
  65. solution P exists.
  66.  
  67. This is inherently a non-boolean satisfiability problem.
  68. The translation made here to boolean SAT is straightforward:
  69. it uses n * (n variables, one of which is set and n-1 are clear).
  70.  
  71. */
  72.  
  73.  
  74. #include <limits.h>
  75. #include <stdlib.h>
  76. #include <stdio.h>
  77.  
  78.  
  79. /*
  80. find an at-least-32 bits type u32
  81. how to describe it to printf P32
  82. and mean to keep the low 32 bits L32()
  83. */
  84. #if UINT_MAX==0xFFFFFFFF
  85. typedef unsigned u32;
  86. #define P32
  87. #define L32(x) ((u32)(x))
  88. #else
  89. typedef unsigned long u32;
  90. #define P32 "l"
  91. #if ULONG_MAX==0xFFFFFFFF
  92. #define L32(x) ((u32)(x))
  93. #else
  94. #define L32(x) ((u32)(x)&0xFFFFFFFF)
  95. #endif
  96. #endif
  97.  
  98. /*{ PRNG; fast, fully portable across machines, period of any bit at least 2^49-2^17, not crypto-quality */
  99.  
  100. /* return an about uniformly distributed u32 */
  101. #define u32RNG() ((RNGA=L32((RNGA+1u)*0xA85ADDCDu)),(RNGB=(RNGB>>1)^(((RNGB|0xFFFFFFFEu)+1u)&0xD7626A57u))+(RNGA^(RNGA>>16)))
  102.  
  103. /* for extra speed, a local rng context can be declared */
  104. #define u32RNGcontext u32 RNGA=0, RNGB=0
  105.  
  106. /* else by default a global rng context is used */
  107. static u32RNGcontext;
  108.  
  109. /* seed the RNG (optional) */
  110. #define SRNG(x) do RNGB=(RNGA=L32(x))&0x7FFFFFFFu; while(0)
  111. /*}*/
  112.  
  113.  
  114. /* type we use for most things, and how to describe it to printf */
  115. typedef int tNum;
  116. #define PNum "%4u"
  117.  
  118. /* return a pseudorandom permutation on range [0..n-1] */
  119. void randperm(tNum P[],tNum n)
  120. {
  121. tNum j,g;
  122. for(j=0;j<n;++j)
  123. {
  124. g = u32RNG()%(j+1); /* not perfectly evenly distributed, but good enough */
  125. P[j] = P[g];
  126. P[g] = j;
  127. }
  128. }
  129.  
  130. #define nmax 300
  131. #define ncha 256 /* size of the challenge */
  132.  
  133. tNum P[nmax],Q[nmax],QC[ncha]={
  134. 61, 71, 49, 62, 52, 185, 214, 89, 156, 120, 240, 139, 172, 184, 43, 168,
  135. 74, 8, 132, 151, 83, 186, 159, 229, 23, 175, 112, 142, 75, 232, 204, 123,
  136. 12, 59, 73, 64, 225, 14, 161, 198, 68, 69, 92, 226, 63, 32, 87, 150, 178,
  137. 118, 245, 196, 45, 116, 255, 18, 46, 102, 179, 13, 136, 252, 154, 35, 70,
  138. 53, 169, 242, 72, 194, 10, 42, 19, 209, 121, 140, 86, 124, 80, 201, 137,
  139. 109, 114, 88, 106, 205, 11, 234, 157, 247, 129, 153, 28, 31, 238, 122, 202,
  140. 22, 103, 171, 37, 119, 166, 212, 182, 17, 91, 30, 216, 93, 101, 104, 0, 78,
  141. 141, 95, 107, 195, 1, 66, 41, 217, 237, 199, 165, 56, 143, 127, 100, 76,
  142. 117, 131, 193, 253, 167, 223, 38, 227, 113, 97, 206, 228, 130, 181, 221,
  143. 84, 236, 6, 211, 55, 33, 110, 177, 29, 27, 145, 96, 219, 249, 230, 40, 174,
  144. 105, 138, 85, 36, 243, 218, 9, 25, 4, 244, 250, 158, 149, 208, 188, 94,
  145. 146, 207, 111, 224, 203, 213, 125, 191, 7, 215, 200, 47, 148, 170, 26, 24,
  146. 34, 54, 57, 233, 192, 173, 44, 126, 98, 197, 3, 144, 128, 99, 134, 2, 58,
  147. 65, 133, 248, 241, 160, 152, 67, 164, 220, 183, 51, 239, 222, 189, 135,
  148. 155, 82, 210, 246, 187, 79, 190, 176, 81, 162, 39, 60, 50, 77, 254, 15,
  149. 180, 147, 251, 231, 16, 163, 90, 108, 48, 20, 115, 5, 21, 235
  150. };
  151.  
  152. int main(int argc, char *argv[])
  153. {
  154. /* return the n-th argument with default value */
  155. #define arg(x,d) ((tNum)(((x)<argc&&argv[x]!=0&&*argv[x]!=0)?atol(argv[x]):(d)))
  156.  
  157. tNum n,j,k,l,c,g;
  158. u32 s;
  159. char chal = 0; /* 1 for the challenge */
  160. char verb = 1; /* 1 for full comments */
  161.  
  162. /* get parameters */
  163. n = arg(1,10);
  164. g = arg(2,0);
  165. s = arg(3,0);
  166.  
  167. /* establish the VMPC problem */
  168. if (n<0)
  169. {
  170. n = -n;
  171. verb = 0;
  172. }
  173.  
  174. if (n==0)
  175. {
  176. chal = 1;
  177. n = ncha;
  178. for(j=0;j<n;++j) P[j]=n;
  179. P[228]=86; P[86]=12; P[87]=35; P[240]=85; P[229]=137; P[252]=133; P[197]
  180. =187; P[129]=108; P[236]=80; P[156]=231; P[141]=152; P[158]=89; P[111]=97;
  181. P[29]=190; P[192]=236; P[232]=91; P[152]=62; P[248]=153; P[189]=45; P[182]
  182. =165; P[205]=25; P[119]=132; P[62]=130; P[7]=49; P[148]=181; P[42]=44; P
  183. [115]=16; P[167]=131; P[214]=158;
  184. s = g = 0;
  185. for(j=0;j<n;++j) g += P[j]!=n;
  186. }
  187. else
  188. {
  189. SRNG(s); /* seed the RNG */
  190. if (n>nmax) n = nmax;
  191. randperm(P,n);
  192. for(j=n;j--;)
  193. Q[j] = P[(P[P[j]]+1)%n];
  194. }
  195.  
  196. if (g<0) g = 0;
  197. if (g>n) g = n;
  198.  
  199. #define VP(a,b) ((a)*n+(b)+1) // variable true when P(a)==b
  200.  
  201. /* initial comments */
  202. printf("c VMPC problem of size %u translated to SAT; %u entries revealed",n,g);
  203. if (verb)
  204. printf("; random seed %lu",s);
  205. printf("\nc "); for(j=0;j<n;++j) printf(PNum,j);
  206. if (verb || chal)
  207. {
  208. printf("\nc P "); for(j=0;j<n;++j) printf((chal&&P[j]==n)?" ? ":PNum,P[j]);
  209. }
  210. printf("\nc Q "); for(j=0;j<n;++j) printf(PNum,Q[j]);
  211. if (chal)
  212. printf("\nc Problem reportedly SAT, with $100 prize; see <http://www.vmpcfunction.com/trial.htm>");
  213. else
  214. {
  215. if (verb)
  216. {
  217. printf("\nc Problem is known SAT when true variables are:\nc");
  218. for(j=0;j<n;++j) printf(" %d",VP(j,P[j]));
  219. }
  220. }
  221.  
  222. #define IMP2(X,Y) do if ((X)!=(Y)) printf("%d %d 0\n",-(X),(Y)); while(0) // clause for X => Y
  223. #define ANDIMP1(X,Y,Z) do if ((X)!=(Z) && (Y)!=(Z)) ++c; while(0) // clause for X&Y => Z
  224. #define ANDIMP2(X,Y,Z) do if ((X)!=(Z) && (Y)!=(Z)) if (X==Y) printf("%d %d 0\n",-(X),(Z)); else printf("%d %d %d 0\n",-(X),-(Y),(Z)); while(0) // clause for X&Y => Z
  225.  
  226. /* precompute the number of clauses, which vary slightly */
  227. c = (n+n*n*(n-1))*2+g;
  228. for(j=0;j<n;++j)
  229. for(k=0;k<n;++k)
  230. for(l=0;l<n;++l)
  231. {
  232. ANDIMP1(VP(j,k),VP(k,l),VP((l+1)%n,Q[j]));
  233. ANDIMP1(VP(k,l),VP((l+1)%n,Q[j]),VP(j,k));
  234. ANDIMP1(VP((l+1)%n,Q[j]),VP(j,k),VP(k,l));
  235. }
  236. printf("\np cnf %d %d\n",n*n,c);
  237.  
  238. /* giveaway variables */
  239. if (chal)
  240. {
  241. for(j=0;j<n;++j)
  242. if (P[j]!=n)
  243. printf("%d 0\n",VP(j,P[j]));
  244. }
  245. else
  246. for(j=0;j<g;++j)
  247. printf("%d 0\n",VP(j,P[j]));
  248.  
  249. /* "at least one per row" clauses */
  250. for(j=0;j<n;++j)
  251. {
  252. for(k=0;k<n;++k)
  253. printf("%d ",VP(j,k));
  254. printf("0\n");
  255. }
  256.  
  257. /* "at least one per column" clauses */
  258. for(k=0;k<n;++k)
  259. {
  260. for(j=0;j<n;++j)
  261. printf("%d ",VP(j,k));
  262. printf("0\n");
  263. }
  264.  
  265. for(j=0;j<n;++j)
  266. for(k=0;k<n;++k)
  267. for(l=0;l<n;++l)
  268. {
  269. if (l!=k)
  270. IMP2(VP(j,k),-VP(j,l)); /* "at most one per row" clauses */
  271. if (l!=j)
  272. IMP2(VP(j,k),-VP(l,k)); /* "at most one per column" clauses */
  273. ANDIMP2(VP(j,k),VP(k,l),VP((l+1)%n,Q[j])); /* VMPC discovery rule 1 */
  274. ANDIMP2(VP(k,l),VP((l+1)%n,Q[j]),VP(j,k)); /* VMPC discovery rule 2 */
  275. ANDIMP2(VP((l+1)%n,Q[j]),VP(j,k),VP(k,l)); /* VMPC discovery rule 3 */
  276. }
  277. return 0;
  278. }
  279.  
Advertisement
Add Comment
Please, Sign In to add comment
Public Pastes
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!