Hi, see here:
http://doc.sagemath.org/html/en/reference/sat/index.html#solvers sage: from sage.sat.solvers.dimacs import DIMACS sage: fn = tmp_filename() sage: solver = DIMACS(filename=fn) sage: solver.add_clause( ( 1, 2, 3) ) sage: solver.add_clause( ( 1, 2, -3) ) sage: _ = solver.write() sage: for line in open(fn).readlines(): ....: print line, p cnf 3 2 1 2 3 0 1 2 -3 0 or simpler: sage: from sage.sat.solvers.dimacs import DIMACS sage: fn = tmp_filename() sage: solver = DIMACS() sage: solver.add_clause( ( 1, 2, 3) ) sage: solver.add_clause( ( 1, 2, -3) ) sage: solver.clauses(fn) sage: for line in open(fn).readlines(): ....: print line, p cnf 3 2 1 2 3 0 1 2 -3 0 On Thursday 14 May 2015 00:44:41 Alan Chee wrote: > Hi all!, > > I downloaded the CryptoMiniSat package from > http://www.sagemath.org/packages/optional/ and I hope to save the CNF > clauses derived from a polynomial system to a file. I > did the following: > > sage: from sage.sat.converters.polybori import CNFEncoder > sage: from sage.sat.solvers import CryptoMiniSat > sage: cms = CryptoMiniSat() > > sage: fn = tmp_filename() > sage: phi = CNFEncoder(cms,R) > sage: phi(F) # F is a system of Booleanpolynomials > > However, there is no 'clauses' attribute for the cms object for sage 5.7. > Is there any way to write the CNFs to a file? > Thanks in advance! > > Alan -- You received this message because you are subscribed to the Google Groups "sage-support" 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-support. For more options, visit https://groups.google.com/d/optout.
