SatSolver.clauses

[malb]

Add a function to SatSolver to get back the original clauses.

Depends on #14198

Component: misc

Keywords: sat, cryptominisat

Author: Martin Albrecht

Reviewer: Nathann Cohen

Merged: sage-5.8.beta3

Issue created by migration from https://trac.sagemath.org/ticket/14180

[malb]

comment:1

The attached patch requires CryptoMiniSat 2.9.6 (which hasn't been released yet).

[6bdad4c1-1e26-4f2f-a442-a01a2292c181]

comment:2

(cc me)

[malb]

comment:3

attached patch depends on #14198

[malb]

Dependencies: #14198

[6bdad4c1-1e26-4f2f-a442-a01a2292c181]

comment:4

This patch does not apply on beta2, because of #6495 that totally changed the filenames in doc/.

Nathann

[malb]

Attachment: trac_14180_satsolver_clauses.patch.gz

[malb]

comment:5

Updated the patch 5.8.beta2

[6bdad4c1-1e26-4f2f-a442-a01a2292c181]

comment:6

HMmmmmmmmm... I've got some questions about your patch :

• You do not seem to accept as input a DIMACS file with is_xor clauses with clauses(), while you WRITE such files with render_dimacs() ?...
• I do not get what this does... It's meant to store is_xor clauses but I don't get it ^^;

closing = lits[-1] if rhs else -lits[-1]
fh.write("x" + " ".join(map(str, lits[:-1])) + " %d 0\n"%closing)

• I do not get this either

+    def __getattr__(self, name):
+        """
+        EXAMPLE::
+
+            sage: from sage.sat.solvers.satsolver import SatSolver
+            sage: solver = SatSolver()
+            sage: solver.gens() # __getattr__ points this to clauses
+            Traceback (most recent call last):
+            ...
+            NotImplementedError
+        """
+        if name == "gens":
+            return self.clauses
+        else:
+            raise AttributeError("'%s' object has no attribute '%s'"%(self.__class__.__name__,name))
+
+    def trait_names(self):
+        """
+        Allow alias to appear in tab completion.
+
+        EXAMPLE::
+
+            sage: from sage.sat.solvers.satsolver import SatSolver
+            sage: solver = SatSolver()
+            sage: solver.trait_names()
+            ['gens']
+        """
+        return ["gens"]

Why don't you just create a gens method ? Why would you need one by the way, as it is an alias to `clauses` anyway ?

Have fuuuuuuuuuuuuuuuuuuuuuuuunnn !!

Nathann

[malb]

comment:8

Replying to @nathanncohen:

HMmmmmmmmm... I've got some questions about your patch :

• You do not seem to accept as input a DIMACS file with is_xor clauses with clauses(), while you WRITE such files with render_dimacs() ?...

clauses() does not accept any input file, only a file to write to (?)

• I do not get what this does... It's meant to store is_xor clauses but I don't get it ^^;

CryptoMiniSat expresses xor clauses by prefixing them with an "x" and flipping the last clause if the right hand side if false.

• I do not get this either Why don't you just create a gens method ? Why would you need one by the way, as it is an alias to clauses anyway ?

A gens() method needs doctstring, doctests etc. This way, everything is in place automatically. I added the alias gens() for clauses() because Sage users are used to gens() as the method to return the generators.

[6bdad4c1-1e26-4f2f-a442-a01a2292c181]

comment:9

clauses() does not accept any input file, only a file to write to (?)

Oops right. I meant : when you read self._tail. The parsing only creates clauses with is_xor set to False :

clauses.append( ( tuple(clause), False, None ) )

Hence the output of clauses never returns a clause with is_xor = True.

Oh. But may it be because there is actually no way to create a xor clause with te DIMACS interface ?

CryptoMiniSat expresses xor clauses by prefixing them with an "x" and flipping the last clause if the right hand side if false.

Oh. Weird. Thanks :-)

A gens() method needs doctstring, doctests etc. This way, everything is in place automatically. I added the alias gens() for clauses() because Sage users are used to gens() as the method to return the generators.

?

Well, why wouldn't you just write gens = clauses then ? O_o

Nathann

[malb]

comment:10

Replying to @nathanncohen:

clauses() does not accept any input file, only a file to write to (?)

Oh. But may it be because there is actually no way to create a xor clause with te DIMACS interface ?

Correct, only CryptoMiniSat does that.

Well, why wouldn't you just write gens = clauses then ? O_o

If I do this in the base clase (SatSolver) it would point to the clauses() method in the base class which just raises NotImplementedError. So every subclass would have to redefine it it. This way (doing it in __getattr__ means it is handled automatically.

[6bdad4c1-1e26-4f2f-a442-a01a2292c181]

comment:12

Hellooooooooo again !!!

I read the patc anew, and this time I understood what I saw ! I am not a very big fan of your text files though, but well.. If it does the job for you :-)

Anyway this patch does its job, passes test, and can make it into Sage asap !

Nathann

[6bdad4c1-1e26-4f2f-a442-a01a2292c181]

Reviewer: Nathann Cohen

[malb]

comment:14

Replying to @nathanncohen:

I read the patch anew, and this time I understood what I saw ! I am not a very big fan of your text files though, but well.. If it does the job for you :-)

Can you elaborate on that? I could try to fix it (in another patch). Do you mean something with textfiles I just added or something that was in the DIMACS class before this patch? To explain the latter case: I didn't want to keep clauses in RAM because I routinely have problems with gigabytes of clauses.

Anyway this patch does its job, passes test, and can make it into Sage asap !

Thanks!

[6bdad4c1-1e26-4f2f-a442-a01a2292c181]

comment:15

Can you elaborate on that? I could try to fix it (in another patch). Do you mean something with textfiles I just added or something that was in the DIMACS class before this patch? To explain the latter case: I didn't want to keep clauses in RAM because I routinely have problems with gigabytes of clauses.

Nonnoo, it's nothing that you added just there. Well, for a start it took me some time to realise that your ._tail variable was actually your whole data. The place where you store everything. And you parse it each time you want to find out the list of clauses, which I don't like either. It nothing you added here, just "how this system is built".

Of course, if you tell me that you usually cannot store your clauses in memory, then that's another problem and you probaly found the best answer by storing this in text files.

Well. Storing RAM stuff in text file is what SWAP does, though.

Really ? This takes Gigabytes of clauses ? List of lists of integers ? :-/

How do the solver deal with them, then ? Do they work directly on the text files ? O_o;;;

Nathann

[malb]

comment:16

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?

[6bdad4c1-1e26-4f2f-a442-a01a2292c181]

comment:17

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

[jdemeyer]

Merged: sage-5.8.beta3