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.

Answer 1

If I understand correctly (and I might not), it sounds like maybe the property you are trying to prove is

$$\forall G . C_1(G) \implies (\exists x . C_2(G,x) \land C_3(G,x))$$

where $G$ ranges over all graphs and $x$ ranges over all possible assignments to the program variables.

If that's right, then you can't check this with SAT or with CBMC. It's a second-order formula, so you need a 2QBF solver to check it. SAT can help you check properties of the form "$\forall x . F(x)$" and properties of the form "$\exists x . F(x)$", but for properties of the form "$\forall x . \exists y . F(x,y)$" or "$\exists x . \forall y . F(x,y)$", you need 2QBF (or, more generally, QBF). There do exist 2QBF solvers, but checking 2QBF properties is much harder than checking SAT.

An additional complication is that it sounds like you want to quantify over all graphs of all sizes.

It sounds like you want to verify the following property: for all graphs, if C1 is true, then C2 and C3 are true.

The standard approach is to use assume and assert statements. You first write some assume statements that capture the assumption that the input graph satisfies C1. You then write some assert statements that capture the requirement that the C2 and C3 had better be true. The model checker checks whether there are any inputs that satisfy all the assume statements, and make at least one of the assertions false.

If you were going to use a SAT solver, you would search for a counterexample by writing a boolean formula C1 && not(C2 and C3), then asking the SAT solver to find a satisfying assignment for that formula. If it finds one, that it has found a counterexample to your property. If the formula is unsatisfiable, then your property holds. This all assumes that you are reasoning about graphs of a fixed size.

If the graph is of arbitrary size, then the problem is much harder. That falls beyond SAT and beyond even QBF, as both SAT and QBF relate to formulas with a fixed (constant) number of boolean variables -- but if you want to reason about arbitrary-sized graphs, there is no encoding of that into a fixed number of boolean variables. A standard heuristic is to check the property on graphs of size N for a few small values of N (say, for N=1,2,3,4,5,6,... until you run out of patience or the solver starts taking too long).