CODEWITHSUNDEEP
satsatisfiabilitysat-solvers
red_house
red_house

Reputation: 63

Solving with multiple assumptions

Suppose I have a CNF expression with variables (a,b,c,d,e,f,g). How would I go about using a SAT solver to find an assignment for (d,e,f) given that {a,b,c,g} = {1,0,0,1} and {a,b,c,g} = {1,1,1,1}? If it was one assumption, calling a sat solver to find assignments for {d,e,f} would be straight-forward (E.g., by adding unit clauses to the CNF). But what if I have multiple assumptions? Is this possible?

Upvotes: 1

Views: 450

Answers (2)

Tim
Tim

Reputation: 1098

It is not quite clear if you want a practical answer or an interesting theoretical answer. I will go after practical.

For each set of assumptions, call a sat solver that supports solve with assumptions on that set of assumptions (example). Do this sequentially on the same solver instance.

Pros:

  • You do not mix satisfiability of mutually exclusive sets of assumptions. If set of assumptions A is sat for a formula F and the other set A' is unsat for F, each call to the solver tells you if those assumptions are sat/unsat.
  • Learned clauses from the first call may stick around for the second call. The intermediate learned clauses talk about the same variables. (Note: If you have a disjoint formula F & G where F is over variables X, G is over variables Y and X and Y share no variables, resolution -- the inference rule used in CDCL -- cannot derive clauses mixing F and G. There is no obvious gain of mixing the two together instead of splitting them apart unless one instance is much easier to prove unsat and stop early.)

Cons:

  • If instance A is hard to solve in practice but A' is trivial, you might get stuck on A.
  • It is not parallel so if you have way more instances than two that you want to solve ASAP you'll need additional mechanisms.

I know this is a bit of an obvious answer, but it is worth trying. If that fails, you can try doing fancier things like solving w.r.t. the assumptions A union A', and only if that is unsat solving falling back on this strategy of A then A'. This won't help for your example as (a,b,c,g) = (1,0,0,1) and (a,b,c,g) = (1,1,1,1) are mutually exclusive.

Upvotes: 0

Kyle Jones
Kyle Jones

Reputation: 5532

Here are the steps for what (I think) harold was trying to describe to you. You have some CNF formula F over the variables a, b, c, d, e, f and g.

  1. Duplicate the formula, calling the duplicate G.
  2. In G, replace the variable a with aa, b with bb, c with cc, and g with gg.
  3. Add unit clauses to F so that (a,b,c,g) = (1,0,0,1).
  4. Add unit clauses to G so that (aa,bb,cc,gg) = (1,1,1,1).
  5. Concatenate the formulas F and G and feed the result into the SAT solver.

The solver will find a satisfying assignment consistent with both (a,b,c,g)'s and (aa,bb,cc,gg)'s preset values.

Upvotes: 4

Related Questions