Opened 3 years ago
Closed 3 years ago
#14180 closed enhancement (fixed)
SatSolver.clauses
Reported by: | malb | Owned by: | jason |
---|---|---|---|
Priority: | major | Milestone: | sage-5.8 |
Component: | misc | Keywords: | sat, cryptominisat |
Cc: | Merged in: | sage-5.8.beta3 | |
Authors: | Martin Albrecht | Reviewers: | Nathann Cohen |
Report Upstream: | N/A | Work issues: | |
Branch: | Commit: | ||
Dependencies: | #14198 | Stopgaps: |
Description
Add a function to SatSolver to get back the original clauses.
Attachments (1)
Change History (19)
comment:1 Changed 3 years ago by malb
comment:2 Changed 3 years ago by ncohen
(cc me)
comment:3 Changed 3 years ago by malb
- Dependencies set to #14198
- Status changed from new to needs_review
attached patch depends on #14198
comment:4 Changed 3 years ago by ncohen
- Status changed from needs_review to needs_work
This patch does not apply on beta2, because of #6495 that totally changed the filenames in doc/.
Nathann
Changed 3 years ago by malb
comment:5 Changed 3 years ago by malb
- Status changed from needs_work to needs_review
Updated the patch 5.8.beta2
comment:6 follow-up: ↓ 8 Changed 3 years ago by ncohen
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
comment:7 Changed 3 years ago by ncohen
- Status changed from needs_review to needs_info
comment:8 in reply to: ↑ 6 ; follow-up: ↓ 9 Changed 3 years ago by malb
Replying to ncohen:
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.
comment:9 in reply to: ↑ 8 ; follow-up: ↓ 10 Changed 3 years ago by ncohen
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
comment:10 in reply to: ↑ 9 Changed 3 years ago by malb
Replying to ncohen:
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.
comment:11 Changed 3 years ago by malb
- Type changed from PLEASE CHANGE to enhancement
comment:12 follow-up: ↓ 14 Changed 3 years ago by ncohen
- Reviewers set to Nathann Cohen
- Status changed from needs_info to needs_review
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
comment:13 Changed 3 years ago by ncohen
- Status changed from needs_review to positive_review
comment:14 in reply to: ↑ 12 ; follow-up: ↓ 15 Changed 3 years ago by malb
Replying to ncohen:
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!
comment:15 in reply to: ↑ 14 Changed 3 years ago by ncohen
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
comment:16 follow-up: ↓ 17 Changed 3 years ago by malb
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?
comment:17 in reply to: ↑ 16 Changed 3 years ago 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
comment:18 Changed 3 years ago by jdemeyer
- Merged in set to sage-5.8.beta3
- Resolution set to fixed
- Status changed from positive_review to closed
The attached patch requires CryptoMiniSat? 2.9.6 (which hasn't been released yet).