On 2012-05-01, Tom Boothby <tomas.boot...@gmail.com> wrote:
> At one point, Victor Miller, William Stein and I looked at interfacing
> directly to minisat, but IMO, we stopped due to a lack of a nice
> interface. I've tried to rewrite my SAT approach every time I solve a
> new problem with SAT solvers -- forcing me to rethink it every time.
>
> In general, I've gotten happier with the interface every time, and I'm
> fairly satisfied with this. In particular, it feels very similar to
> the interface for DLXCPP, the ExactCover solver in Sage. It supports
> any hashable variables, and most SAT solvers. I don't know anything
> about MAXSAT.
well, there you have weights on clauses, and the goal is to find an
assignment minimising the total weight of unsatisfied clauses.
It would report such an assigment, and/or the corresponding total
weight. One can use integer linear programming for this, but this
is often sub-optimal.
>
> If anybody wants to use this, I'm happy to place it in the public domain.
>
> SATPROG = '/home/boothby/minisat'
> class SAT:
> def __init__(self,clauses):
> self.vars = {}
> self.clauses = []
> for c in clauses:
> self(*c)
> def __getitem__(self,k):
> if k in self.vars:
> return self.vars[k]
> else:
> r = self.vars[k] = len(self.vars)+1
> return r
> def __call__(self,pos = (),neg = ()):
> clause = [` self[v]` for v in pos]
> clause+= [`-self[v]` for v in neg]
> self.clauses.append(clause)
> def __str__(self):
> s = 'p cnf %s %s\n'%(len(self.vars), len(self.clauses))
> s+= ' 0\n'.join(map(' '.join, self.clauses+['']))
> return s
>
> def solve(self):
> fn = tmp_filename()
> open(fn+".sat",'w').write(str(self))
> os.system("%s -verb=0 %s.sat %s.sol >/dev/null"%(SATPROG,fn,fn))
> sol = open(fn+".sol")
> res = sol.readline()[:-1]
> if res == "SAT":
> xtovar = dict((v,k) for k,v in self.vars.iteritems())
> keys = map(int,sol.readline().split(' ')[:-1])
> return [xtovar[i] for i in keys if i > 0], [xtovar[-i] for
> i in keys if i < 0]
> else:
> return None
>
> def all_sols(self):
> sol = self.solve()
> while sol is not None:
> pos,neg = sol
> yield pos,neg
> self(pos=neg,neg=pos)
> sol = self.solve()
>
> Example:
>
> sage: a,b,c,d = var('a,b,c,d')
> sage: clauses = [
> ... [ [a,b],[c] ], # a or b or not c
> ... [ [a,c],[b] ], # a or c or not b
> ... [ [c,d],[] ], # c or d
> ...
> sage: ]
> sage: for sol in SAT(clauses):
> ... pos,neg = sol
> ... print pos
> [a, d]
> [d]
> [a, c]
> [a, c, d]
> [a, b, d]
> [b, c]
> [b, c, d]
> [a, b, c]
> [a, b, c, d]
>
> On Tue, May 1, 2012 at 2:40 AM, Dima Pasechnik <dimp...@gmail.com> wrote:
>> On 2012-05-01, Martin Albrecht <martinralbre...@googlemail.com> 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: martinralbre...@jabber.ccc.de
>>>
>>
>> --
>> To post to this group, send an email to sage-devel@googlegroups.com
>> To unsubscribe from this group, send an email to
>> sage-devel+unsubscr...@googlegroups.com
>> For more options, visit this group at
>> http://groups.google.com/group/sage-devel
>> URL: http://www.sagemath.org
>
--
To post to this group, send an email to sage-devel@googlegroups.com
To unsubscribe from this group, send an email to
sage-devel+unsubscr...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/sage-devel
URL: http://www.sagemath.org
