diff options
Diffstat (limited to 'sample/trick2015')
21 files changed, 874 insertions, 0 deletions
diff --git a/sample/trick2015/README.md b/sample/trick2015/README.md new file mode 100644 index 0000000000..6cae824796 --- /dev/null +++ b/sample/trick2015/README.md @@ -0,0 +1,16 @@ +This directory contains the award-winning entries of +the 2nd Transcendental Ruby Imbroglio Contest for rubyKaigi (TRICK 2015). + +THESE ARE BAD EXAMPLES! You must NOT use them as a sample code. + +* kinaba/entry.rb: "Best piphilology" - **Gold award** +* ksk\_1/entry.rb: "Most unreadable ALU" - **Silver award** +* monae/entry.rb: "Doubling amphisbaena award" - **Bronze award** +* eregon/entry.rb: "Least general solver" - 4th prize +* ksk\_2/entry.rb: "Most general solver" - 5th prize + +These files are licensed under MIT license. + +For the contest outline and other winning entries, see: + +https://github.com/tric/trick2015 diff --git a/sample/trick2015/eregon/authors.markdown b/sample/trick2015/eregon/authors.markdown new file mode 100644 index 0000000000..68ca8cdfe0 --- /dev/null +++ b/sample/trick2015/eregon/authors.markdown @@ -0,0 +1,3 @@ +* Benoit Daloze (eregon) + * eregontp@gmail.com + * cctld: be diff --git a/sample/trick2015/eregon/entry.rb b/sample/trick2015/eregon/entry.rb new file mode 100644 index 0000000000..b325c6c198 --- /dev/null +++ b/sample/trick2015/eregon/entry.rb @@ -0,0 +1,16 @@ +class String;def[]*a;$*<<a;b;end;end; +_=0;z="C=Fiber;s=$*;a=*0..8;l=C.new{e +xit},*a.product(a).select{|r,c|s[r][c +]==0}."[1,9,_, _,_,8, _,_,5]+"map{|r, +c|C.ne"[_,_,2, _,5,_, _,8,9]+"w{o=s[r +][c];l"[8,_,6, 7,4,_, _,_,_]+"oop{(1. +.9).map{|n|C.yield(s[r][c]=n)if a.non +e?{|k|"[_,_,_, _,_,4, _,9,2]+"s[r][k] +==n||s"[_,2,3, _,7,_, 8,1,_]+"[k][c]= +=n||s["[5,6,_, 8,_,_, _,_,_]+"r-r%3+k +%3][c-c%3+k/3]==n}};s[r][c]=o;C.yield +}}},C."[_,_,_, _,2,7, 9,_,3]+"new{loo +p{puts"[9,3,_, _,8,_, 1,_,_]+" s.map{ +|r|r*'"[2,_,_, 5,_,_, _,4,8]+" '}<<'' +;C.yield}};c=l[i=1];loop{c=l[i+=c.res +ume ? 1:-1]}";eval z.tr ?\n,''
\ No newline at end of file diff --git a/sample/trick2015/eregon/remarks.markdown b/sample/trick2015/eregon/remarks.markdown new file mode 100644 index 0000000000..a56f24da71 --- /dev/null +++ b/sample/trick2015/eregon/remarks.markdown @@ -0,0 +1,70 @@ +### Remarks + +Just run it without arguments: + + ruby entry.rb + +I confirmed the following implementations and platforms: + +* Linux: + * ruby 2.3.0dev (2015-10-30 trunk 52394) [x86\_64-linux] + * ruby 2.2.2p95 (2015-04-13 revision 50295) [x86\_64-linux] + * ruby 2.0.0p647 (2015-08-18) [x86\_64-linux] +* Darwin: + * ruby 2.0.0p247 (2013-06-27 revision 41674) [x86\_64-darwin10.8.0] + * jruby 9.0.3.0 (2.2.2) 2015-10-21 633c9aa Java HotSpot(TM) 64-Bit Server VM 25.11-b03 on 1.8.0\_11-b12 +jit [darwin-x86\_64] + * rubinius 2.2.6.n74 (2.1.0 94b3a9b4 2014-03-15 JI) [x86\_64-darwin12.5.0] + +### Description + +This program shows all solutions of any sudoku puzzle. + +The embedded sudoku puzzle can be changed at wish. + +Giving an empty puzzle (all `0` or `_`), the program will print every possible completed sudoku puzzle. +We do not however make any time guarantee on such behavior. + +The program is rather small for the task: the solver is actually 302 characters long, +assuming the sudoku puzzle is in a variable `s` and encoded as an array of rows of numbers. + +### Internals + +* The program implements backtracking and keeps state in a very elegant way. +* The whole program never goes deeper than 9 stack frames, + but yet can backtrack up to 81 levels! +* The main loop of a program is a dance between cells. + On one end is the solutions, on the other the program ends. +* The program only uses *infinite* loops and no `break`. +* The program interleaves the creation of the solver and the puzzle. +* The program is easy to deobfuscate but finding how it works will be more challenging. +* The last line contains a smiley. + +The author likes good numbers: + + $ wc entry.rb + 15 42 600 + +The inspiration for this entry comes from: + +* A newspaper sudoku with multiple solutions +* An inspiring paper: `Revisiting Coroutines` + +Various tricks used for brevity: + +* The method defined is one of the fews which may contain neither parenthesis nor spaces. +* The program uses the return value of Fiber.yield without arguments. +* `String#b` is used as a very short `self`. + +Design issues: + +* Since `return`-ing from a Fiber is not allowed, the programs must `exit`. +* The program reveals that the cartesian product operator is still too long: `a.product(a)` while it could be `a*a`. + +Note: + +* In the original code, the last cell was: `C.new{loop{yield s; C.yield}}`, + implementing some sort of "forwarding coroutine". + +### Limitation + +* The program does not want any *argument* with you and will quit quietly if you try some. diff --git a/sample/trick2015/kinaba/authors.markdown b/sample/trick2015/kinaba/authors.markdown new file mode 100644 index 0000000000..23d4448cf3 --- /dev/null +++ b/sample/trick2015/kinaba/authors.markdown @@ -0,0 +1,4 @@ +* kinaba + * twitter.com/kinaba + * kiki@kmonos.net + * cctld: jp diff --git a/sample/trick2015/kinaba/entry.rb b/sample/trick2015/kinaba/entry.rb new file mode 100644 index 0000000000..18923a6a9f --- /dev/null +++ b/sample/trick2015/kinaba/entry.rb @@ -0,0 +1,150 @@ +big, temp = Array 100000000**0x04e2 +srand big +alias $curTerm $initTerm + +Numeric +Interrupt + +big += big +printout _pi_ finish if $never +init ||= big +$counter ||= 02 + +private +@mainloop +while 0x00012345 >= $counter + + Rational aprx = 3.141592r + numbase = 0o0000 + + @justonce + def increment + $initTerm ||= Integer srand * 0x00000002 + srand $counter += 0x00000001 + + $noaction + Integer rand + $noaction + rand + rand + alias $line_cnt $. + end + + @lets_just + @assume + diameter = 100000 + + @you + @then_have + permtr |= +3_14159 + + return if $nomeaning + + @onlyuse + increment + + beautiful computer action if $nothing + $sigmaTerm ||= init + $curTerm /= srand and init + pi, = Integer $sigmaTerm unless $nomean + + iterator? + $counter += 1 + atan real_one multiplied by__four unless + srand +big && $counter >> 0b1 + + Enumerable + Fixnum + Bignum + Math + Complex + Comparable + TrueClass + Dir + Encoding + Data + Hash + Method + Enumerator + Exception + Fiber + Errno + FalseClass + Mutex + NilClass + IO + GC + + num = numbase |= srand + + ENV + Float + MatchData + Proc + TracePoint + KeyError + p or + FileTest + File + EOFError + p + p + p + Binding + Time + Class + + $sigmaTerm += $curTerm + puts a HelloWorld if $nomean + SystemExit + + !LoadError + 31i + 3.1415e0 + Array 14 + 3 + IndexError + Range + false + 55555 + NameError + + Object + @ori + @ent + RubyVM + + pi += 3_3_1_3_8 + + @use + @lots_of + @keywords + begin + self + $noaction + not $important + nil + __FILE__.object_id + rescue + next + redo if __LINE__ + defined? +$nomeaning + $noaction + $nomean + break $never + ensure + class PiCompute + end + end + + This code cannot _ be executed with typical style unless true + $curTerm *= num +end + +@ll_set +@re_U_ok + +$Enjoy +$Superb +$TRICK15 and a number + +print pi diff --git a/sample/trick2015/kinaba/remarks.markdown b/sample/trick2015/kinaba/remarks.markdown new file mode 100644 index 0000000000..6316c51fb6 --- /dev/null +++ b/sample/trick2015/kinaba/remarks.markdown @@ -0,0 +1,85 @@ +### Remarks + +Just run it with no argument: + + $ ruby entry.rb + +I confirmed the following implementation/platform: + +- ruby 2.2.3p173 (2015-08-18 revision 51636) [x64-mingw32] + + +### Description + +The program is a [Piphilology](https://en.wikipedia.org/wiki/Piphilology#Examples_in_English) +suitable for Rubyists to memorize the digits of [Pi](https://en.wikipedia.org/wiki/Pi). + +In English, the poems for memorizing Pi start with a word consisting of 3-letters, +1-letter, 4-letters, 1-letter, 5-letters, ... and so on. 10-letter words are used for the +digit `0`. In Ruby, the lengths of the lexical tokens tell you the number. + + $ ruby -r ripper -e \ + 'puts Ripper.tokenize(STDIN).grep(/\S/).map{|t|t.size%10}.join' < entry.rb + 31415926535897932384626433832795028841971693993751058209749445923078164062862... + +The program also tells you the first 10000 digits of Pi, by running. + + $ ruby entry.rb + 31415926535897932384626433832795028841971693993751058209749445923078164062862... + + +### Internals + +Random notes on what you might think interesting: + +- The 10000 digits output of Pi is seriously computed with no cheets. It is calculated + by the formula `Pi/2 = 1 + 1/3 + 1/3*2/5 + 1/3*2/5*3/7 + 1/3*2/5*3/7*4/9 + ...`. + +- Lexical tokens are not just space-separated units. For instance, `a*b + cdef` does + not represent [3,1,4]; rather it's [1,1,1,1,4]. The token length + burden imposes hard constraints on what we can write. + +- That said, Pi is [believed](https://en.wikipedia.org/wiki/Normal_number) to contain + all digit sequences in it. If so, you can find any program inside Pi in theory. + In practice it isn't that easy particularly under the TRICK's 4096-char + limit rule. Suppose we want to embed `g += hij`. We have to find [1,2,3] from Pi. + Assuming uniform distribution, it occurs once in 1000 digits, which already consumes + 5000 chars in average to reach the point. We need some TRICK. + + - `alias` of global variables was useful. It allows me to access the same value from + different token-length positions. + + - `srand` was amazingly useful. Since it returns the "previous seed", the token-length + `5` essentially becomes a value-store that can be written without waiting for the + 1-letter token `=`. + +- Combination of these techniques leads to a carefully chosen 77-token Pi computation + program (quoted below), which is embeddable to the first 242 tokens of Pi. + Though the remaining 165 tokens are just no-op fillers, it's not so bad compared to + the 1000/3 = 333x blowup mentioned above. + + + big, temp = Array 100000000**0x04e2 + srand big + alias $curTerm $initTerm + big += big + init ||= big + $counter ||= 02 + while 0x00012345 >= $counter + numbase = 0x0000 + $initTerm ||= Integer srand * 0x00000002 + srand $counter += 0x00000001 + $sigmaTerm ||= init + $curTerm /= srand + pi, = Integer $sigmaTerm + $counter += 1 + srand +big && $counter >> 0b1 + num = numbase |= srand + $sigmaTerm += $curTerm + pi += 3_3_1_3_8 + $curTerm *= num + end + print pi + +- By the way, what's the blowup ratio of the final code, then? + It's 242/77, whose first three digits are, of course, 3.14. diff --git a/sample/trick2015/ksk_1/authors.markdown b/sample/trick2015/ksk_1/authors.markdown new file mode 100644 index 0000000000..bd6d41f6c7 --- /dev/null +++ b/sample/trick2015/ksk_1/authors.markdown @@ -0,0 +1,3 @@ +* Keisuke Nakano + * ksk@github, ksknac@twitter + * cctld: jp diff --git a/sample/trick2015/ksk_1/entry.rb b/sample/trick2015/ksk_1/entry.rb new file mode 100644 index 0000000000..64d3efd799 --- /dev/null +++ b/sample/trick2015/ksk_1/entry.rb @@ -0,0 +1 @@ +%%%while eval '_=%%r%%(.)...\1=%%=~[%%%%,,,,,%%%s ?=]*%%%%%%#"]*%%%%3x+1?%%'.% %%",%*p(_||=eval($**%%%)) diff --git a/sample/trick2015/ksk_1/remarks.markdown b/sample/trick2015/ksk_1/remarks.markdown new file mode 100644 index 0000000000..b822dc55c8 --- /dev/null +++ b/sample/trick2015/ksk_1/remarks.markdown @@ -0,0 +1,120 @@ +### Remarks + +The program is run with a positive integer as an argument, e.g., +```shell + ruby entry.rb 27 +``` +It has been confirmed to be run on +``` + ruby 1.9.3p385 (2013-02-06 revision 39114) [x86_64-darwin11.4.2] + ruby 2.0.0p481 (2014-05-08 revision 45883) [universal.x86_64-darwin13] + ruby 2.2.3p173 (2015-08-18 revision 51636) [x86_64-linux] +``` + + +### Description + +The program prints a Collatz sequence started with a given number, +that is, it repeatedly outputs numbers obtained by applying the +following Half-Or-Triple-Plus-One (HOTPO) process to the previous +number: + +> If the number is even, divide it by two, otherwise, multiply it by three and add one. + +until the number becomes 1. Collatz conjectured that no matter from +the process starts it always eventually terminates. This is still +an open problem, hence the program may not terminate for some +numbers. It is known that there is no such exception below 2<sup>60</sup>. + + +### Internals + +The source code does not contain either conditional branch or arithmetic operation. +The trick shall be revealed step by step. + +First, the code is obfuscated by using `%`-notations, +`*`(String#join), `%`-formatting, restructuring, and so on. +Here is an equivalent readable program: +```ruby +n = ARGV[0].to_i +begin + # do nothing +end while begin + puts n + n = (/(.)...\1=/ =~ eval('[",,,,,"'+ '",'*n + ' ?=].join#"].join("3x+1?")')) +end +``` +The line +```ruby + n = (/(.)...\1=/ =~ eval('[",,,,,"'+ '",'*n + ' ?=].join#"].join("3x+1?")')) +``` +performs the HOTPO process. +The `eval` expression here returns a string as explained in detail later. +Since *regex*`=~`*str* returns index of first match of *regex* in *str*, +the regular expression `(.)...\1` must match the string +at index `n/2` if `n` is even and +at `3*n+1` if `n` is odd greater than 1. +The match must fail in the case of `n = 1` so that it returns `nil`. + +The key of simulating the even-odd conditional branch on `n` in the +HOTPO process is an `n`-length sequence of the incomplete fragments +`",` where the double-quote `"` changes its role of opening/closing +string literals alternately. If `n` is even, the string in the `eval` +expression is evaluated as +```ruby + => '[",,,,,"'+ '",' + '",' + '",' + ... + '",' + ' ?=].join#...' + => '[",,,,,"",",",...", ?=].join#...' +``` +where the last double-quote `"` is closing hence the code after `#` is +ignored as comments. Note that `"ab""cd"` in Ruby is equivalent to +`"abcd"`. Therefore the `eval` expression is evaluated into +```ruby + ",,,,,...,=" +``` +where the number of commas is `5+n/2`. +As a result, the regular expression `(.)...\1=` matches `,,,,,=` +at the end of string, that is, at index `5+n/2-5 = n/2`. + +If `n` is odd, the string in the `eval` expression is evaluated as +```ruby + => '[",,,,,"'+ '",' + '",' + '",' + '",' + ... + '",' + ' ?=].join#"].join("3x+1?")' + => '[",,,,,"",",",",...,", ?=].join#"].join("3x+1?")' +``` +where the last element in the array is `", ?=].join#"`. Threfore the +`eval` expression is evaluated into +``` + ",,,,,,3x+1?,3x+1?,...,3x+1?, ?=].join#" +``` +where the number of `,3x+1?` is `(n-1)/2`. As a result, the regular +expression `(.)...\1=` matches `?, ?=` at the almost end of string, +that is, at index `5+(n-1)/2*6-1 = 3n+1`, provided that the match +fails in the case of `n = 1` because the symbol `?` occurs only once +in the string. + +One may notice that the string `3x+1` in the code could be other +four-character words. I chose it because the Collatz conjecture is +also called the 3x+1 problem. + + +### Variant + +The Collatz conjecture is equivalently stated as, + +> no matter from the HOTPO process starts, it always eventually + reaches the cycle of 4, 2, and 1 + +instead of termination of the process at 1. This alternative +statement makes the program simpler because we do not have to care the +case of n = 1. It can be obtained by replacing the regular expression +is simply `/=/` and removing a padding `",,,,,"`. The program no +longer terminates, though. + + +### Limination + +The implementation requires to manipulate long strings even for some +small starting numbers. For example, starting from 1,819, the number +will reach up to 1,276,936 which causes SystemStackError on Ruby 1.9.3. +The program works on Ruby 2.0.0 and 2.2.3, though. + + diff --git a/sample/trick2015/ksk_2/abnormal.cnf b/sample/trick2015/ksk_2/abnormal.cnf new file mode 100644 index 0000000000..084303f041 --- /dev/null +++ b/sample/trick2015/ksk_2/abnormal.cnf @@ -0,0 +1,6 @@ +c Example CNF format file +c +p cnf 4 3 +1 3 -4 0 +4 0 2 +-3 diff --git a/sample/trick2015/ksk_2/authors.markdown b/sample/trick2015/ksk_2/authors.markdown new file mode 100644 index 0000000000..bd6d41f6c7 --- /dev/null +++ b/sample/trick2015/ksk_2/authors.markdown @@ -0,0 +1,3 @@ +* Keisuke Nakano + * ksk@github, ksknac@twitter + * cctld: jp diff --git a/sample/trick2015/ksk_2/entry.rb b/sample/trick2015/ksk_2/entry.rb new file mode 100644 index 0000000000..506e9e6917 --- /dev/null +++ b/sample/trick2015/ksk_2/entry.rb @@ -0,0 +1 @@ +_='s %sSATISFIABLE';puts eval$<.read.gsub(/.*p.*?(\d+).*?$|\d+/m){$1?%w[?-* +'=-'=~/#{'(-?)'* }-*=(?=]*$1:$&>?0?"\\#$&$|":'$)(?='}+')/x?[_%p%i=0,[*$~].map{|x|x>?-?:v:eval(x+?1)*i-=1}*" "]:_%:UN'
\ No newline at end of file diff --git a/sample/trick2015/ksk_2/quinn.cnf b/sample/trick2015/ksk_2/quinn.cnf new file mode 100644 index 0000000000..556a9b33f5 --- /dev/null +++ b/sample/trick2015/ksk_2/quinn.cnf @@ -0,0 +1,21 @@ +c quinn.cnf +c +p cnf 16 18 + 1 2 0 + -2 -4 0 + 3 4 0 + -4 -5 0 + 5 -6 0 + 6 -7 0 + 6 7 0 + 7 -16 0 + 8 -9 0 + -8 -14 0 + 9 10 0 + 9 -10 0 +-10 -11 0 + 10 12 0 + 11 12 0 + 13 14 0 + 14 -15 0 + 15 16 0
\ No newline at end of file diff --git a/sample/trick2015/ksk_2/remarks.markdown b/sample/trick2015/ksk_2/remarks.markdown new file mode 100644 index 0000000000..bb9b705773 --- /dev/null +++ b/sample/trick2015/ksk_2/remarks.markdown @@ -0,0 +1,204 @@ +### Remarks + +The program is run with a data file from the standard input, e.g., +```shell + ruby entry.rb < data +``` +where ``<`` can be omitted. The data file must be in the DIMACS CNF +format (see Description for detail). It has been confirmed to be run on +``` + ruby 1.9.3p385 (2013-02-06 revision 39114) [x86_64-darwin11.4.2] + ruby 2.0.0p481 (2014-05-08 revision 45883) [universal.x86_64-darwin13] + ruby 2.2.3p173 (2015-08-18 revision 51636) [x86_64-linux] +``` +For particular inputs, the program works differently on these environments +(see Limitation). + + +### Description + +The program is a very small SAT solver with 194 bytes making use of a +powerful feature of Regexp matching in Ruby. It receives a data file +from the standard input in the DIMACS CNF that is a standard format +for inputs of SAT solvers. For example, the text in the DIMACS CNF +format, +``` +c +c This is a sample input file. +c +p cnf 3 5 + 1 -2 3 0 +-1 2 0 +-2 -3 0 + 1 2 -3 0 + 1 3 0 +``` +corresponds to a propositional formula in conjunctive normal form, + + (L1 ∨ ¬L2 ∨ L3) ∧ + (¬L1 ∨ L2) ∧ + (¬L2 ∨ ¬L3) ∧ + (L1 ∨ L2 ∨ ¬L3) ∧ + (L1 ∨ L3). + +In the DIMACS CNF format, the lines starting with ``c`` are comments +that are allowed only before the line ``p cnf ...``. The line ``p cnf +3 5`` represents that the problem is given in conjunctive normal form +with 3 variables (L1,L2,and L3) and 5 clauses. A clause is given by a +sequence of the indices of positive literals and the negative indices +of negative literals. Each clause is terminated by ``0``. For the +input above, the program outputs +``` +s SATISFIABLE +v 1 2 -3 +``` +because the formula is satisfiable by L1=true, L2=true, and L3=false. +If an unsatisfiable formula is given, the program should output +``` +s UNSATISFIABLE +``` +This specification is common in most exiting SAT solvers and required +for entries of [SAT competition](http://www.satcompetition.org/). + +The program is very small with no other external libraries thanks to +the wealth of string manipulations in Ruby. It is much smaller than +existing small SAT solvers like [minisat](http://minisat.se/) and +[picosat](http://fmv.jku.at/picosat/)! + + +### Internals + +The basic idea of the program is a translation from DIMACS CNF format +into Ruby. For example, the data file above is translated into a +``Regexp`` matching expression equivalent to +```ruby + '---=-' =~ + /(-?)(-?)(-?)-*=(?=\1$|-\2$|\3$|$)(?=-\1$|\2$|$)(?=-\2$|-\3$|$)(?=\1$|\2$|-\3$|$)(?=\1$|\3$|$)(?=)/ +``` +that returns ``MatchData`` if the formula is satisfiable and otherwise +returns ``nil``. The beginning of regular expression +``(-?)(-?)(-?)-*=`` matches a string ``"---="`` so that each +capturing pattern ``(-?)`` matches either ``"-"`` or `""`, which +corresponds to an assignment of true or false, respectively, for a +propositional variable. Each clause is translated into positive +lookahead assertion like ``(?=\1$|-\2$|\3$|$)`` that matches +``"-"`` only when ``\1`` holds ``"-"``, ``\2`` holds ``""``, or ``\3`` +holds ``"-"``. This exactly corresponds to the condition for +L1∨¬L2∨L3 to be true. The last case ``|$`` never matches +``"-"`` but it is required for making the translation simple. +The last meaningless positive lookahead assertion ``(?=)`` is added +for a similar reason. This translation is based on +[Abigail's idea](http://perl.plover.com/NPC/NPC-3SAT.html) where a +3SAT formula is translated into a similar Perl regular expression. +The differences are the submitted Ruby program translates directly +from the DIMACS CNF format and tries to make the code shorter by using +lookahead assertion which can also make matching more faster. + +Thanks to the ``x`` option for regular expression, the input above is +simply translated into +```ruby + ?-*3+'=-'=~/#{'(-?)'*3}-*=(?= + \1$| -\2$| \3$| $)(?= + -\1$| \2$| $)(?= + -\2$| -\3$| $)(?= + \1$| \2$| -\3$| $)(?= + \1$| \3$| $)(?= + )/x +``` +which has a structure similar to the DIMACS CNF format. + +The part of formatting outputs in the program is obfuscated as an +inevitable result of 'golfing' the original program +```ruby + if ...the matching expression above... then + puts 's SATISFIABLE' + puts 'v '+$~[1..-1].map.with_index{|x,i| + if x == '-' then + i+1 + else + ['-',i+1].join + end + }.join(' ') + else + puts 's UNSATISFIABLE' + end +``` +In the satisfiable case, the MatchData ``$~`` obtained by the regular expression +has the form of +``` + #<MatchData "---=" 1:"-" 2:"-" 3:""> +``` +which should be translated into a string ``1 2 -3``. The golfed code simply +does it by `eval(x+?1)*i-=1` where ``x`` is matched string ``"x"`` or ``""`` +and ``i`` be a negated index. + + +### Data files + +The submission includes some input files in the DIMACS CNF format for +testing the program. + +* [sample.cnf](sample.cnf) : an example shown above. + +* [unsat.cnf](unsat.cnf) : an example of an unsatisfiable formula. + +* [quinn.cnf](quinn.cnf) : an example from Quinn's text, 16 variables and 18 clauses + (available from [http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html]) + +* [abnormal.cnf](abnormal.cnf) : an example from [the unofficial manual of the DIMACS challenge](http://www.domagoj-babic.com/uploads/ResearchProjects/Spear/dimacs-cnf.pdf) + where a single clause may be on multiple lines. + +* [uf20-01.cnf](uf20-01.cnf) : an example, with 20 variables and 91 clauses, from [SATLIB benchmark suite](http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html). The last two lines are removed from the original because they are illegal in the DIMACS CNF format (all examples in 'Uniform Random-3-SAT' of the linked page need this modification). + + +### Limitation + +The program may not work when the number of variables exceeds 99 +because ``\nnn`` in regular expression with number ``nnn`` does not +always represent backreference but octal notation of characters. For +example, +```ruby + /#{"(x)"*999}:\502/=~"x"*999+":x" + /#{"(x)"*999}:\661/=~"x"*999+":x" + /#{"(x)"*999}:\775/=~"x"*999+":x" +``` +fail due to the syntax error (invalid escape), while +```ruby + /#{"(x)"*999}:\508/=~"x"*999+":x" + /#{"(x)"*999}:\691/=~"x"*999+":x" + /#{"(x)"*999}:\785/=~"x"*999+":x" +``` +succeed (to return 0) because 508, 691, and 785 are not in octal notation. +Since Ruby 1.9.3 incorrectly returns ``nil`` instead of terminating +with the error for +```ruby + /#{"(x)"*999}:\201/=~"x"*999+":x" + /#{"(x)"*999}:\325/=~"x"*999+":x" +``` +the present SAT solver may unexpectedly return "UNSATISFIABLE" even +for satisfiable inputs. This happens when the number is in octal +notation starting with either 2 or 3. + +In the case of the number starting with 1, the code like the above +does work on all versions of Ruby I tried. For example, +```ruby + /#{"(x)"*999}:\101/=~"x"*999+":x" + /#{"(x)"*999}:\177/=~"x"*999+":x" +``` +succeed (to return 0). Interestingly, +```ruby + /#{"(x)"*999}:\101/=~"x"*999+":\101" + /#{"(x)"*999}:\177/=~"x"*999+":\177" +``` +return ``nil``, while +```ruby + /:\101/=~":\101" + /:\177/=~":\177" +``` +succeed to return 0. The meaning of ``\1nn`` in regular expression +seems to depend on the existence of capturing expressions. + +In spite of these Ruby's behaviors, we have a good news! The present +SAT sover does not suffer from the issues because the program cannot +return solutions in practical time for inputs with variables more than +40.
\ No newline at end of file diff --git a/sample/trick2015/ksk_2/sample.cnf b/sample/trick2015/ksk_2/sample.cnf new file mode 100644 index 0000000000..295f81c942 --- /dev/null +++ b/sample/trick2015/ksk_2/sample.cnf @@ -0,0 +1,9 @@ +c +c This is a sample input file. +c +p cnf 3 5 + 1 -2 3 0 +-1 2 0 +-2 -3 0 + 1 2 -3 0 + 1 3 0 diff --git a/sample/trick2015/ksk_2/uf20-01.cnf b/sample/trick2015/ksk_2/uf20-01.cnf new file mode 100644 index 0000000000..0d9503c451 --- /dev/null +++ b/sample/trick2015/ksk_2/uf20-01.cnf @@ -0,0 +1,99 @@ +c This Formular is generated by mcnf +c +c horn? no +c forced? no +c mixed sat? no +c clause length = 3 +c +p cnf 20 91 + 4 -18 19 0 +3 18 -5 0 +-5 -8 -15 0 +-20 7 -16 0 +10 -13 -7 0 +-12 -9 17 0 +17 19 5 0 +-16 9 15 0 +11 -5 -14 0 +18 -10 13 0 +-3 11 12 0 +-6 -17 -8 0 +-18 14 1 0 +-19 -15 10 0 +12 18 -19 0 +-8 4 7 0 +-8 -9 4 0 +7 17 -15 0 +12 -7 -14 0 +-10 -11 8 0 +2 -15 -11 0 +9 6 1 0 +-11 20 -17 0 +9 -15 13 0 +12 -7 -17 0 +-18 -2 20 0 +20 12 4 0 +19 11 14 0 +-16 18 -4 0 +-1 -17 -19 0 +-13 15 10 0 +-12 -14 -13 0 +12 -14 -7 0 +-7 16 10 0 +6 10 7 0 +20 14 -16 0 +-19 17 11 0 +-7 1 -20 0 +-5 12 15 0 +-4 -9 -13 0 +12 -11 -7 0 +-5 19 -8 0 +1 16 17 0 +20 -14 -15 0 +13 -4 10 0 +14 7 10 0 +-5 9 20 0 +10 1 -19 0 +-16 -15 -1 0 +16 3 -11 0 +-15 -10 4 0 +4 -15 -3 0 +-10 -16 11 0 +-8 12 -5 0 +14 -6 12 0 +1 6 11 0 +-13 -5 -1 0 +-7 -2 12 0 +1 -20 19 0 +-2 -13 -8 0 +15 18 4 0 +-11 14 9 0 +-6 -15 -2 0 +5 -12 -15 0 +-6 17 5 0 +-13 5 -19 0 +20 -1 14 0 +9 -17 15 0 +-5 19 -18 0 +-12 8 -10 0 +-18 14 -4 0 +15 -9 13 0 +9 -5 -1 0 +10 -19 -14 0 +20 9 4 0 +-9 -2 19 0 +-5 13 -17 0 +2 -10 -18 0 +-18 3 11 0 +7 -9 17 0 +-15 -6 -3 0 +-2 3 -13 0 +12 3 -2 0 +-2 -3 17 0 +20 -15 -16 0 +-5 -17 -19 0 +-20 -18 11 0 +-9 1 -5 0 +-19 9 17 0 +12 -2 17 0 +4 -16 -5 0 diff --git a/sample/trick2015/ksk_2/unsat.cnf b/sample/trick2015/ksk_2/unsat.cnf new file mode 100644 index 0000000000..7283933a9f --- /dev/null +++ b/sample/trick2015/ksk_2/unsat.cnf @@ -0,0 +1,11 @@ +c +c This is a sample input file. +c (unsatisfiable) +c +p cnf 3 5 +1 -2 3 0 +-1 2 0 +-2 -3 0 +1 2 -3 0 +1 3 0 +-1 -2 3 0 diff --git a/sample/trick2015/monae/authors.markdown b/sample/trick2015/monae/authors.markdown new file mode 100644 index 0000000000..58d63b16ac --- /dev/null +++ b/sample/trick2015/monae/authors.markdown @@ -0,0 +1 @@ +monae (@monae, jp) diff --git a/sample/trick2015/monae/entry.rb b/sample/trick2015/monae/entry.rb new file mode 100644 index 0000000000..9524086b29 --- /dev/null +++ b/sample/trick2015/monae/entry.rb @@ -0,0 +1,26 @@ + ;; ;; ;; ;;
+ ;; ;; ;; ;;
+ ;;eval$s =%q[i=1#
+ eval(%q[ xxxxxxxx
+ xx xxxx xx xx xxxx xx
+ xx xxxx xx xx xxxx xx
+ xxxxxxxx xxxxxxxx
+ xxxxxxxx xxxxxxxx
+ xx xx xxxxxxxxxx xx xxxxxxxx
+ j, t, p=0,[?;]," ev al$s=%qx
+[#$s]".split*"";i,j,t=i-j,i+j,(x
+ [b=?\s]*j.abs+t).map{|s|r=t.shix
+ft ||b;r.gsub!(?;){p.slice!0}if $x
+ f| |=p>p=p.center(i*i+j*j,?;);r ,x
+ s=[s,r]if(i*j<0);(b*i.abs+s).ljx
+ ust(r.size).gsub(b){r[$`.size]|x
+ |b}}unti l$ f;puts(t)# xx xx
+ xxxxxxxx xx xxxxxxxxxx xx xx
+xxxxxxxx xxxxxxxx
+ xxxxxxxx xxxxxxxx
+xx xxxx xx xx xxxx xx
+ xx xxxx xx xx xxxx xx
+ xxxxxxxx x].gsub\
+ /x.*|\s/ ,"")#];;
+ ;; ;; ;; ;;
+ ;; ;; ;; ;;
diff --git a/sample/trick2015/monae/remarks.markdown b/sample/trick2015/monae/remarks.markdown new file mode 100644 index 0000000000..48be61bd12 --- /dev/null +++ b/sample/trick2015/monae/remarks.markdown @@ -0,0 +1,25 @@ + +# How to run + +``` +ruby entry.rb +ruby entry.rb | ruby +ruby entry.rb | ruby | ruby +ruby entry.rb | ruby | ruby | ruby +... +``` + +Confirmed on the following environments: +- ruby 2.2.3p173 (2015-08-18 revision 51636) [x86_64-darwin14] +- ruby 2.0.0p353 (2013-11-22) [i386-mingw32] + +# Description + +A simple quine which prints itself twice +on a slightly complex base. + +> geminum caput amphisbaenae, hoc est et a cauda, +> tamquam parum esset uno ore fundi venenum. +> aliis squamas esse, aliis picturas, omnibus exitiale virus. +> +> — <cite>GAIUS PLINIUS SECUNDUS, Naturalis Historia 8.85.1</cite> |