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:

Status badges

Description (last modified by boothby)

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)

trac_5671-part1.patch (4.9 KB) - added by was 12 years ago.
minisat.spkg (78.6 KB) - added by boothby 12 years ago.
trac_5671-part2.patch (933 bytes) - added by boothby 12 years ago.
trac_5671-part3.patch (3.7 KB) - added by was 12 years ago.

Download all attachments as: .zip

Change History (20)

Changed 12 years ago by was

comment:1 Changed 12 years ago by boothby

  • Description modified (diff)
  • Summary changed from Create a spkg for minisat to Wrap miniSAT.

comment:2 Changed 12 years ago by mabshoff

  • Milestone set to sage-3.4.2

Might I point out that this is a dupe of #418.

You also

  • should assign a milestone when you open a ticket
  • not attach spkgs to tickets, but post a link. Given that this one is 77kb it might be a borderline case.

Cheers,

Michael

Changed 12 years ago by boothby

Changed 12 years ago by boothby

Changed 12 years ago by was

comment:3 Changed 12 years ago by was

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 was

  • Summary changed from Wrap miniSAT. to Create a documented minimal useful Cython wrapper for miniSAT along with an spkg

comment:5 follow-up: Changed 12 years ago by malb

This

http://planete.inrialpes.fr/~soos/CryptoMiniSat/index.html

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 kcrisman

  • Report Upstream set to N/A

Replying to malb:

This

http://planete.inrialpes.fr/~soos/CryptoMiniSat/index.html

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 fichtejo

  • Cc fichtejo added

comment:8 Changed 9 years ago by malb

I vote for declaring this ticket a dupe.

comment:9 Changed 8 years ago by jdemeyer

  • Milestone changed from sage-5.11 to sage-5.12

comment:10 Changed 7 years ago by vbraun_spam

  • Milestone changed from sage-6.1 to sage-6.2

comment:11 Changed 7 years ago by mmezzarobba

  • Milestone changed from sage-6.2 to sage-duplicate/invalid/wontfix
  • Status changed from new to needs_review

comment:12 follow-up: Changed 7 years ago by malb

I'm not sure what needs review here?

comment:13 Changed 7 years ago by kcrisman

  • 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 mmezzarobba

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 kcrisman

Which has been done :) mmezz, just add your real name in the reviewers field.

comment:16 Changed 7 years ago by vbraun

  • Resolution set to duplicate
  • Status changed from positive_review to closed
Note: See TracTickets for help on using tickets.