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.

  1. variables = ((20**P*)*I^2) = 4000

  2. 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.


closed as off-topic by D.W., Emil Jeřábek, Aryeh, Gamow, Hsien-Chih Chang 張顯之 Mar 19 at 17:23

This question appears to be off-topic. The users who voted to close gave this specific reason:

  • "Your question does not appear to be a research-level question in theoretical computer science. For more information about the scope, please see help center. Your question might be suitable for Computer Science which has a broader scope." – D.W., Emil Jeřábek, Aryeh, Gamow, Hsien-Chih Chang 張顯之
If this question can be reworded to fit the rules in the help center, please edit the question.