In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula.

We can see that some graph problems such as the coloring problem and the problem of finding k-cliques can be transformed into SAT problem.  I am not familiar with how maple uses the sat solver. I am trying to use maple to solve the following game for a solution. The game is a good choice for understanding the SAT.

• http://www.cril.univ-artois.fr/~roussel/satgame/satgame.php?level=1&lang=eng

The game is won when at least one cell on each line is green. 

Clicking on a number will color each cell with the same number in green, and each cell with the opposite number in red. 

For example:

If we choose ``1" as green(i.e. be chosen), then -1 is red (not be chosen) in any cell.  I guss that the maple function Satisfy can do it. 

That is, we are looking for a set of solutions such that at least one number in any line is selected as green. 

Here is a solution for winning this game:

How to use the SAT solver Satisfy in maple to find a solution from a sat game?

I open the command-line of maple 2022, and I can run the code alone. But when I save it in a text named ``6conn.txt", I don't know how to run it.

with(GraphTheory):
g:=Graph({{0 ,1},{3 ,4},{4 ,1},{1 ,3},{3 ,0},{0 ,4},
{2 ,1},{4 ,5},{4 ,2},{3 ,6},{4 ,6},{6 ,5},{1 ,6},{6 ,2},
{5 ,0},{0 ,2},{2 ,5},{7 ,8},{12 ,10},{10 ,11},{11 ,8},{8 ,10},
{10 ,7},{7 ,11},{9 ,8},{11 ,12},{11 ,9},{10 ,13},
{11 ,13},{13 ,12},{8 ,13},{13 ,9},{12 ,7},{7 ,9},{9 ,12},
{8 ,2},{13 ,0},{10 ,5},{12 ,3},{1 ,9},{7 ,6}
});

I tried  .\E:\\6conn.txt or !E:\\6conn.txt. Neither seems to work.

6conn.txt

It is easy to simplify the following expression (to 4), but maple's ceil function does not seem to be interested in simplifying it.

where n is greater than or equal to 4. 

simplify(ceil((3*n-8)/(n-3))) assuming n>=4, n::positive # As-is output

We have to rewrite "(3*n-8)/(n-3)" in this form "3 + 1/(n - 3)" to recognize.

simplify(ceil(3 + 1/(n - 3))) assuming  n>=4, n::positive

4

• My first question is: How to transform (3*n-8)/(n-3) into 3 + 1/(n - 3) by maple?
• My second question: Can we see the steps of execution of the simplification involving  ceil)?

I have an expression and I want to find its maximum value.

expr:=sin(sqrt(3)*t)*cos(sqrt(3)*t)*(sqrt(3)*cos(sqrt(3)*t) - sin(sqrt(3)*t))/3

It is easy to find its maximum value in a numerical form.

Optimization:-Maximize(sin(sqrt(3)*t)*cos(sqrt(3)*t)*(sqrt(3)*cos(sqrt(3)*t) - sin(sqrt(3)*t))/3)

[0.324263244248023330, [t = 1.39084587050767]]

The images of the expression is as follows.

But does it exist an acceptable maximum value in symbolic form?  As the function maximize seems to take a lot of time, I don't see any hope so far. Perhaps the expression is indeed complex.

maximize(expr)# it runs long time.

We try to find the derivative of expr and get some points where thier derivatives are 0.

s:=[solve(diff(expr,t),t)]
evalf~(s) # Some solutions seem to have been left out.

[0.7607468963 + 0.*I, -0.4229534936 - 0.*I, 0.2668063857 + 0.*I]

ex:=convert(expr,exp):
s:=[solve(diff(ex,t)=0,t)]:
s1:=evalf~(s);# choose the 6th item: 1.390845877 + (4.655829150*10^(-9))*I
fexpr := unapply(ex, t);
evalf(fexpr(s1[6]));
fexpr (s[6]); # a very long expression that is not quite acceptable.

-I/6*(-sqrt(-(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3)*((1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(2/3)*sqrt(3)*I - 2*I*sqrt(3)*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3) + (1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(2/3) + 36*I*sqrt(3) + 2*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3) - 44))/(6*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3)) + 6*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3)/sqrt(-(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3)*((1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(2/3)*sqrt(3)*I - 2*I*sqrt(3)*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3) + (1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(2/3) + 36*I*sqrt(3) + 2*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3) - 44)))*(-sqrt(-(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3)*((1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(2/3)*sqrt(3)*I - 2*I*sqrt(3)*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3) + (1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(2/3) + 36*I*sqrt(3) + 2*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3) - 44))/(12*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3)) - 3*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3)/sqrt(-(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3)*((1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(2/3)*sqrt(3)*I - 2*I*sqrt(3)*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3) + (1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(2/3) + 36*I*sqrt(3) + 2*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3) - 44)))*(sqrt(3)*(-sqrt(-(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3)*((1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(2/3)*sqrt(3)*I - 2*I*sqrt(3)*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3) + (1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(2/3) + 36*I*sqrt(3) + 2*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3) - 44))/(12*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3)) - 3*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3)/sqrt(-(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3)*((1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(2/3)*sqrt(3)*I - 2*I*sqrt(3)*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3) + (1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(2/3) + 36*I*sqrt(3) + 2*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3) - 44))) + (-sqrt(-(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3)*((1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(2/3)*sqrt(3)*I - 2*I*sqrt(3)*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3) + (1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(2/3) + 36*I*sqrt(3) + 2*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3) - 44))/(6*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3)) + 6*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3)/sqrt(-(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3)*((1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(2/3)*sqrt(3)*I - 2*I*sqrt(3)*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3) + (1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(2/3) + 36*I*sqrt(3) + 2*(1404*I*sqrt(3) - 1396 + 36*sqrt(-3018 - 3018*I*sqrt(3)))^(1/3) - 44)))*I/2)

An interesting problem is that an acceptably concise expression (although it is very subjective) for the maximum value may not exist mathematically. But knowing this in advance is difficult.

Download compute_zlc.mw

The edge connectivity of a connected graph G  is the minimum number of edges whose deletion from the graph G disconnects G. Below we are concerned with a particular kind of edge-cut.

• For a connected graph G=(V ,E), an edge set S ⊂ E is a restricted-edge-cut, if G−S is disconnected and every connected component of  G−S has at least 2 vertices. 

Clearly, a restricted-edge-cut is an edge cut with a special requirement.

• The restricted-edge-connectivity of G, denoted by κres(G), is defined as the cardinality of a minimum restricted-edge-cut.

For example, a graph g is as follows.

Clearly, its edge-connectivity is 1 since (0,3) or (0,4) is a edge cut of g. But we can find that  if we remove the edge (0,3), then "3" is a isolated vertex. Similarly, "4" is a isolated vertex if we remove  (0,4). It is not difficult to find g has exactly the two cut-edges (0,3) and (0,4).

Based on the definition of the restricted-edge-cuts, neither {(0,3)} nor  {(0,4)} are restricted-edge-cuts.  A minimum restricted-edge-cut is {(0,1),(0,2)} since every connected component of G-{(0,1),(0,2)} has  (at least) 2 vertices.

So  κres(g) is 2.  My problem is:

Given a graph G, how to calculate the restricted-edge-connectivity of  G?  Moreover, how to find a minimum restricted-edge-cut? 

A specific graph that I want to test is as follows. (it has 16 vertices and 56 edges.) I would like to calculate its restricted-edge-connectivity and find a minimum restricted-edge-cut. 

g:=ConvertGraph("O~tIID@wL~j`PbOqgLJ@p");
DrawGraph(g, stylesheet=[vertexborder=false,vertexpadding=15,edgecolor = "Black",
     vertexcolor="Black",edgethickness=2])

EdgeConnectivity(g) 

6

One option I came up with is to find all 6-edge subsets first. Test if they satisfy  the restricted condition (one by one). Then continue to increase to 7 or more. But this violent calculation may get stuck in the first step. That is, test all the minimum edge cut sets (Note that we will consider 32468436 edge-subsets!) I was referring to the efficiency aspect.  

with(Iterator):
C:=Combination(58,6):
K:=Edges(g):
#sub:=seq( K[[seq(c[]+1)]], c=C); # do not run this code since it has 32468436 members.

Any language is acceptable.( C or C++, Python. )

PS: Some time ago, I also asked a related question (but with some differences) on mathematica stack （Find all the minimum edge cuts of a graph）. Although Bob Hanlon  gave a reply, the actual result is not good.

Edits: The following literature gives a polynomial algorithm for computing the restricted-edge-connectivity of a given  graph. The heart of it is to computing the least cardinality of some  edge-pairs's edge separator. I'm stuck here.

• Esfahanian A H, Hakimi S L. On computing a conditional edge-connectivity of a graph[J]. Information processing letters, 1988, 27(4): 195-199.

How to implement this algorithm is my current concern.