Submission details
Task:3SAT solver
Sender:taige
Submission time:2020-09-19 16:00:14 +0300
Language:Python3 (PyPy3)
Status:READY
Result:
Test results
testverdicttime
#1ACCEPTED0.05 sdetails
#2ACCEPTED0.05 sdetails
#3ACCEPTED0.05 sdetails
#4ACCEPTED0.05 sdetails
#5ACCEPTED0.05 sdetails
#6--details
#7--details
#8--details
#9--details
#10--details
#11--details
#12--details
#13--details
#14--details
#15--details
#16--details

Code

from itertools import product


def main():
    first_line = input().split()
    n, var_num = int(first_line[-1]), int(first_line[-2])
    final = []
    for i in range(n):
        line = [int(x) for x in input()[:-2].split()]
        line = ["var[" + str(x - 1) + "]" if x >
                0 else "(not var[" + str(- x - 1) + "])" for x in line]
        final.append("(" + " or ".join(line) + ")")
    final_logic = " and ".join(final)
    l = [True, False]
    for var in product(l, repeat=var_num):
        if eval(final_logic):
            print("s SATISFIABLE")
            print("v", end="")
            for i in range(1, var_num + 1):
                print(" " + str(i) if var[i - 1] else " -" + str(i), end="")
            print(" 0")
            break



def main2():
    first_line = input().split()
    n, var_num = int(first_line[-1]), int(first_line[-2])
    possibleValue = dict()
    for i in range(1, var_num+1):
        possibleValue[i] = [True, False]
    for i in range(n):
        line = [int(x) for x in input()[:-2].split()]
        for x in line:
            if x < 0:
                if possibleValue[-x] == [True]:
                    possibleValue[-x] = []
                else:
                    possibleValue[-x] = [False]
            else:
                if possibleValue[x] == [False]:
                    possibleValue[x] = []
                else:
                    possibleValue[x] = [True]
    print(possibleValue)
    
main()

#
#[(False, False, False), (False, False, True), (False, True, False), (False, True, True), (True, False, False), (True, False, True), (True, True, False), (True, True, True)]

Test details

Test 1

Verdict: ACCEPTED

input
p cnf 3 3
-2 3 -1 0
2 3 1 0
-1 -2 -3 0

correct output
(empty)

user output
s SATISFIABLE
v 1 -2 3 0

Test 2

Verdict: ACCEPTED

input
p cnf 3 3
1 -3 -2 0
1 2 3 0
-1 3 -2 0

correct output
(empty)

user output
s SATISFIABLE
v 1 2 3 0

Test 3

Verdict: ACCEPTED

input
p cnf 5 5
3 -1 -5 0
2 4 1 0
3 -4 5 0
-5 -4 2 0
...

correct output
(empty)

user output
s SATISFIABLE
v 1 2 -3 -4 -5 0

Test 4

Verdict: ACCEPTED

input
p cnf 8 5
4 -5 3 0
-5 -2 -4 0
8 -1 2 0
-3 5 6 0
...

correct output
(empty)

user output
s SATISFIABLE
v 1 2 3 4 -5 6 7 8 0

Test 5

Verdict: ACCEPTED

input
p cnf 10 10
5 9 3 0
3 7 4 0
-10 2 -1 0
-6 4 2 0
...

correct output
(empty)

user output
s SATISFIABLE
v 1 2 3 4 5 6 7 8 9 -10 0

Test 6

Verdict:

input
p cnf 1000 1000
218 -786 362 0
917 -477 -142 0
-371 701 -71 0
376 -524 -131 0
...

correct output
(empty)

user output
(empty)

Test 7

Verdict:

input
p cnf 1000 1000
-347 913 411 0
-636 -948 -23 0
262 584 -137 0
-832 627 -775 0
...

correct output
(empty)

user output
(empty)

Test 8

Verdict:

input
p cnf 1000 1000
18 556 -650 0
353 33 -765 0
573 -401 -81 0
903 -727 -81 0
...

correct output
(empty)

user output
(empty)

Test 9

Verdict:

input
p cnf 10000 1000
9123 -904 -9430 0
8097 -9174 8218 0
4006 6631 -6981 0
-9882 -8579 114 0
...

correct output
(empty)

user output
(empty)

Test 10

Verdict:

input
p cnf 10000 10000
-5406 13 3055 0
9649 -4669 2543 0
9573 70 6642 0
-7247 -7063 -3679 0
...

correct output
(empty)

user output
(empty)

Test 11

Verdict:

input
p cnf 10000 10000
1046 386 -9246 0
-8809 -7155 -3610 0
-756 1484 8757 0
5954 485 -3403 0
...

correct output
(empty)

user output
(empty)

Test 12

Verdict:

input
p cnf 10000 10000
905 9130 -2491 0
5382 -8040 6550 0
409 -1140 5181 0
-7597 6500 8010 0
...

correct output
(empty)

user output
(empty)

Test 13

Verdict:

input
p cnf 100 100
44 -24 -54 0
35 11 51 0
-79 -91 -26 0
-69 63 -64 0
...

correct output
(empty)

user output
(empty)

Test 14

Verdict:

input
p cnf 1000 1000
644 -384 -491 0
603 -228 866 0
-149 173 413 0
-954 -456 -883 0
...

correct output
(empty)

user output
(empty)

Test 15

Verdict:

input
p cnf 10000 10000
4889 -6889 246 0
-1046 431 -4659 0
1064 9683 2950 0
5140 -2131 -2105 0
...

correct output
(empty)

user output
(empty)

Test 16

Verdict:

input
p cnf 100000 10000
-97152 27630 29913 0
-41365 41432 26220 0
-66537 -46395 -83221 0
62364 -79006 -76860 0
...

correct output
(empty)

user output
(empty)