Empty Clauses and Formulas

[Chris Brelski]

In Lab2 a formula with all empty clauses was considered SAT; any empty
clause was considered SAT as well.
So, in case of empty clauses, my program treats each as always SAT and
finds assignments for the rest of the formula. In the case of a blank
formula it returns SAT immediately with no assignments.
Is this the desired correct behaviour ? Should any of these cases be
treated as invalid?

[Alexander Smith]

Any CNF formula that was valid in lab 2 should still be considered valid
in lab 3. Empty clauses are automatically satisfied. So is an empty
formula. If a formula is satisfiable, your program should return a
satisfying assignment. In the case of an empty formula, ANY assignment is
a satisfying assignment, including one with all X's. It would also be ok
in this case to return an assignment vector which is all 0's, or any
combination of 0's and 1's, since the formula is satisfied under all those
assignments. Basically, if your satsolve program returns SAT, then you
should be able to give that vector along with the formula to satverify
from the lab 2 reference solution, and it should also say SAT.

Alexander

Post by Chris Brelski
In Lab2 a formula with all empty clauses was considered SAT; any empty
clause was considered SAT as well.
So, in case of empty clauses, my program treats each as always SAT and
finds assignments for the rest of the formula. In the case of a blank
formula it returns SAT immediately with no assignments.
Is this the desired correct behaviour ? Should any of these cases be
treated as invalid?

[Sheena Lynch]

if the input file reads:
p cnf 0 0

is it correct to have it just output SAT
without any assignments? (i.e. 1101)

[Alexander Smith]

Yes. If you have no variables, then, technically, your assignment vector
is 0 characters long. In this case, the main() function you're given will
print out SAT followed by a blank line.

Alexander

Post by Sheena Lynch
p cnf 0 0
is it correct to have it just output SAT
without any assignments? (i.e. 1101)