Doubt about the paper first equation

[ebonetti]

Hello folks at CMU Locus Lab! :)
You have some great repositories, currently I use your TCN net and this one seems quite intriguing too. Reading your paper I stumbled upon the first equation
maximize ∑_j V_i 1{s_ij * v_i > 0} and I couldn't quite figure it out: lets say a certain clause is verified one variable and falsified for all the others, the clause should be falsified, but in your equation it's not.

Why not use instead maximize ∑_j ∧_i 1{s_ij * v_i >= 0} ?
(Using logical conjunction instead of disjunction; equality needed for the s_ij=0 cases)

Keep up the great work,
Enrico Bonetti Vieno

P.S.: the notation 1{...} is a step function over a boolean value: 1 if true, 0 otherwise - right?

[priyald17]

Thank you for your interest in the paper! Since we are viewing SAT problems as a conjunction of disjunctions (i.e. we are using conjunctive normal form), we allow a clause to be true/verified if at least one variable within it is true/verified. As a result, in the case you mention (where one variable in a clause is true/verified and the others are all false/falsified), the clause should be true, as is reflected in our formula.

Your understanding of the notation 1{...} is correct!

[ebonetti]

Thanks for the detailed reply!