Correspondence Between Variable no. in CNF and Minisat Output?

[Payman]

Dear all,
I am beginner in using Minisat.I am trying to use Minisat in SAT_ATPG
but I have two problem:
I searched the forum but I did not find clear answer.
1-What is the correspondence between variable no. in CNF and output of
Ministat?
Example:suppose that CNF file is :
p cnf 7 11
-3 -5 0
3 5 0
1 -6 0
2 -6 0
-1 -2 6 0
5 6 -7 0
-6 7 0
-5 7 0
4 -7 0
-4 7 0
4 0
and the output of Minisat is
SAT
-1 -2 -3 4 5 -6 7 0
what is the correspondence between variable no. in CNF and minisat
output? for example -2 means that variable "2" in CNF should be zero
or it means that second variable in CNF that is ("5") should be zero
or something else?
2-suppose that I changed variable 3 in CNF to for example 15; I this
case the output of Minisat is:
SAT
-1 -2 -3 4 5 -6 7 -8 -9 -10 -11 -12 -13 -14 -15 0
what this happen while several variables has not been used in CNF at
all
Can someone suggest a clear answer that explain what is one to one
corresponding between variable no in CNF and output of Minisat ?


Best regards,

Payman

[Payman Behnam]

[Yuval Mines]

Hi

It means that variable "2" in CNF should be set zero

You can also take a simple example and try to set the solution.

Best

Yuval

--
Yuval Mines

[a_tom]

variable "2" not the variable number 2. Also, in case of your second question, I guess you changed variable 3 at one of its place and not at all of the places(i.e. you did not replace the variable "3" with variable "15" in whole of the cnf file)?

रविवार, 8 अप्रैल 2012 4:02:37 pm UTC+2 को, Payman ने लिखा:

[Lucas Rodrigues]

I have the same problem of your second question!