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

dev-0.18.0 #237

Draft
wants to merge 22 commits into
base: main
Choose a base branch
from
Draft

dev-0.18.0 #237

wants to merge 22 commits into from

Conversation

shnarazk
Copy link
Owner

@shnarazk shnarazk commented Mar 26, 2024 •
edited
Loading

  • Redesign Clause
  • Simplify clause reduction implementation
  • Increase fundamental types' bit-widths

target line

# 0.16.1, timeout:2000 on localhost @ 2024-08-15T16:27:32
# ~/.cargo/bin/splr-0.17.3 (0.18.0-dev0) @ 2024-04-27T01:23:06
solver,       num,                       target,     time
"splr-0.17.3",  1,                 "UF250(100)",   33.543
"splr-0.17.3",  2,                "UUF250(100)",  126.195
"splr-0.17.3",  3,   "3SAT/360  S722433227-030",   13.189
"splr-0.17.3",  4,   "3SAT/360 S2032263657-035",    6.483
"splr-0.17.3",  5,   "3SAT/360  S368632549-051",    8.475
"splr-0.17.3",  6,   "3SAT/360 S1684547485-073",    0.600
"splr-0.17.3",  7,   "3SAT/360 S1711406314-093",   11.929
"splr-0.17.3",  8,   "3UNS/360 S1369720750-015",   67.939
"splr-0.17.3",  9,   "3UNS/360  S367138237-029",  172.283
"splr-0.17.3", 10,   "3UNS/360  S680239195-053",   94.397
"splr-0.17.3", 11,   "3UNS/360  S253750560-086",   69.033
"splr-0.17.3", 12,   "3UNS/360 S1028159446-096",   86.342
"splr-0.17.3", 13,   "[SAT] SR2015/m283,  3553",   24.382
"splr-0.17.3", 14,   "[SAT] SR2015/38b,    448",    6.913
"splr-0.17.3", 15,   "[SAT] SR2015/44b,    609",   10.248
"splr-0.17.3", 16,   "[SAT] SC21/b04_s_unknown",   38.712
"splr-0.17.3", 17,   "[SAT] SC21/quad_r21_m22 ",    6.976
"splr-0.17.3", 18,   "[SAT] SC21/toughsat_895s",   72.302
"splr-0.17.3", 19,   "[UNS] SC21/assoc_mult_e3",   75.138
"splr-0.17.3", 20,   "[UNS] SC21/dist4.c      ",  134.452
"splr-0.17.3", 21,   "[UNS] SC21/p01_lb_05    ",   36.283
"splr-0.17.3", 22,   "[UNS] SC21/shift1add    ",   92.997
med:    37.498, max:   172.283,           total: 1188.811

# 0.16.1, timeout:2000 on localhost @ 2024-08-11T20:47:29
solver,       num,                       target,     time
"0.17.3",       1,                 "UF250(100)",   34.514
"0.17.3",       2,                "UUF250(100)",  126.764
med:    80.639, max:   126.764,           total:  161.278

$f = log_2(scale) + 1$

solver,       num,                       target,     time
"dc2af717",     1,                 "UF250(100)",   81.421
"dc2af717",     2,                "UUF250(100)",  179.593
med:   130.507, max:   179.593,           total:  261.014

$f = log_2(scale) + 2$

solver,       num,                       target,     time
"dc2af717",     1,                 "UF250(100)",   54.338
"dc2af717",     2,                "UUF250(100)",  132.133
med:    93.236, max:   132.133,           total:  186.471

$f = log_2(scale) + 3$

solver,       num,                       target,     time
"dc2af717",     1,                 "UF250(100)",   45.617
"dc2af717",     2,                "UUF250(100)",  125.561
med:    85.589, max:   125.561,           total:  171.178

$f = log_2(scale) + 4$

solver,       num,                       target,     time
"dc2af717",     1,                 "UF250(100)",   45.419
"dc2af717",     2,                "UUF250(100)",  132.757
med:    89.088, max:   132.757,           total:  178.176

$f = log_2(scale) + 5$

solver,       num,                       target,     time
"dc2af717",     1,                 "UF250(100)",   38.306
"dc2af717",     2,                "UUF250(100)",  142.196
med:    90.251, max:   142.196,           total:  180.502

$f = 2 \times log_2(scale)$

solver,       num,                       target,     time
"dc2af717",     1,                 "UF250(100)",   72.765
"dc2af717",     2,                "UUF250(100)",  188.014
med:   130.309, max:   188.014,           total:  260.779

$f = 2 \times log_2(scale) + 1$

solver,       num,                       target,     time
"dc2af717",     1,                 "UF250(100)",   82.930
"dc2af717",     2,                "UUF250(100)",  197.382
med:   140.156, max:   197.382,           total:  200.312

$f = 2 \times log_2(scale) + 2$

solver,       num,                       target,     time
"dc2af717",     1,                 "UF250(100)",   51.277
"dc2af717",     2,                "UUF250(100)",  134.194
med:    92.736, max:   134.194,           total:  185.471

$f = 2 \times log_2(scale) + 3$

solver,       num,                       target,     time
"dc2af717",     1,                 "UF250(100)",   44.060
"dc2af717",     2,                "UUF250(100)",  130.964
med:    87.512, max:   130.964,           total:  175.024

$f = 2 \times log_2(scale) + 4$

solver,       num,                       target,     time
"dc2af717",     1,                 "UF250(100)",   44.425
"dc2af717",     2,                "UUF250(100)",  140.583
med:    92.504, max:   140.583,           total:  185.008

$f = 3 \times log_2(scale) - 1$

solver,       num,                       target,     time
"dc2af717",     1,                 "UF250(100)",  149.712
"dc2af717",     2,                "UUF250(100)",  988.551
med:   569.131, max:   988.551,           total: 1138.263

@shnarazk shnarazk self-assigned this Mar 26, 2024
@shnarazk
WatchLiteralIndex dancing weaves (#251)
6875911 
* Add dancing links to `Clause`

* Remove watch_cache

* Refactor `assign`

* (StageManager) change stage unit

* redesign Clause::search_from

* Switch to WatchLiteralIndexWeaver (#250)

* change feature "no_clause_elimination" to "clause_elimination"

* remove feature `unsafe_access`

* Add feature 'interleave' (#245)

* add ratatui

* add experimental executable 'splw'

* Add feature `deterministic`  (#249)

* eliminator: ditch `timedout`

* delete old `Solver::search`

* eliminator: use the length of a clause instead of the number of clauses for abort condition

* solver: rename 'SearchContext' to 'SearchState'

* deleted:    .gitlab-ci.yml

* rename feature 'watch' to 'graph_view'

* new file (a non-deterministic instance):   cnfs/uf200-074.cnf

* fix the region controlled by feature 'clause_elimination'

* make 'deterministic' default

* revert (some) eliminator settings

* 0.18.0-dev1 as 0240705-WatchLiteralIndexDancingWeaver

* new file:   cnfs/uf75-01.cnf

* `update_lbd` counts unassigned literals

* debug; change `Lit` definition to use `u32`

* Fix a crucial typo in `try_subsume`

* Rename `Clause::links` to `link`

* Remove FlagClause::DEAD

* `AssignReason::Implication` takes `WatchLiteralIndex`; drop `FlagClause::PROPAGATEBY1`

* Weavers select push-head or push-tail automatically based on c.rank

* 20240714 delete biclause loop (#253)

* revert `update_lbd` to take a working buffer
* Delete biclause loop; various optimizations guided by profiler
* change the condition to call minimize_with_bi_clauses
* (src/bin/splw.rs) add var activity moving history
* Rename `Var::reward` to `activity`

* bump version to 0.18.0-dev3
@shnarazk shnarazk added enhancement New feature or request experimental project labels Jul 16, 2024
shnarazk added 11 commits July 20, 2024 16:27
@shnarazk
Fix errors on features on reduce (#255)
72f5d5d 
* Fix errors under 'clause_rewarding'; redefine 'just_used'
* src/solver/search.rs: add more branches on clause reduction
@shnarazk
revise a comment
278beb0
@shnarazk
Remove a default feature 'deterministic', which is not in use now
2cbf629
@shnarazk
Spin momentum (#254)
dc0a0d8 
* Bump version to dev3-spin
* Ema* are derived from `Default`
* `Var` has `spin`
* Splw displays the development of spins
* Delegate AssignStack::activity to Var::activity
@shnarazk
bump version to 0.18.0-dev4
7bd27eb
@shnarazk
modified: src/bin/splw.rs
24a3627
@shnarazk
modified: Cargo.toml
206ad74
@shnarazk
Remove ClauseDB::new_clause_sandbox
72a7c59
@shnarazk
Remove AssignStack::propagate_sandbox
1a8e201
@shnarazk
Remove unused FlagClause::SANDBOX
d35f97a
@shnarazk
20240728 rewrite conflict_analyze (#259)
a9dd091 
* bump to 0.18.0-dev5

* conflict-side-rewarding + just_used (non)reduction

* cargo: update rust-verion; cargo update

* (conflict_analyze) Switch from `loop` to `for`
@shnarazk
Copy link
Owner Author

shnarazk commented Jul 29, 2024 •
edited
Loading

What a bummer! Disappointed!

nix$ cargo run --release -- cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf
warning: unused manifest key: build
    Finished `release` profile [optimized] target(s) in 0.02s
     Running `~/.cargo/target/release/splr cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf`
unif-k3-r4.25-v360-c1530-S1293537826-039.cnf       360,1530 |time:  1333.01
 #conflict:   24269436, #decision:     33695466, #propagate:     1304320284
  Assignment|#rem:      349, #fix:        2, #elm:        9, prg%:   3.0556
      Clause|Remv:    48650, LBD2:     3437, BinC:       22, Perm:     1499
    Conflict|entg:   7.4957, cLvl:  11.2724, bLvl:  10.1228, /cpr:   331.93
    Learning|avrg:  12.3750, trnd:   1.2995, #RST:   202138, /dpc:     1.77
        misc|vivC:     5220, xplr:   0.5816, core:      121, /ppc:    53.75
      Result|file: ./ans_unif-k3-r4.25-v360-c1530-S1293537826-039.cnf
s SATISFIABLE: cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@shnarazk shnarazk

Labels
enhancement New feature or request experimental project
Projects
None yet
Milestone
No milestone
Development

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