I have a set of propositional clauses generated by clausification of a set of first-order logic axioms containing 2 binary predicates (p and c). Assume P is the number of distinct predicates in the axiomatization (P = 2).
$[-p(x,y) ∨ -p(y,x) ∨ (y = x)] ∧ [-c(x,z_3) ∨ c(x,z_1)] ∧ [c(x,z_3) ∨ c(x,z_2)]$
Now this statement has 2 clauses with 3 variables (V3 = 2), 1 clause with 2 variables(V2 = 1). Suppose I have a set of ten distinct individuals in my dataset (i.e. domain size, I=10), and I want to instantiate my clauses with these ten objects and also place a constraint that there are exactly 20 instantiations for each of the binary predicates (p and c) using the ten data individuals. I'd like to now calculate the number of clauses and variables that would be generated in my resulting SAT problem. These are the formulas I am using.
variables = ((20**P*)*I^2) = 4000
clauses = ((20*V3)* I^3) + ((20*V2)*I^2) = 42000
Since I am new to SAT, I would like to make sure that I am making the right assumptions or formulas in making my calculations.