SAT solver by gmk

x=n="";r=[]
$<.read.split(/ *0?\n */).map{|l|l<?c?x<<"(#{l.gsub(/ +|\-|\d+/){["1-","a[#$&]",?|][$&<=>?-]}})&":n=l[/\d+/].to_i}
f=eval"->a{#{x}1}"
(2**n*2).times{|w|f[w]>0&&r<<w}
puts"s %sSATISFIABLE%s"%(r!=[]?["","
v "+(r=r.sort_by{|q|q.to_s(2).split(?0).map(&:size).sort.reverse}[-1];(1..n).map{|k|?-*-~-r[k]+k.to_s}*" ")]:[:UN,""])

Note that non-ascii characters in the above source code will be escaped (such as \x9f).

To protect the system from spam, please input your favorite sport (hint: I believe its name must start with 'g', case insensitive)

download

return to the top page