How to use aiger and pysat together

[bbc2]

Looking at the documentation at https://pysathq.github.io/docs/html/api/formula.html#pysat.formula.CNF.from_aiger mentioned in other issues in this repository, I thought I'd be able to use the aiger library to help me solve non-CNF formulas. Unfortunately, I couldn't get the expected result. Either there's a huge bug in one of these libraries, or I'm not using them correctly (which is much more likely :)).

Here's my sample program:

import aiger
from pysat.formula import CNF
from pysat.solvers import Glucose3

x = aiger.atom("x")
expr = x & ~x
cnf = CNF(from_aiger=expr)
print("Map:", [(v, cnf.vpool.obj(v)) for v in cnf.inps])

solver = Glucose3(bootstrap_with=cnf.clauses)
solver.solve()
print("Solution:", solver.get_model())

Expected output:

Map: [(1, Input(name='x'))]
Solution: None

Actual output:

Map: [(1, Input(name='x'))]
Solution: [-1, -2]

Do you know why I get this result? Sorry if I'm doing something stupid. I'm a complete noob in SAT solving.

I used the following versions:

• CPython: 3.10.1
• python-sat: 0.1.7.dev15
• py-aiger: 6.1.20
• py-aiger-cnf: 5.0.4

[alexeyignatiev]

Hi @bbc2,

You are doing almost everything correctly. One comment to make is that if you want to check satisfiability of your non-clausal formula, you should enforce the outputs of the expression. These are stored in cnf.outs. So if you make an oracle call like this solver.solve(assumptions=cnf.outs), then you should get the correct output False.

(Note that instead of using assumptions, you may want to add a unit clause to the solver for each of the outputs of cnf.outs.)

Hope this helps, Alexey

[bbc2]

Hi, and thank you very much for the advice, this now works well! I feel a little dumb for not having understood the difference between a formula and a circuit at first, but this makes a lot more sense to me now.

(Note that instead of using assumptions, you may want to add a unit clause to the solver for each of the outputs of cnf.outs.)

That's an interesting alternative. I noted that it was necessary if I wanted to enumerate solutions with solver.enum_models() instead of just getting the first one found by the solver (with solver.get_model()). Somehow, enum_models doesn't do what I expect if I use solve with the assumptions argument: it can return invalid solutions.

[alexeyignatiev]

Somehow, enum_models doesn't do what I expect if I use solve with the assumptions argument: it can return invalid solutions.

Well, in principle model enumeration should work exactly the same way. Note that solver.enum_models() can also handle a list of used-defined assumptions. However, in the case of circuits, model enumeration may indeed enumerate more "models" because of the auxiliary Tseitin variables encoding the gates. By default, at each iteration, the method gets a complete model (on all variables) and blocks it. To ensure that model enumeration works properly for circuits, you should additionally block the part of the model that corresponds to the input variables only.