Opened 12 years ago
Closed 7 years ago
#5671 closed enhancement (duplicate)
Create a documented minimal useful Cython wrapper for miniSAT along with an spkg
Reported by: | boothby | Owned by: | boothby |
---|---|---|---|
Priority: | minor | Milestone: | sage-duplicate/invalid/wontfix |
Component: | packages: standard | Keywords: | |
Cc: | fichtejo | Merged in: | |
Authors: | Reviewers: | Martin Albrecht, Karl-Dieter Crisman | |
Report Upstream: | N/A | Work issues: | |
Branch: | Commit: | ||
Dependencies: | Stopgaps: |
Description (last modified by )
Sage lacks a SAT solver. First step, lets make a spkg and wrap it. In the future, we should add boolean functions, etc., but one step at a time.
Attachments (4)
Change History (20)
Changed 12 years ago by
comment:1 Changed 12 years ago by
- Description modified (diff)
- Summary changed from Create a spkg for minisat to Wrap miniSAT.
comment:2 Changed 12 years ago by
- Milestone set to sage-3.4.2
Changed 12 years ago by
Changed 12 years ago by
Changed 12 years ago by
comment:3 Changed 12 years ago by
With just the posted code to this point:
sage: S = minisat.Solver(verbosity=2) sage: S.new_var() 0 sage: S.new_var() 1 sage: S.new_var() 2 sage: S.new_var() 3 sage: S.add_clause([1]) pushing lit.p = Literal 1 sage: S.add_clause([2]) pushing lit.p = Literal 2 sage: S.solve() ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 0 | 0 0 0 | 0 0 nan | 0.000 % | =============================================================================== Verified 0 original clauses. True
comment:4 Changed 12 years ago by
- Summary changed from Wrap miniSAT. to Create a documented minimal useful Cython wrapper for miniSAT along with an spkg
comment:5 follow-up: ↓ 6 Changed 12 years ago by
This
might be relevant. It is an enhanced MiniSat? with:
- Natively handled XOR functions
- Statistics generation
- Search randomization
- Detailed solving process visualization
- Clause grouping and group naming
- Variable naming
- Debug mode
- Code cleanup
comment:6 in reply to: ↑ 5 Changed 9 years ago by
- Report Upstream set to N/A
Replying to malb:
This
might be relevant. It is an enhanced MiniSat? with:
- Natively handled XOR functions
- Statistics generation
- Search randomization
- Detailed solving process visualization
- Clause grouping and group naming
- Variable naming
- Debug mode
- Code cleanup
Given this and recent developments at #418, perhaps this is a dupe?
comment:7 Changed 9 years ago by
- Cc fichtejo added
comment:8 Changed 9 years ago by
I vote for declaring this ticket a dupe.
comment:9 Changed 8 years ago by
- Milestone changed from sage-5.11 to sage-5.12
comment:10 Changed 7 years ago by
- Milestone changed from sage-6.1 to sage-6.2
comment:11 Changed 7 years ago by
- Milestone changed from sage-6.2 to sage-duplicate/invalid/wontfix
- Status changed from new to needs_review
comment:12 follow-up: ↓ 14 Changed 7 years ago by
I'm not sure what needs review here?
comment:13 Changed 7 years ago by
- Reviewers set to Martin Albrecht, Karl-Dieter Crisman
- Status changed from needs_review to positive_review
comment:14 in reply to: ↑ 12 Changed 7 years ago by
Replying to malb:
I'm not sure what needs review here?
As far as I understand the way to have a ticket closes as "wontfix" or similar is to set the milestone to duplicate/invalid/wontfix
and wait for someone else to review that choice.
comment:15 Changed 7 years ago by
Which has been done :) mmezz, just add your real name in the reviewers field.
comment:16 Changed 7 years ago by
- Resolution set to duplicate
- Status changed from positive_review to closed
Might I point out that this is a dupe of #418.
You also
Cheers,
Michael