[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Re: RFC: implementation of package pools



Anthony Towns wrote:

On Thu, Oct 26, 2000 at 02:52:53AM +0300, Eray Ozkural wrote:

Checking the license is AI-complete. ;)

Which is why we have a human do it.


Still, my proposal includes automation. You'll see what I mean by that
if I have some time from these awful projects. :/

Logic symbols are a solved problem: &, |, ~.
a Depends: b | c, d translates to  (~a | b | c) & (~a | d)
a Conflicts: b, c translates to (~a | ~b) & (~a | ~c)
a is installable translates to "a"

Correction: "a is installed translates to `a'", and "a is installable
is equivalent to -there exists a solution of the SAT problem where a
is true-"


Then here's the correct sentence for the example package, with the C-like notation that you use :) [The example is not a good one, as it seems to be a always false. ]

a & (b | c) & d & !b & !c

Anyway, translating depends and conflicts in this manner is trivial.

The problem is then:
Find a set of valuations to propositional letters in the sentence F that
yields truth value 1.

Which is really set, and the sentences are indeed in CNF.

Well, there must be something wrong here since if I give a valuation 0
to a then the two propositional sentences are satisfied trivially. Could you
please review this? Let's not be mistaken.

Yes, you can solve all the depends and conflicts relations by not
having anything installed. Please spend a little time thinking about
this in future before posting.


Well, Anthony I have difficulty in following this. You're first correcting something, and then you are saying it is incorrect that I'm warning that it is false. I'm trying
to say in the above paragraph that the translations

a Depends: b | c, d translates to  (~a | b | c) & (~a | d)
a Conflicts: b, c translates to (~a | ~b) & (~a | ~c)
are wrong, which you also seem to agree with.

At any rate, now that we've sorted out what the translation procedure is, we can
have a decisive solution to the uninvestigated problems.

1) Are these sentences mostly easy instances of the SAT problem?

It seems so. One justification is that your code runs quite fast for thousands of these sentences. And by inspection we see that the number of clauses is usually not much, and each clause usually contains a little number of disjunctive terms. We have agreement here.

2) Is the search algorithm complete?

Is it guaranteed to find a solution if there's one? I think you can answer that better, since you've coded it. Does it converge to BFS or DFS and exhaustively search every possible combination
of valuations? That should be the worst case behaviour.

It'd seem that anwering 2 would be enough for now, because correctness is more important than performance for any search algorithm. [And in this case, we'd like the search to be
complete]

Thanks,

__
Eray



Reply to: