Formal specification; Logical formula

Question

* Initial Question *

I'm trying to write a logical formula consists of three Boolean variable C1, C2, C3.

My program takes graph as input and checks properties about them. C1 represents presence of some structural properties of the input graph (graph being strongly connected). If graph have this property, variable C1 is True else its False.

Variable C2 and C3 represent another set of properties involving other program variables.

The property i'm interested is

If graph have this desired structural property then there is an assignment to program variables that makes C2 & C3 True.

For checking one specific graph i can just say:

SAT (C1 && C2 && C3)

And if there is a satisfying assignment i'm done.

But rather than checking properties of specific graph i'm interested in checking for every graph which have this structural property (represented by C1) also have other properties too (represented by C2,C3).

So I represent graph as arbitrary two dimensional array of size N. So that i can allow my program to iterate over any graph of size N.

Bool Graph[N][N]

• I'm using CBMC (C Bounded Model checker) to write and check program.

I want to write this.

For_all Graph[N][N] s.t C1 $\implies$ There_exists(an assignment) s.t C2 && C3

I'm not sure how to can i write this property? Any help in this regard?

Updated Question : To make question clear as after an answer i thought i was unable to put my point clear.

In my program i'm taking graph as input. based on this graph i'm trying to make connection that if the graph have some structural property then it has other properties also.

The structural property is: graph being strongly connected. Other properties are based on the label of edges and nodes. So to generalize, other properties depend on program variable x,y,z,.. and Boolean function f.

I can build this program by using a Boolean variable B1 to inspect whether graph is strongly connected or not, if its is B1 is True, otherwise False. and use other Boolean variable B2 and B3 to represent other properties. Hence both B1 and B2, B3 depend on graph and B2, B3 also depend on other variables x,y,z,... and Boolean function f.

To check for a single graph i can ask:

SAT (B1 and B2 and B3). if there is an assignment i'm :)

Problem arise when i'm interested not in a particular graph but in every graph (certain fixed size N). Worst possible try is to generate all graphs of certain size and check each one by one and make sure that its the case.

The thing i'm trying to achieve is something like this :

For_all graphs G s.t B1 -> There_exist an assignment to (x,y.., f) s.t B2 and B3.

Edited

I want to iterate over all graphs (which i can do making graph arbitrary)

unsigned int Graph[N][N];  // For some specified N

but with that i'm looking to check whether there exists an assignment that makes other property works. If other property were VALID(tautologous) or Contradiction i could have checked easily. But other properties(represented by C2 , C3) are not either a Valid or a contradiction. For example with SAT (C1 && C2 && C3) and SAT (C1 && !(C2 && C3)) both have a witness.

I'm interested in iterating and checking that there exists at least one possible assignment for each graph that makes C1 && C2 && C3 true.