On 2012-05-01, Martin Albrecht <[email protected]> wrote: > Hi, > > On Tuesday 01 May 2012, Dima Pasechnik wrote: >> Has there been any discussion and/or consensus on how to encode boolean >> formulae in Sage? > > So far the only interfaces to SAT Solvers were fire & forget interfaces for > Boolean polynomials. There also the logic module but I never used it.
The latter (which I was not even aware about, thanks for pointing it out!) is very basic. In constructs truth tables and decides satisfiability by searching them, which makes it pretty useless for "real" problems. On the other hand it can parse quite complicated expressions, so it seems to be a reasonable starting point for extension. Or maybe not... Dima > >> I, incidentally, need to solve some MAXSAT problems from Sage-generated >> data, and am musing about writing a proper interface to akmaxsat, see >> http://www.uni-ulm.de/fileadmin/website_uni_ulm/iui.inst.190/Mitarbeiter/ku >> egel/akmaxsat_1.1.tgz which has a Sage-compatible licence, by the way... >> >> Dima > > Cheers, > Martin > > -- > name: Martin Albrecht > _pgp: http://pgp.mit.edu:11371/pks/lookup?op=get&search=0x8EF0DC99 > _otr: 47F43D1A 5D68C36F 468BAEBA 640E8856 D7951CCF > _www: http://martinralbrecht.wordpress.com/ > _jab: [email protected] > -- To post to this group, send an email to [email protected] To unsubscribe from this group, send an email to [email protected] For more options, visit this group at http://groups.google.com/group/sage-devel URL: http://www.sagemath.org
