HM0880 commented 2 years ago

Is there a way to update the clause database to solve ALLSAT? My current approach is to add a blocking clause to the solver and then re-run the solver. The re-running approach is fine for small formulas, but I would like to use a more efficient technique for larger formulas.

def solve(solver_name, solver, formula):
    """Given a solver name, a PySAT solver object [1], and the SAT
    formula itself, find all satisfying assignments of the formula.

    PySAT's `solve' routine returns True when the formula can be
    satisfied [2].

    [1] https://pysathq.github.io/docs/html/api/solvers.html
    [2] https://pysathq.github.io/docs/html/api/solvers.html#pysat.solvers.Solver.solve

    """
    # Add the clauses to the chosen solver
    for line in formula:
        if isinstance(line, list):
            solver.add_clause(line[:-1])  # remove clause-terminating 0 for PySAT

    # Add blocking clauses to solve ALLSAT
    solve_status = True  # initialize
    idx = 0
    start = datetime.datetime.now()
    while solve_status:
        solve_status = solver.solve()  # try to solve again
        if solve_status:
            model = solver.get_model()  # "model" = current satisfying assignment
            solver.add_clause([-1 * x for x in model])  # add blocking clause
            idx += 1  # increment
        else:
            stop = datetime.datetime.now()
            print(
                f"solver, {solver_name:14s}, solutions found, {idx:4d}, total time (seconds), {stop-start}"
            )

alexeyignatiev commented 2 years ago

What kind of formula update do you mean? Presumably, it is different from adding more clauses. Does it mean you want to remove clauses too?

HM0880 commented 2 years ago

Answers to questions

What kind of formula update do you mean? Presumably, it is different from adding more clauses.

I want to update the internal database with a blocking clause for every model of ϕ. I do not want to restart the solver from scratch every time I add a new blocking clause (see MWE below).

Does it mean you want to remove clauses too?

I do not want to remove clauses.

Minimal working example (MWE)

Consider the formula ϕ = (-x1 ∨ x2). I have written out each step of the “full solve” routine in the “Code” section. For this trivial formula, I call solver.solve four times; for my real formulas, I have millions of solutions, and I want to keep as much of the internal solver state as possible for each new solution of ϕ. In other words, I want to call solver.solve once, find a blocking clause, update the internal solver state, and solve again with the new information from the blocking clause.

Does this MWE clarify what I want to do and why I want to do it? Let me know if you need more clarification.

Code

import pysat

solver = pysat.solvers.Minisat22()  # make solver
solver.add_clause([-1, 2])  # add the formula ϕ = (-x1 ∨ x2)

# Full solve #1
solve_status = solver.solve()
model = solver.get_model()
print(f"ϕ is {solve_status}; the model is {model}")
solver.add_clause([-1 * x for x in model])  # add blocking clause

# Full solve #2
solve_status = solver.solve()
model = solver.get_model()
print(f"ϕ is {solve_status}; the model is {model}")
solver.add_clause([-1 * x for x in model])  # add blocking clause

# Full solve #3
solve_status = solver.solve()
model = solver.get_model()
print(f"ϕ is {solve_status}; the model is {model}")
solver.add_clause([-1 * x for x in model])  # add blocking clause

# Full solve #4
solve_status = solver.solve()
model = solver.get_model()
print(f"ϕ is {solve_status}; the model is {model}")

# We are done since we have solved ALLSAT for this ϕ.

Output

ϕ is True; the model is [-1, -2]
ϕ is True; the model is [-1, 2]
ϕ is True; the model is [1, 2]
ϕ is False; the model is None

haz commented 2 years ago

Why not use python-nnf if you want to enumerate all the models? You could push it through a knowledge compilation step to do it more efficiently than per-model no-good blocking.

alexeyignatiev commented 2 years ago

@HM0880, okay, I see what you mean. Your initial words on "updating the database" confused me, sorry.

What you want is basically warm restarts, i.e. when the solver finds a model, it then does not backtrack to level 0 undoing all the assignments but instead keeps its internal state and simply returns the model while the new call to solve starts at exactly the same point of the search space. Please confirm.

Although this is not difficult to implement in a SAT solver like MiniSat, this isn't currently supported by the solvers included in PySAT. I can mark this as an enhancement to be potentially implemented.

Having said that, I should mention that thanks to phase saving implemented in most modern SAT solvers, in some cases a new call to solve should not need to do much - it will try to restore the state following the phases saved. Although yes, restoring the assignments and doing propagation may cost a bit. Also, it may branch on different variables due to the updated activities, which may lead it to a different point.

HM0880 commented 2 years ago

@haz I don't know much about NNF. (Part of my efforts are for pedagogical reasons, so I am interested in CNF for teaching purposes.) Can python-nnf [1] also enumerate the solutions? From what I can tell, python-nnf can do #SAT, but I did not see support for enumeration.

[1] https://github.com/QuMuLab/python-nnf

haz commented 2 years ago

Yep: https://python-nnf.readthedocs.io/en/stable/nnf.html#nnf.NNF.models

Just use a knowledge compiler to put it into d-DNNF first.

HM0880 commented 2 years ago

@alexeyignatiev

okay, I see what you mean. Your initial words on “updating the database” confused me, sorry.

No problem. :)

What you want is basically warm restarts, i.e. when the solver finds a model, it then does not backtrack to level 0 undoing all the assignments but instead keeps its internal state and simply returns the model while the new call to solve starts at exactly the same point of the search space. Please confirm.

Yes, exactly. Thank you for the term warm restarts. (I would also like return the model that was found, but that is a detail.)

Although this is not difficult to implement in a SAT solver like MiniSat, this isn’t currently supported by the solvers included in PySAT. I can mark this as an enhancement to be potentially implemented.

Takahisa Toda has three ALLSAT solvers based on MiniSat [1] and a survey paper with Takehide Soh [2]. My question for PySAT is motivated by Toda’s work where I am interested in using different SAT solvers to solve ALLSAT by doing warm restarts.

Having said that, I should mention that thanks to phase saving implemented in most modern SAT solvers, in some cases a new call to solve should not need to do much - it will try to restore the state following the phases saved. Although yes, restoring the assignments and doing propagation may cost a bit.

Oh, this is very interesting. My concern is that with many solutions (~10e15), the cost of restoring and propagating may be too costly.

Also, it may branch on different variables due to the updated activities, which may lead it to a different point.

A different point (i.e., a different model) is fine since eventually we will find all the models, yes?

[1] https://www.disc.lab.uec.ac.jp/toda/code/allsat.html

[2] https://arxiv.org/abs/1510.00523

HM0880 commented 2 years ago

@haz Thanks! I will hopefully have some time to try NNF.

alexeyignatiev commented 2 years ago

@HM0880, thanks for the pointers. My colleagues and I also had a couple of enumerators based on warm restarts in MiniSat. So I should be able to add that - the only issue is time as always.

HM0880 commented 2 years ago

@alexeyignatiev Does a warm restart example already exist in PySAT? I'm pretty motivated to study ALLSAT for my own research, so I am interested in helping add an ALLSAT enhancement to PySAT.

alexeyignatiev commented 2 years ago

@HM0880, no, warm restarts aren't available in PySAT's solvers. What I meant is that it is relatively easy to implement in a MiniSat-based solver. For that, you only need a couple of "components" to make it work:

you need to have a Boolean flag to determine whether or not you are in the warm-start mode;
when the solver finds a model, you don't backtrack to level 0 if you are in the warm-start mode (you do if you are in the standard mode);
between warm starts, you need to add your blocking clause (just like you are doing it now) but you should implement a special clause adding method for that, which will determine the backtrack level k given the blocking clause (k should be equal to the second maximum level in the clause), such that the clause becomes asserting (in the sense of CDCL terminology); then the procedure should apply backtracking to level k followed by unit propagation of the "latest" literal in the blocking clause. This isn't really difficult. I can implement it when I get a chance. The problem is as always time... :(

HM0880 commented 2 years ago

no, warm restarts aren't available in PySAT's solvers.

Yes, I know, which is why I asked for an example. :)

The bullet points actually help a lot (sort of the example/workflow I wanted to see). The last bullet point has the details (e.g., backtrack level k) that I did not know.

(No promises, but I may have some time to try to implement the warm restart...)

alexeyignatiev commented 1 year ago

@HM0880, I added warm start mode to a bunch of MiniSat-based solvers in the latest version (0.1.7.dev22). So I am closing this issue for now. If you believe it needs more work, feel free to reopen.

HM0880 commented 1 year ago

Excellent; thank you! (Commit 450559f42b42a6627a60d032947b189d01c21a65 for future reference.)

pysathq / pysat

Solving ALLSAT #112

Answers to questions

Minimal working example (MWE)

Code

Output