diff options
| author | mame <mame@b2dd03c8-39d4-4d8f-98ff-823fe69b080e> | 2015-12-11 14:37:06 +0000 |
|---|---|---|
| committer | mame <mame@b2dd03c8-39d4-4d8f-98ff-823fe69b080e> | 2015-12-11 14:37:06 +0000 |
| commit | 5c28308f9fbb44bfc73fe8af58fdcce0ad0379f2 (patch) | |
| tree | b096f65a2e92c00028406ba988cd5e55094ab2f4 /sample/trick2015/ksk_2 | |
| parent | d65bc80d3f71bf5423a6a6d9b3f8d4ff2faf6bd5 (diff) | |
* sample/trick2015/: added the award-winning entries of TRICK 2015.
See https://github.com/tric/trick2015 for the contest outline.
git-svn-id: svn+ssh://ci.ruby-lang.org/ruby/trunk@53041 b2dd03c8-39d4-4d8f-98ff-823fe69b080e
Diffstat (limited to 'sample/trick2015/ksk_2')
| -rw-r--r-- | sample/trick2015/ksk_2/abnormal.cnf | 6 | ||||
| -rw-r--r-- | sample/trick2015/ksk_2/authors.markdown | 3 | ||||
| -rw-r--r-- | sample/trick2015/ksk_2/entry.rb | 1 | ||||
| -rw-r--r-- | sample/trick2015/ksk_2/quinn.cnf | 21 | ||||
| -rw-r--r-- | sample/trick2015/ksk_2/remarks.markdown | 204 | ||||
| -rw-r--r-- | sample/trick2015/ksk_2/sample.cnf | 9 | ||||
| -rw-r--r-- | sample/trick2015/ksk_2/uf20-01.cnf | 99 | ||||
| -rw-r--r-- | sample/trick2015/ksk_2/unsat.cnf | 11 |
8 files changed, 354 insertions, 0 deletions
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 |