Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

a new branch: define a new type representing solver's result #64

Merged
merged 5 commits into from
Dec 9, 2017
Merged

a new branch: define a new type representing solver's result #64

merged 5 commits into from
Dec 9, 2017

Conversation

shnarazk
Copy link
Owner

@shnarazk shnarazk commented Dec 9, 2017 •
edited
Loading

  • add SolverResult
  • support a CSV-formatted status report for benchmarking

shnarazk added 4 commits December 9, 2017 14:41
a new branch: define a new type representing solver's result
63c3514
done: as a side effect, the benchmark format was updated:
1bd3cc5 
The CSV has the following 5 fields:
solverId,sequenceNum,problem,elapsedTime,flag

* flag=0: solved as UNSAT
* flag=1: solved as SAT
* flag=2: too large to solve
* flag=3: timeout
Mios.hs: revise comment
51b324b
Mios.hs: update the export list
5f1b6a1
@shnarazk shnarazk mentioned this pull request Dec 9, 2017
Merged
5 tasks
@shnarazk
Copy link
Owner Author

shnarazk commented Dec 9, 2017

d48dae3 no problem

# 2017-12-09T16:13 mios-1.5.3; mios-1.5.3#64 -- https://github.com/shnarazk/mios
# sat-benchmark 0.13.5, j=1, t=510, p='' on xingu @ 2017-12-09T16:14:38+09:00
"mios-1.5.3", 1, 200,	 20.09
"mios-1.5.3", 2, 225,	 49.15
"mios-1.5.3", 3, 250,	 134.06
"mios-1.5.3", 4, "itox",	 25.55
"mios-1.5.3", 5, "m283",	 80.50
"mios-1.5.3", 6, "38b",	 21.97
"mios-1.5.3", 7, "44b",	 77.75

@shnarazk shnarazk merged commit 1fbe7b2 into WIP-for-1.5.3 Dec 9, 2017
shnarazk added a commit that referenced this pull request Dec 13, 2017
@shnarazk
mios version 1.5.3 (#61)
b11e210 
- implement EMA based Glucose heuristics (Biere 2015) #62 
- implement two-phase restart
- fix a bug on learnt clause reduction in a marginal situation
- thread-based timeout handling #58
- update command line options
- update the benchmark report format #64 
- add a new type to represent search result #64
- learnt clause simplification uses 64-bit computation
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@shnarazk