ruby--ruby/sample/trick2015/ksk_2/remarks.markdown

Remarks

The program is run with a data file from the standard input, e.g.,

  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.

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 and 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

 '---=-' =~ 
 /(-?)(-?)(-?)-*=(?=\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 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

  ?-*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

   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 : an example shown above.

• unsat.cnf : an example of an unsatisfiable formula.

• 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 : an example from the unofficial manual of the DIMACS challenge where a single clause may be on multiple lines.

• uf20-01.cnf : an example, with 20 variables and 91 clauses, from SATLIB benchmark suite. 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,

  /#{"(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

  /#{"(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

  /#{"(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,

  /#{"(x)"*999}:\101/=~"x"*999+":x"
  /#{"(x)"*999}:\177/=~"x"*999+":x"

succeed (to return 0). Interestingly,

  /#{"(x)"*999}:\101/=~"x"*999+":\101"
  /#{"(x)"*999}:\177/=~"x"*999+":\177"

return nil, while

  /:\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.