#14180: SatSolver.clauses
--------------------------------------+-------------------------------------
Reporter: malb | Owner: jason
Type: enhancement | Status: positive_review
Priority: major | Milestone: sage-5.8
Component: misc | Resolution:
Keywords: sat, cryptominisat | Work issues:
Report Upstream: N/A | Reviewers: Nathann Cohen
Authors: Martin Albrecht | Merged in:
Dependencies: #14198 | Stopgaps:
--------------------------------------+-------------------------------------
Comment (by ncohen):
> The solvers of course deal with these clauses in RAM, I didn't want to
have them in RAM twice though. Perhaps I should add an option to keep it
in RAM (which would be default) and text files are used when explicitly
asked for?
Hmmmm... Looks like too much trouble if you always need to have them on a
disk file anyway `:-/`
What would you think of this: you deal with everything in RAM, ad you only
output it to a file when you want to actually solve it ? For Cryptominisat
there is no problem as you directly deal with that solver's data
structure.. But how do you work with other solvers ?
Actually, doing everything in RAM and creating the text file only when
needed makes sense too. Especially when you hav a function to write them
available already, and when the constructor can take a dimacs file as an
argument ?
Nathann
--
Ticket URL: <http://trac.sagemath.org/sage_trac/ticket/14180#comment:17>
Sage <http://www.sagemath.org>
Sage: Creating a Viable Open Source Alternative to Magma, Maple, Mathematica,
and MATLAB
--
You received this message because you are subscribed to the Google Groups
"sage-trac" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/sage-trac?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.
