{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":792945577,"defaultBranch":"main","name":"yass","ownerLogin":"rhartert","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2024-04-28T01:58:13.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/91352809?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1715152852.0","currentOid":""},"activityList":{"items":[{"before":"9461cb54a8dd37a4fa7bede1957002b0189eb30e","after":"de93ae89d723ecc51346dda4ae19525826280e61","ref":"refs/heads/main","pushedAt":"2024-06-04T01:24:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Remove useless return","shortMessageHtmlLink":"Remove useless return"}},{"before":"dbd5a2ddefe4117db6a99429383e6d72b7957da8","after":"9461cb54a8dd37a4fa7bede1957002b0189eb30e","ref":"refs/heads/main","pushedAt":"2024-05-31T02:21:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Allow clients to import the sat and parsers pkg\n\nAllow clients to import the sat and parsers packages by moving them outside of the internal directory. The goal is to allow early clients (myself at the moment) to start using the solver in other projects. Note that the structure is likely to change in the future.","shortMessageHtmlLink":"Allow clients to import the sat and parsers pkg"}},{"before":"6665771a870855ae51bc3449cb1aec98217a4e5b","after":"dbd5a2ddefe4117db6a99429383e6d72b7957da8","ref":"refs/heads/main","pushedAt":"2024-05-20T07:16:24.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Minor refactoring of package dimacs (now parsers)","shortMessageHtmlLink":"Minor refactoring of package dimacs (now parsers)"}},{"before":"cd917efe4b1570a100b35927c20988301459cd3c","after":"6665771a870855ae51bc3449cb1aec98217a4e5b","ref":"refs/heads/main","pushedAt":"2024-05-19T02:33:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Use CNF parsing from package `rhartert/dimacs`\n\nThe parsing logic from package `dimacs` has been copied and refactored in its own repo/package `github.com/rhartert/dimacs`. This commit updates the code to use that new package.\n\nThis also simplify the code to read model files.","shortMessageHtmlLink":"Use CNF parsing from package <code>rhartert/dimacs</code>"}},{"before":"ce9b26065e13b3de1b1dd1d2932237f7d51f299c","after":"cd917efe4b1570a100b35927c20988301459cd3c","ref":"refs/heads/main","pushedAt":"2024-05-17T06:19:30.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Directly load DIMACS files in the solver\n\n... rather than loading them in the intermediary Instance struct which is then used to load the data in the solver.","shortMessageHtmlLink":"Directly load DIMACS files in the solver"}},{"before":"aaab8ec208f848820e3067588d880bea195b5637","after":"ce9b26065e13b3de1b1dd1d2932237f7d51f299c","ref":"refs/heads/main","pushedAt":"2024-05-17T02:56:10.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Make prints more informative\n\nThe main change in this commit is the addition of an \"event\" char at the beginning of each row. The letter indicates if the print was a restart (R), a clean-up of the local clauses (C), or simple info (no letter). This removed the need for the restart column which has been replaced with metrics about the core clauses.","shortMessageHtmlLink":"Make prints more informative"}},{"before":"389dc9daa88bae596c72d8254cad0bbae0b90fd7","after":"aaab8ec208f848820e3067588d880bea195b5637","ref":"refs/heads/main","pushedAt":"2024-05-17T02:51:05.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Separate learnt clauses in local and core clauses\n\nThis commit implements a similar clause management strategy as the one presented in Chanseok's PhD thesis (chapter 2).","shortMessageHtmlLink":"Separate learnt clauses in local and core clauses"}},{"before":"1eb73a381d346c9a976f05954c0a76281583d344","after":"389dc9daa88bae596c72d8254cad0bbae0b90fd7","ref":"refs/heads/main","pushedAt":"2024-05-16T14:37:31.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Free instance after reading\n\nQuick hack to reduce memory consumption. Ideally, this should be done inline, instantiating the clauses and the variables as the instance is read.","shortMessageHtmlLink":"Free instance after reading"}},{"before":"8ee1a0e971a4abe9c2be121df7a75f874bdfe612","after":"1eb73a381d346c9a976f05954c0a76281583d344","ref":"refs/heads/main","pushedAt":"2024-05-16T07:02:26.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Track exp moving average of conflict levels","shortMessageHtmlLink":"Track exp moving average of conflict levels"}},{"before":"4511075749978804b4cd2c6898a416d27e9c30c9","after":"8ee1a0e971a4abe9c2be121df7a75f874bdfe612","ref":"refs/heads/main","pushedAt":"2024-05-16T06:40:13.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Remove unnecessary pointers in favor of values","shortMessageHtmlLink":"Remove unnecessary pointers in favor of values"}},{"before":"5245e144f1de8ba4c9f5bc0a7a8fbddca1ead6a1","after":"4511075749978804b4cd2c6898a416d27e9c30c9","ref":"refs/heads/main","pushedAt":"2024-05-16T06:36:17.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Tweak balance between memory and speed in set.go\n\nUsing `int16` reduces the cost of loading the set of memory at the expense of increasing the frequency at which linear reinitialization of the structure are needed. Using `int16` seems to be improving the speed by ~1% on large instances.","shortMessageHtmlLink":"Tweak balance between memory and speed in set.go"}},{"before":"6e6e06489ab8d5d70b91494095edbce7640aa454","after":"5245e144f1de8ba4c9f5bc0a7a8fbddca1ead6a1","ref":"refs/heads/main","pushedAt":"2024-05-16T05:35:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Use the trail as the propagation queue\n\nThis commit removes `propQueue` which is redundant. Indeed, the same information is already available in the trail itself. Also rename `trailLim` to `trailLevels` which better convey what the slice is about.","shortMessageHtmlLink":"Use the trail as the propagation queue"}},{"before":"479942acd1cadd886fa4c8df81fa19f1d7e98ced","after":"6e6e06489ab8d5d70b91494095edbce7640aa454","ref":"refs/heads/main","pushedAt":"2024-05-16T02:51:56.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Improve readability of stats prints","shortMessageHtmlLink":"Improve readability of stats prints"}},{"before":"797b9146dea35d67c0dcf779151f92101bd0532a","after":"479942acd1cadd886fa4c8df81fa19f1d7e98ced","ref":"refs/heads/main","pushedAt":"2024-05-16T02:50:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Fix broken type change from 37e21cf","shortMessageHtmlLink":"Fix broken type change from <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/rhartert/yass/commit/37e21cf5b92b21dad80d516ba039d02f54ee19dd/hovercard\" href=\"https://github.com/rhartert/yass/commit/37e21cf5b92b21dad80d516ba039d02f54ee19dd\"><tt>37e21cf</tt></a>"}},{"before":"37e21cf5b92b21dad80d516ba039d02f54ee19dd","after":"797b9146dea35d67c0dcf779151f92101bd0532a","ref":"refs/heads/main","pushedAt":"2024-05-16T02:41:32.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Switch to Go 1.22","shortMessageHtmlLink":"Switch to Go 1.22"}},{"before":"5745b189a78b53daac364151bc4e30d690259f4e","after":"37e21cf5b92b21dad80d516ba039d02f54ee19dd","ref":"refs/heads/main","pushedAt":"2024-05-16T02:40:50.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Reorder clause field to improve alignment\n\nThis reduces the unsafe.Sizeof size of a clause from 56 to 48 bytes.","shortMessageHtmlLink":"Reorder clause field to improve alignment"}},{"before":"08c22741da06e6f74a87add3cff9f1b0bbbbd63a","after":"5745b189a78b53daac364151bc4e30d690259f4e","ref":"refs/heads/main","pushedAt":"2024-05-15T23:55:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Prefer range-loops over i-loops","shortMessageHtmlLink":"Prefer range-loops over i-loops"}},{"before":"34d241209b668ec0cfddb31ac7512de05878e4d6","after":"08c22741da06e6f74a87add3cff9f1b0bbbbd63a","ref":"refs/heads/main","pushedAt":"2024-05-15T01:51:00.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Minor speed-up VarOrder.Reinsert\n\nMethod `VarOrder.Reinsert` is called more frequently than `VarOrder.NextDecision`. It is thus more efficient to check if phase saving is enabled when making the decision rather than in `VarOrder.Reinsert`.","shortMessageHtmlLink":"Minor speed-up VarOrder.Reinsert"}},{"before":"adf366818440aa09f1630c6fc3422297362b3862","after":"34d241209b668ec0cfddb31ac7512de05878e4d6","ref":"refs/heads/main","pushedAt":"2024-05-15T01:46:56.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Speed-up propagation by tracking last watched lit\n\nRather than starting the search for a new literal to watch from the beginning, start the search from the position of the last previously watched literal.\n\nThe change yields a ~20% speed improvement on large instance with large clauses. Though, it's important to note that it has drawbacks. First, it introduces some overhead for small clauses (e.g. 3~6 literals). Second, it modifies the behavior of the solver as it impacts propagation order and thus what conflict are analyzed to produce new clauses.\n\nHaving different implementations for clauses of different sizes might help mitigate the first drawback.","shortMessageHtmlLink":"Speed-up propagation by tracking last watched lit"}},{"before":"36de583beb3e32edb7374c40b3b6daf1b3cefb19","after":"adf366818440aa09f1630c6fc3422297362b3862","ref":"refs/heads/main","pushedAt":"2024-05-15T01:38:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Print propagations per sec in millions per sec.","shortMessageHtmlLink":"Print propagations per sec in millions per sec."}},{"before":"9a3abfc977e469adeadbe43a66740f3790429868","after":"36de583beb3e32edb7374c40b3b6daf1b3cefb19","ref":"refs/heads/main","pushedAt":"2024-05-14T10:11:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Remove allocation pool and free \"dead\" slices\n\nCurrently, clauses keep being referenced even after deletion (e.g. in the underlying array of the learnt slice or the the watcher slices). Because of that, many slices of literals were not properly freed by the garbage collector. This commits fixes this issue by \"cutting\" the reference to the slice when a clause is deleted.\n\nAs expected, this change led to a substantial reduction of in-use memory. What was not expected is that the pool of slice is now adding more overhead than help. I think the solver will still benefit of a slice freelist at some point. Though, this would likely have to be a little more tailored than sync.Pool.\n\nAnother change introduced in this commit is the use of a bit mask instead of different booleans to maintain the different status of a clause. This currently saves one byte per clause.","shortMessageHtmlLink":"Remove allocation pool and free \"dead\" slices"}},{"before":"40a324dc22dad91f49c90d5d58c442e6b9ae4a07","after":"9a3abfc977e469adeadbe43a66740f3790429868","ref":"refs/heads/main","pushedAt":"2024-05-13T06:01:13.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Centralize search statistics in their own struct","shortMessageHtmlLink":"Centralize search statistics in their own struct"}},{"before":"cc35084ec3ee2ac9b4f4ee6867b19b3ff2733531","after":"40a324dc22dad91f49c90d5d58c442e6b9ae4a07","ref":"refs/heads/main","pushedAt":"2024-05-13T05:13:02.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Change type of Literal from int to uint32\n\n32bits should be largely sufficient to hold all the literals. For example, the largest instances from the SAT23 competitions do not exceed 20M literals (which is two orders of magnitude lower than 2^32).","shortMessageHtmlLink":"Change type of Literal from int to uint32"}},{"before":"9dd6d40370c6172c8196077d0dc1fb20f5913661","after":"cc35084ec3ee2ac9b4f4ee6867b19b3ff2733531","ref":"refs/heads/main","pushedAt":"2024-05-13T04:57:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Noop simplification of `Solver.analyze`","shortMessageHtmlLink":"Noop simplification of <code>Solver.analyze</code>"}},{"before":"295ca9e18fa50f3e5baa480664fa1576fe31910a","after":"9dd6d40370c6172c8196077d0dc1fb20f5913661","ref":"refs/heads/main","pushedAt":"2024-05-10T07:29:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Simplify function allocSlice","shortMessageHtmlLink":"Simplify function allocSlice"}},{"before":"c63b8de0fa621ea7b89e9540d9fa014f680f8d53","after":"295ca9e18fa50f3e5baa480664fa1576fe31910a","ref":"refs/heads/main","pushedAt":"2024-05-10T05:47:53.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Fix performance bug in allocSlice\n\nFunction allocSlice could return slices with a smaller capacity than what it was required if these slices are pulled from the last pool.\n\nThis wasn't an issue in practice as clauses properly resized their underlying slices. However, this bug led to doing more allocations than necessary (e.g. if the returned slice has a much smaller capacity than what was requested).","shortMessageHtmlLink":"Fix performance bug in allocSlice"}},{"before":"bdad4b3a20bc4051d590e97798b0877db5c211d0","after":"c63b8de0fa621ea7b89e9540d9fa014f680f8d53","ref":"refs/heads/main","pushedAt":"2024-05-10T04:21:42.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Add an option to read gzipped CNF files","shortMessageHtmlLink":"Add an option to read gzipped CNF files"}},{"before":"f489caa9b291262f6e84836a5dfbb59fd803b435","after":"bdad4b3a20bc4051d590e97798b0877db5c211d0","ref":"refs/heads/main","pushedAt":"2024-05-10T03:45:43.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Reduce GC overhead using a pool for clause slices\n\nThis commit introduces the use of `sync.Pool` to manage the clauses' underlying slices. The idea is to allow new clauses to re-use the slice of a previously deleted clause without having to burden the system to allocate a new clause.\n\nThis change results in more than 10X decrease in memory need to solve some large instances. Though, the value of `nPools` still has to be optimized.","shortMessageHtmlLink":"Reduce GC overhead using a pool for clause slices"}},{"before":"a36b74ab5718e6d0f326426a609092b8edc479a1","after":"f489caa9b291262f6e84836a5dfbb59fd803b435","ref":"refs/heads/main","pushedAt":"2024-05-09T02:31:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Implement Glucose-like reduceDB trigger\n\nThis commit changes the condition to trigger a reduction of the clause DB. The new one is more similar to what Glucose 4.1 is doing which will help better compare the performance of YASS with Glucose.","shortMessageHtmlLink":"Implement Glucose-like reduceDB trigger"}},{"before":"fad81271f7f5dec3ef1e00a310e65668d01c8c5f","after":"a36b74ab5718e6d0f326426a609092b8edc479a1","ref":"refs/heads/main","pushedAt":"2024-05-09T01:37:58.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"rhartert","name":"Ren Hartert","path":"/rhartert","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/91352809?s=80&v=4"},"commit":{"message":"Try to assign positive literal by default","shortMessageHtmlLink":"Try to assign positive literal by default"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEW4K9dwA","startCursor":null,"endCursor":null}},"title":"Activity · rhartert/yass"}