I am very new to SAT and Z3 (Have not even started with SMT yet). I have been playing around with gophersat (A nice Go implementation which works for a good set of SAT problems) and I discovered DIMACS format there. Although I agree that it is not the best way to work with variables, but for some simple testing I found it pretty handy. I tried to check if there is a direct way to read, parse, and construct a SAT formula from a DIMACS file in Z3. I didn't find any (as mentioned, I am very new, so I may not know the existence of one). So I ended up coding the following. I would like to know what people think about it and whether there is a better way to achieve the same.
(N.B.: I have not put any checks on the number of clauses and/or number of variables for the formula)
from z3 import *
def read_dimacs_and_make_SAT_formula(file_name: str):
vars = dict()
base_name = "x"
with open(file_name, "r") as f:
for idx, line in enumerate(f):
if line.strip() != "\n" and line.strip() != "" and line.strip() != "\r" and line.strip() != None and idx > 0:
splitted_vals = line.split()
for element in splitted_vals:
if int(element) != 0:
if int(element) > 0 and vars.get(element) is None:
# pure variable which never seen
vars[element] = Bool(base_name+element)
elif int(element) > 0 and vars.get("-"+element) is not None:
# pure variable we have seen the negetion before.
vars[element] = Not(vars["-"+element])
elif int(element) < 0 and vars.get("-"+element) is None:
# negetion of a variable and we have not seen it before.
vars[element] = Not(Bool(base_name+element.replace("-", "")))
elif int(element) < 0 and vars.get(element.replace("-", "")) is not None:
# Negetion, we have seen the pure variable before.
vars[element] = Not(vars[element.replace("-", "")])
f.seek(0)
disjunctions = []
for idx, line in enumerate(f):
clauses = []
if line.strip() != "\n" and line.strip() != "" and line.strip() != "\r" and line.strip() != None and idx > 0:
splitted_vals = line.split()
for element in splitted_vals:
if int(element) != 0:
clauses.append(vars[element])
disjunctions.append(Or([*clauses]))
# print(disjunctions)
if disjunctions:
return And([*disjunctions])
return None
The way you use it is simple. Like so -
if __name__== "__main__":
s = Solver()
disjunctions = read_dimacs_and_make_SAT_formula("dimacs_files/empty.cnf")
if disjunctions is not None:
s.add(disjunctions)
print(s.check())
if s.check().r != -1:
print(s.model())
If called that way, the result looks like the following
python test_1.py ✔ │ SAT Py
sat
[x3 = False, x2 = True, x1 = True, x4 = False]
So the question is, again, what do you think? And can I do something else? Is there a better way?
Thanks in advance
Note that code reviews are usually off-topic for stack-overflow. There's a dedicated stack-exchange website (https://codereview.stackexchange.com) for such purposes. You might get better feedback on your program there.
Having said that, z3 supports DIMACS format out-of-the-box, so you don't really need to program it. Here's an example. Say we have the file a.dimacs:
c simple_v3_c2.cnf
c
p cnf 3 2
1 -3 0
2 3 -1 0
You can directly feed this to z3:
$ z3 a.dimacs
s SATISFIABLE
v -1 -2 -3
Or, if you want to use the Python API, you can write:
from z3 import *
s = Solver()
s.from_file("a.dimacs")
print(s)
print(s.check())
print(s.model())
which prints:
[Or(k!1, Not(k!3)), Or(Not(k!1), k!2, k!3)]
sat
[k!1 = False, k!3 = False, k!2 = False]
Note that the file extension has to be dimacs, so z3 will use the correct parser internally when you call s.from_file. From the command line, you can either use the .dimacs extension, or pass the command line option -dimacs to z3.