using CUDF for SAT solving

[Clemens Lang]

Hi,

----- On 25 Mar, 2015, at 13:28, Jackson Isaac jacksonisaac2008 at gmail.com wrote:

> So one single CUDF file will contain information about all the
> packages and dependencies?

That is my understanding, but it's been a while since I've read the spec.


> I was going through the cudf 2.0 specifications:
> http://www.mancoosi.org/reports/tr3.pdf and it says in one CUDF file
> there would be a preamble, list of dependent packages followed by one
> requested package.

Yeah, but since we want the SAT solver to compute *which* packages are
dependencies the list of dependent packages would have to contain them
all, if I'm not mistaken. I'll re-read to make sure.


>> Using CUDF has the
>> advantage of already "knowing" what dependencies and packages are, so we
>> don't have to do the mapping to boolean formulas.
> 
> We can extract Portfile information using the dlist Datastructure
> from which we can get the package to be installed and list of
> dependencies and create a CUDF.
> 
> What to do with this CUDF that we get?
> Do we need to implement a module which will solve (probably interpret)
> this CUDF and then pass that information to the installer (after
> displaying the output and confirming from the user) as I can't find
> how will this cudf file solve the dependencies and conflicts? Is it
> using libCUDF ? If so, we could implement our own file as you
> mentioned above, so that we could add more features to it.

There are solvers available that will use CUDF as input and print a
solution as output. We'll have to test a few, call those solvers with the
correct input and parse the output they generate. 

-- 
Clemens Lang