SAT solver

Submit

Language is selected by the extension of the file. See the list of supported languages to know the extension of your language.

Problem

See <a href="https://github.com/tric/trick2015/blob/master/ksk_2/remarks.markdown">this description for detail</a>. If there are multiple solutions, output the one which have as many leading positive numbers as possible.

This problem is a test for <a href="rejudge.html">the rejudge feature</a>. Hopefully luck-depend solutions won't work anymore, though this problem itself wouldn't be a good problem because this could be exploitable by embeded solutions.

Options

exec is denied

rejudge feature is enabled

now post-mortem time, all source codes will be revealed

Sample input:_

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

Sample output:

s SATISFIABLE
v 1 2 3 -4 5 6 7 8 9 10 -11 12 13 -14 -15 16

Sample input:_

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

Sample output:

s UNSATISFIABLE

Sample input:_

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

Sample output:

s SATISFIABLE
v 1 2 -3

Ranking

Ruby _

Ruby2 _

Perl _

Xtal _

PARI/GP _

C _

sed _

jq _

R _

Language Ranking_

return to the top page