2
$\begingroup$

I'm trying to solve a constraint programming problem using a SAT solver. I have set of constraints in the form of propositional logic statements, which are converted to CNF using Tseitin transformation. A number of inputs are fixed and pretty large - up to ~30k. A number of constraints can be ~200k.

Right now, I have to choose between several constraint candidates which will be added to the CNF formula. All of them have some quality parameter - basically, a candidate should not remove too many feasible solutions from a search space. I can choose between smaller rules (a few boolean operators like AND, OR and no more than 10 inputs), but it is just impossible for the larger constraints (dozens of operators and ~100 inputs), there is no way to predict the quality of solution in that case. So, I ended up with the idea of a tool, which will automatically choose the best option for me.

For example, I have the basic rule: $$\neg(A \wedge B \wedge(C \vee D \vee E))1)$$ For this rules, I have two corresponding additional rules and I have to choose one of them: $$\neg(A \wedge B) \wedge blah2)$$ $$\neg (C \vee D \vee E) \wedge blah3)$$ The (2) formula is the best for me - it removes lesser number of solutions. blah is not relevant to my question, but it always appears inside candidates.

What I have tried already:

  1. Use Espresso logic minimization tool. I input all candidates at ones and hope to get the minimal representation. It kind of works, but the tool ignores a quality metric - the result is too constraining for my problem. Too many possible solutions are prohibited. In addition, my problem is far too big for Espresso and I have to use it in incremental manner. I assume that is an issue too - Espresso does not see the whole picture at ones.
  2. SAT solvers or model counting. The idea is the following - estimate a number of possible solutions under some basic constraints. I can add one of the candidates, estimate a number of possible solutions again, remove it and run such a procedure for each candidate. Eventually, I can choose one with the largest number of legal solutions. It seems to be working, however, it is too slow with real cases - exact counter freezes forever, approximate counter concludes that there are infinite number of solutions.

I would like to brainstorm that problem - maybe someone can propose interesting formulation/approaches for this task? May it can be formulated as ILP task somehow?

UPDATE: I am given a geometry problem - i have a rectangular tile that should be filled with a set of various objects. Some configurations of objects are prohibited (it does not matter why). Each rule is populated in every applicable point of a tile: enter image description here $$\psi = \neg (A_1 \wedge B_1 \wedge C_1) \wedge \neg (A_2 \wedge B_2 \wedge C_2)$$

Blue bold lines are tile's borders. Such configuration of objects is prohibited: $$ \neg (A \wedge B \wedge C) 4)$$ This fact is represented as a set of clauses. $\psi$ forms a SAT task. You can think of it like "SAT, find me a tile which does not have any of these prohibited configurations". And this is my core formula. The same rule in different points of tile forms an identical set of clauses, but over different variables, e.g. $A_1, B_1, C_1$ and $A_2, B_2, C_2$ in the formula above - one rule forbids a set of 3 objects in 2 different points.

At the same time, such rules can be partially outside a tile (pay attention to the right side border). The object outside is transparent: enter image description here

This is prohibited too. The issue is that SAT solver does not know anything about world outside a tile, there is literally nothing out there. However, I still need to capture such configurations. I take each core rule and split it with boundary: enter image description here $$\neg(A \wedge boundary) 5)$$ $$\neg(A \wedge C \wedge boundary) 6)$$

Over the whole tile it looks like this: enter image description here

If we choose 5) rule, we will prohibit all obects $A$ near the boundary: $$\psi = \neg (A_1 \wedge boundary) \wedge \neg (A_2 \wedge boundary) \wedge \neg (A_3 \wedge boundary) \wedge \neg (A_4 \wedge boundary)$$

However, we can choose 6) rule: $$\psi = \neg (A_1 \wedge A_2 \wedge boundary) \wedge \neg (A_2 \wedge A_3 \wedge boundary) \wedge \neg (A_3 \wedge A_4 \wedge boundary)$$ This option is much better - it prohibits 2) rule near the boundary already and at the same time it allows to place single $A$ object near the boundary.

My questions:

  1. How can I choose between various candidates?
  2. Which tools can me help? #SAT, MaxSAT, MIP?
  3. Which metric can I use to optimise a set of rules?
$\endgroup$
  • $\begingroup$ this could be explained better/ more formally. (acknowledge its not a simple problem & not easy to describe.) "I have to choose between several constraint candidates which will be added to the CNF formula." can you be more specific? are you saying that these are different clause constraints added? is the "quality" parameter an assignment to boolean variables? etc. sometimes brainstorming goes on in Computer Science Chat. sometimes just clearly explaining the problem can be more than half the battle. $\endgroup$ – vzn Apr 20 '15 at 15:14
  • $\begingroup$ @vzn Sorry for inconvinience. "Quality" parameter is not represented anyhow in clauses themselves, it is some metric for user (me) to choose between several options. And yes, I have to choose one set of clauses from several to add it into a whole problem. I will add geometrical representation to my original post in several hours. $\endgroup$ – CaptainTrunky Apr 20 '15 at 16:04
  • $\begingroup$ I can't quite understand the problem. It sounds like we are given a core formula $\Phi$, a set of candidate formulas $\Psi_1,\dots,\Psi_k$, and a "quality" number for each candidate formula; the goal is to choose one candidate $\Psi_i$ so that $\Phi \land \Psi_i$ is satisfiable and the "quality" of $\Psi_i$ is as large as possible. Is that right? Or do you want to choose a subset of candidates so the conjunction is satisfiable? If so, how do you want to combine the qualities? Maximize the sum the qualities of the selected candidates? Have you looked at (weighted) MAX-SAT? $\endgroup$ – D.W. Apr 22 '15 at 0:04
  • $\begingroup$ Regarding #SAT, you might find this useful: cs.stackexchange.com/q/8952/755 (and maybe cs.stackexchange.com/q/33819/755). $\endgroup$ – D.W. Apr 22 '15 at 0:11
  • $\begingroup$ @D.W. You are absolutely right. I am given some core formula and I would like to add some additional formulas (set of clauses) to it. Each candidate has some quality number assigned to it, for example, a number of possible solutions for the candidate. I want to choose several candidates with the highest quality so the core formula will be satisfiable. And, finally, I didn't check MAXSAT, it is a great idea. Thanks! $\endgroup$ – CaptainTrunky Apr 22 '15 at 7:13
2
$\begingroup$

It appears that your problem is the following:

Input: boolean formulas $\Phi,\Psi_1,\dots,\Psi_k$
Output: a set $S \subseteq \{1,\dots,k\}$ whose size is as large as possible, such that $\Phi \land \land_{i \in S} \Psi_i$ is satisfiable

This problem can be formulated as an instance of MAX-SAT, specifically PMAX-SAT, and then solved using a MAX-SAT solver.

In particular, introduce boolean variables $t_1,\dots,t_k$. Define the formula $\Gamma$ to be the result of converting

$$\Phi \land \bigwedge_i (t_i \implies \Psi_i)$$

to CNF form. Now create the conjunction $\Gamma \land t_1 \land \dots \land t_k$, and ask the solver to choose a subset of the clauses $t_1 \land \dots \land t_k$ that makes conjunction satisfiable. (You mark the clauses of $\Gamma$ as required and ask it to find a subset of the remaining clauses.) This is an instance of MAX-SAT; and its solution corresponds to a solution to the original problem.

Alternatively, you can express it as an instance of weighted MAX-SAT. As before, use the conjunction $\Gamma \land t_1 \land \dots \land t_k$, but now give every clause in $\Gamma$ some large weight $W$ (chosen so that effectively, $\Gamma$ is forced to be satisfied) and each clause $t_i$ weight 1. This is an instance of weighted MAX-SAT; and its solution corresponds to a solution to the original problem.


I'm not sure why your #SAT solver was returning "infinity". Maybe you need to find a better solver for #SAT. Actually, approximate-#SAT would be good enough for your needs. See e.g. Is there a sometimes-efficient algorithm to solve #SAT? and Using SMT solvers to generate random solutions to given predicate for some relevant literature and techniques.

$\endgroup$
  • $\begingroup$ Thanks, I will check this out. I use ApproxCount, maybe my artificial test case isn't constrained enough. Or, maybe, I use a wrong set of options, so it just couldn't estimate the number of solutions. $\endgroup$ – CaptainTrunky Apr 22 '15 at 7:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.