CODEWITHSUNDEEP
pythongraphsatsat-solvers
sk0gen
sk0gen

Reputation: 1

Convert Vertex-Total-Magic-Labeling Problem to SAT

Me and my friends receive the problem from title to resolve.

We found nice and easy to use SAT Solver Cryptominisat.

We also found kinda long article about converting VTML to Sat Article. We will generate rules/restrictions from python.

We actually found obstacles with converting whole Graph to Boolean Rules. We also 

c 2 na poczatku to jest Y
c 1 na początku to jest X
p cnf 188 5
c i = 1
-111 21 0
111 -21 0
c i = 2
22 -112 0
22 -21 0
-22 112 21 0
c i = 3
23 -113 0
23 -22 0
-23 113 22 0
c i = 4
24 -114 0
24 -23 0
-24 114 23 0
c i = 5
25 -115 0
25 -24 0
-25 115 24 0
c i = 6
26 -116 0
26 -25 0
-26 116 25 0
c jezeli jedno jest true to reszta nie
-21 112 0
-22 113 0
-23 114 0
-24 115 0
-25 116 0
26 0

According to article I wrote that cnf clausules by hand. 2 at the beginning is Y ,

1 is X X1,1 -> 111

Upvotes: -1

Views: 50

Answers (1)

Kyle Jones
Kyle Jones

Reputation: 5532

  1. The p line declares 188 variables and 5 clauses when there are only 12 active variables and 23 clauses.

  2. SAT solvers generally expect variables to be numbered from 1 to N with all variables between 1 and N inclusive appearing at least once in a clause, rather than being randomly numbered with large blocks of unused identifiers. The solver will probably work anyway, but use more memory than is necessary.

  3. Comments should not appear after the p line.

Other than those complaints you do have a SAT instance which when fed to a SAT solver will produce a result. I don't know anything about vertex total magic labeling so I can't say whether you've encoded the actual problem correctly.

Upvotes: 0

Related Questions