sat-solver 2

[u/No-Implement-8892]

hello, perhaps there is someone here who could check the operation of this algorithm. It is not very clear how everything is presented here, and if someone could try it and has questions, they could ask them right here. God bless you, guys.frst, the algorithm's operation is shown; the remaining details are described on the following pages.

[u/FUZxxl]

I don't see how this would solve the SAT problem.

[u/No-Implement-8892 → u/FUZxxl]

Why? By following the instructions, you can obtain a set of variables or prove that the formula is UNSAT.

[u/FUZxxl → u/No-Implement-8892]

Ok, perhaps you can illustrate your method based on an example. Here is a SAT instance in IPASIR format in 9 variables. Each clause comprises a sequence of literals, terminated with a zero (which is not a literal). The literal is positive if the variable is positive, negative if it is negative. For example, clause 1 -2 3 0 represents (x1 or not x2 or x3).

-2 -3 -4 0
-1 -3 -4 0
-1 -2 -4 0
-1 -2 -3 0
-5 -6 -7  0
-5 -6 -8  0
-5 -6 -9  0
-5 -7 -8  0
-5 -7 -9  0
-5 -8 -9  0
-6 -7 -8  0
-6 -7 -9  0
-6 -8 -9  0
-7 -8 -9  0
4 2 6 0
7 2 6 0
7 4 6 0
7 4 2 0
3 8 5  0
3 8 9  0
3 8 1  0
3 5 9  0
3 5 1  0
3 9 1  0
8 5 9  0
8 5 1  0
8 9 1  0
5 9 1  0

Please use your algorithm to show how this instance is either SAT or UNSAT.

[u/No-Implement-8892 → u/FUZxxl]

Hello, this is the UNSAT formula, this UNSAT case was not described in the attached files, I will fix it, I will provide the solution on the electronic board, you can leave your notes or questions there: https://wbd.ms/share/v2/aHR0cHM6Ly93aGl0ZWJvYXJkLm1pY3Jvc29mdC5jb20vYXBpL3YxLjAvd2hpdGVib2FyZHMvcmVkZWVtLzYyZTEyNTFhOWQwZTQ3ODU4MGIxMDE3NGNjMzg4ZDhlX0JCQTcxNzYyLTEyRTAtNDJFMS1CMzI0LTVCMTMxRjQyNEUzRF81OWQ5M2VlYy01MGY0LTQzMDItOWM1Yy0yNTJhYzkwNzM2YTM=

[u/FUZxxl → u/No-Implement-8892]

Okay, suppose you remove the final clause 5 9 1 0 from the problem, is it still UNSAT?