Discussion:
UNSAT vs UNDETERMINED
(too old to reply)
Greg Sinclair
2004-02-06 08:01:03 UTC
Permalink
If a formula has clauses that are UNSAT and UNDETERMINED, does this make it
UNSAT or UNDETERMINED?

If a formula has SAT and UNDERTIMED, it is UNDETERMINED, correct?

Thanks,

Greg
Alexander Smith
2004-02-06 14:16:06 UTC
Permalink
The lab handout is very clear on this. Read the three sentences under
checkAssignment() in section 3.4:
1) This function returns SAT if *all* clauses in solver are satisfied.
2) It returns UNSAT if *any* clause is unsatisfied.
3) Otherwise it returns UNDETERMINED.
Post by Greg Sinclair
If a formula has clauses that are UNSAT and UNDETERMINED, does this make it
UNSAT or UNDETERMINED?
If *any* clause is UNSAT, then which case applies?
Post by Greg Sinclair
If a formula has SAT and UNDERTIMED, it is UNDETERMINED, correct?
If NOT all clauses are SAT, and NO clauses are UNSAT, then which case
applies?
Post by Greg Sinclair
Thanks,
Greg
Alexander
Sherman
2004-02-07 06:54:11 UTC
Permalink
I thought everyone who is having C second semester must have taken digital
systems first term. I guess I was wrong. ^^"
Post by Alexander Smith
The lab handout is very clear on this. Read the three sentences under
1) This function returns SAT if *all* clauses in solver are satisfied.
2) It returns UNSAT if *any* clause is unsatisfied.
3) Otherwise it returns UNDETERMINED.
Post by Greg Sinclair
If a formula has clauses that are UNSAT and UNDETERMINED, does this make it
UNSAT or UNDETERMINED?
If *any* clause is UNSAT, then which case applies?
Post by Greg Sinclair
If a formula has SAT and UNDERTIMED, it is UNDETERMINED, correct?
If NOT all clauses are SAT, and NO clauses are UNSAT, then which case
applies?
Post by Greg Sinclair
Thanks,
Greg
Alexander
Loading...