In the car industry you have thousand of different variants of components available to choose from when you buy a car. Not every component is combinable, so for each car there exist a lot of rules that are expressed in propositional logic. In my case each car has between 2000 and 4000 rules.
They look like this:
where "∧" = "and" / "∨" = "or" / "¬" = "not" / "→" = "implication".
With the tool "limboole" (http://fmv.jku.at/limboole/) I am able to to convert the propositional logic expressions into conjunctive normal form (CNF). This is needed in case I have to use a SAT solver.
Now, I would like to check the buildability feasibility for specific components within the rule set. For example, for each of the following expressions or combinations, I would like to check if the are feasible within the rule set.
My question is how to solve this problem. I asked a similar questions before (Tool to solve propositional logic / boolean expressions (SAT Solver?)), but with a different focus and now I am stuck again. Or I just do not understand it.
One option is to calculate all solutions with an ALLSAT approach of the rule set. Then I could check if each combination is part of any solution. If yes, I can derive that this specific combination is feasible.
Another option would be, that I add the combination to the rule set and then run a normal SAT solver. But I would have to do it for each expression I want to check.
What do you think is the most elegant or rather easiest way to solve this problem?
The best method which is known to me is to use "incremental solving under assumptions" technique. It was motivated by the same problem you have: multiple SAT instances (CNF formulae) which have some common subformulae.
Formally, you have some core Boolean formula C in CNF. And you have a set of assumptions {A_i}, i=1..n, where A_i is a Boolean formula in CNF also.
On the step 0 you provide to the solver your core formula C. It tries to solve it, says a result to you and save its state (lets call this state as core-state). If formula C is satisfiable, on the step i you provide assumption A_i to the solver and it continues its execution from the core-state. Actually, it tries to solve a formula C ∧ A_i but not from the beginning.
You can find a bunch of papers related to this topic easily, where much information is located. Also, you can check you favorite SAT-solver for the support of this technique.