078f9d1 | Romain WALLON | 11 May 2021, 19:19:38 UTC | Merge branch 'master' of https://gitlab.ow2.org/sat4j/sat4j into assertion-level | 11 May 2021, 19:19:38 UTC |
ca754f5 | Daniel Le Berre | 08 May 2021, 08:39:28 UTC | Merge branch 'master' of https://gitlab.ow2.org/sat4j/sat4j | 08 May 2021, 08:39:28 UTC |
f0d9a86 | Romain WALLON | 10 February 2021, 15:17:47 UTC | Double bump conflicting and better effectiveness. (cherry picked from commit b872caa503b14baacafc4c573408c56aa9b20b57) | 08 May 2021, 08:37:59 UTC |
bee57b1 | Romain WALLON | 06 May 2021, 18:45:11 UTC | :bug: Fixes the choice of literals to weaken. | 06 May 2021, 18:45:19 UTC |
d74050f | Romain WALLON | 03 May 2021, 19:07:13 UTC | :sparkles: New strategies for stopping and weakening. | 03 May 2021, 19:07:13 UTC |
83509e0 | Romain WALLON | 29 April 2021, 18:31:13 UTC | Merge branch 'master' into assertion-level | 29 April 2021, 18:31:13 UTC |
a253421 | Romain WALLON | 22 April 2021, 19:21:09 UTC | :bug: Pigeons in a single conflict. | 22 April 2021, 19:21:09 UTC |
f7f7594 | Romain WALLON | 20 April 2021, 10:07:02 UTC | :bug: Some bugs are now fixed. | 20 April 2021, 10:07:08 UTC |
4390193 | Romain WALLON | 19 April 2021, 08:09:17 UTC | :sparkles: Stats for assertion | 19 April 2021, 08:09:17 UTC |
4e3ed44 | Romain WALLON | 15 April 2021, 16:28:19 UTC | :sparkles: First attempt to compute the exact slack when continuing conflict analysis. | 15 April 2021, 16:28:19 UTC |
4a3e7d8 | Daniel Le Berre | 12 April 2021, 07:03:38 UTC | Removing ow2 staging repository | 12 April 2021, 07:03:38 UTC |
2e54e44 | Daniel Le Berre | 11 April 2021, 08:04:05 UTC | log properly exception messages. | 11 April 2021, 08:04:05 UTC |
7d51fde | Daniel Le Berre | 10 April 2021, 14:49:05 UTC | Refactored propagatePI: it is void a void method. | 10 April 2021, 14:49:05 UTC |
c84cb5b | Daniel Le Berre | 10 April 2021, 13:09:36 UTC | Make Explainer serializable. | 10 April 2021, 13:09:36 UTC |
9f0bb8e | Daniel Le Berre | 10 April 2021, 12:57:18 UTC | Fix serialization violation (sonarqube). | 10 April 2021, 12:57:18 UTC |
2600793 | Daniel Le Berre | 10 April 2021, 12:53:19 UTC | Fix deprecated code and use more adapted assertEquals. | 10 April 2021, 12:53:19 UTC |
982fc24 | Romain WALLON | 10 April 2021, 12:39:37 UTC | Merge branch 'master' into assertion-level | 10 April 2021, 12:39:37 UTC |
1824d4f | Daniel Le Berre | 10 April 2021, 12:31:31 UTC | Remove empty tests cases. | 10 April 2021, 12:31:31 UTC |
b96720d | Daniel Le Berre | 10 April 2021, 12:30:37 UTC | Add missing assertion. | 10 April 2021, 12:30:37 UTC |
66ef175 | Daniel Le Berre | 10 April 2021, 11:10:11 UTC | Fix test case. | 10 April 2021, 11:10:11 UTC |
49895cd | Daniel Le Berre | 10 April 2021, 11:07:22 UTC | Removed deprecated class. | 10 April 2021, 11:07:22 UTC |
ce1061d | Daniel Le Berre | 10 April 2021, 10:25:49 UTC | Add missing assertions. | 10 April 2021, 10:25:49 UTC |
a2117f8 | Daniel Le Berre | 10 April 2021, 10:18:17 UTC | Add missing assertion. | 10 April 2021, 10:18:17 UTC |
3b2122a | Daniel Le Berre | 10 April 2021, 10:02:42 UTC | Add missing assertions. | 10 April 2021, 10:02:42 UTC |
5e65dab | Daniel Le Berre | 10 April 2021, 09:50:17 UTC | Add assertions in bug report test | 10 April 2021, 09:50:17 UTC |
5e1d42a | Daniel Le Berre | 10 April 2021, 09:45:43 UTC | Remove empty test cases. | 10 April 2021, 09:45:43 UTC |
8d4679f | Daniel Le Berre | 10 April 2021, 09:43:41 UTC | Add missing assertions in bug report test. | 10 April 2021, 09:43:41 UTC |
c12a031 | Daniel Le Berre | 10 April 2021, 09:33:00 UTC | Introduce assertions in bug report tests | 10 April 2021, 09:33:00 UTC |
824bfaf | Daniel Le Berre | 10 April 2021, 09:24:51 UTC | Add assertion in test case. | 10 April 2021, 09:24:51 UTC |
28aded5 | Daniel Le Berre | 10 April 2021, 08:55:40 UTC | Moved prefixes in an enum. No more constants in ILauncherMode. | 10 April 2021, 08:55:40 UTC |
845d056 | Daniel Le Berre | 10 April 2021, 08:13:56 UTC | Add details regarding the name of the solver having unit clauses problem. | 10 April 2021, 08:13:56 UTC |
77c2776 | Daniel Le Berre | 10 April 2021, 07:44:51 UTC | update dependencies for java 16 | 10 April 2021, 07:44:51 UTC |
fd6cb9d | Daniel Le Berre | 10 April 2021, 07:36:57 UTC | bump mockito version to 3.8.25 | 10 April 2021, 07:36:57 UTC |
548fddc | Daniel Le Berre | 09 April 2021, 10:54:38 UTC | testing ow2 staging 1.5.1 parent pom | 09 April 2021, 10:54:38 UTC |
00d5623 | Daniel Le Berre | 09 April 2021, 08:58:48 UTC | Update maven 3.6.3 -> 3.8.1 | 09 April 2021, 08:58:48 UTC |
04589bb | Daniel Le Berre | 09 April 2021, 08:55:35 UTC | Using ow2 parent pom 1.5.1-snapshot for maven 3.8.1 | 09 April 2021, 08:55:35 UTC |
2938223 | Romain WALLON | 08 April 2021, 15:50:09 UTC | :bug: Fixes some bugs. | 08 April 2021, 15:50:09 UTC |
29ea179 | Romain WALLON | 07 April 2021, 14:10:18 UTC | :sparkles: Adds the selection of the literal to remove. | 07 April 2021, 14:10:18 UTC |
9939986 | Romain WALLON | 06 April 2021, 18:47:20 UTC | Merge branch 'master' into assertion-level | 06 April 2021, 18:47:20 UTC |
b086d71 | Romain WALLON | 04 March 2021, 14:01:26 UTC | Some fixes and TODO for coming implementations. | 04 March 2021, 14:01:26 UTC |
facdc8b | Daniel Le Berre | 02 March 2021, 13:05:51 UTC | WIP: fix for #165. Need to check how much it affects the solver performance. | 03 March 2021, 06:50:11 UTC |
83133f7 | Daniel Le Berre | 25 February 2021, 10:50:32 UTC | Fix for #164 | 25 February 2021, 10:50:32 UTC |
4a45855 | Daniel Le Berre | 24 February 2021, 06:41:00 UTC | Rename the field lbdTimer into glucoseTimer to make clear it is using the Glucose scheme. | 24 February 2021, 06:41:00 UTC |
250cdf8 | Daniel Le Berre | 24 February 2021, 06:38:07 UTC | Renamed LBDConflictTimer as GlucoseConflictTimer. This scheme is not related to LBD, but to the way Glucose is performing it's clauses cleaning checks. | 24 February 2021, 06:38:07 UTC |
502d199 | Daniel Le Berre | 22 February 2021, 20:09:42 UTC | Remove spurious debug message | 22 February 2021, 20:09:42 UTC |
8c4f55e | Daniel Le Berre | 22 February 2021, 17:58:31 UTC | Test case for #162 | 22 February 2021, 17:58:31 UTC |
4897e44 | Daniel Le Berre | 22 February 2021, 17:57:41 UTC | First steps to fix #162 | 22 February 2021, 17:57:41 UTC |
d8c6f48 | Romain WALLON | 21 February 2021, 20:47:27 UTC | :sparkles: Adds the weakening for preserving the assertion level. | 21 February 2021, 20:47:27 UTC |
d112348 | Romain WALLON | 17 February 2021, 09:22:35 UTC | Creates a strategy for continuing conflict analysis. | 17 February 2021, 09:22:35 UTC |
dbb8901 | Daniel Le Berre | 13 January 2021, 13:18:37 UTC | Updated CI for Sat4j 3.0: Java 11+ | 13 January 2021, 13:18:37 UTC |
eba76d9 | Daniel Le Berre | 13 January 2021, 13:18:05 UTC | Heading to Sat4j 3.0 | 13 January 2021, 13:18:05 UTC |
bf44d05 | Daniel Le Berre | 14 December 2020, 17:12:27 UTC | release 2.3.6 | 14 December 2020, 17:12:27 UTC |
2bcdcb3 | Daniel Le Berre | 08 December 2020, 06:40:25 UTC | ACLIB files for Sat4j | 08 December 2020, 06:40:25 UTC |
4d2dea0 | Daniel Le Berre | 31 October 2020, 09:12:06 UTC | Allow DetectCards to enumerate solutions. | 31 October 2020, 09:12:06 UTC |
b39dab5 | Daniel Le Berre | 31 October 2020, 09:11:05 UTC | Feature annotation. | 31 October 2020, 09:11:05 UTC |
ee9c972 | Daniel Le Berre | 31 October 2020, 09:10:16 UTC | Allow nondeterministic behavior of the solver. | 31 October 2020, 09:10:16 UTC |
4d8c557 | Daniel Le Berre | 04 October 2020, 20:13:55 UTC | Merge branch 'master' of https://gitlab.ow2.org/sat4j/sat4j | 04 October 2020, 20:13:55 UTC |
c2ab17e | Daniel Le Berre | 04 October 2020, 20:12:39 UTC | settings to Java 7 instead of 6 | 04 October 2020, 20:12:39 UTC |
a5ae1b2 | Daniel Le Berre | 04 October 2020, 20:11:38 UTC | Rebuilt random solver. | 04 October 2020, 20:11:38 UTC |
aea5894 | Daniel Le Berre | 04 October 2020, 20:10:38 UTC | Improved debug display | 04 October 2020, 20:10:38 UTC |
b0e95ae | Daniel Le Berre | 04 October 2020, 20:09:15 UTC | Allow non deterministic behavior. | 04 October 2020, 20:09:15 UTC |
0e6a814 | Daniel Le Berre | 04 October 2020, 20:06:13 UTC | Allow setting timeout on core java launcher. | 04 October 2020, 20:06:13 UTC |
4e856a4 | Daniel Le Berre | 04 October 2020, 10:02:19 UTC | Merge branch 'cdcl-strategies' into 'master' Cdcl strategies See merge request sat4j/sat4j!6 | 04 October 2020, 10:02:19 UTC |
c3d638a | Romain WALLON | 18 September 2020, 11:18:21 UTC | Improves the backjump level by looking to falsified literals only | 18 September 2020, 11:18:21 UTC |
91bce9d | Romain Wallon | 13 September 2020, 20:51:14 UTC | Considers watched literals in resolution based solvers for Both-like solvers | 13 September 2020, 20:51:14 UTC |
63107ad | Daniel Le Berre | 10 September 2020, 12:52:34 UTC | Allow a more sober CPU consumption in Both PB solver. | 10 September 2020, 12:52:34 UTC |
985bae7 | Romain WALLON | 09 September 2020, 09:24:18 UTC | Fixes the solver instantiated for RoundingSatPOS2020 | 09 September 2020, 09:24:18 UTC |
a94fbad | Romain WALLON | 09 September 2020, 08:57:46 UTC | Adds factories for the new configurations presented in 2020. | 09 September 2020, 08:57:46 UTC |
f4790fb | Romain Wallon | 11 August 2020, 15:04:42 UTC | Adds a slack based LCDS | 15 August 2020, 11:28:09 UTC |
a5f7588 | Romain Wallon | 07 August 2020, 12:31:58 UTC | Adds back a CLI option that had been removed | 07 August 2020, 12:31:58 UTC |
7ce2784 | Romain Wallon | 07 August 2020, 11:06:29 UTC | Ads some more bumping and LCD strategies | 07 August 2020, 11:06:29 UTC |
3c078bd | Romain Wallon | 05 August 2020, 09:00:03 UTC | :sparkles: Adds the LBD-effective measure | 05 August 2020, 09:00:03 UTC |
297871a | Romain Wallon | 28 July 2020, 16:09:29 UTC | Adds a new bump strategy | 28 July 2020, 16:09:29 UTC |
6d880cc | Romain Wallon | 28 July 2020, 08:54:12 UTC | Adds more statistics to the different LCDSs. | 28 July 2020, 08:54:12 UTC |
c091d76 | Daniel Le Berre | 26 July 2020, 09:54:25 UTC | Fixed test case. | 26 July 2020, 09:54:25 UTC |
ae418f1 | Daniel Le Berre | 26 July 2020, 08:02:07 UTC | Can now detect learned unit clause. | 26 July 2020, 08:02:07 UTC |
408542e | Romain WALLON | 24 July 2020, 09:27:17 UTC | Adds the bumper for effective literals only. | 24 July 2020, 09:33:07 UTC |
e567627 | Daniel Le Berre | 22 July 2020, 15:48:48 UTC | Annotated prime implicant strategy | 22 July 2020, 15:48:48 UTC |
3fc2451 | Romain WALLON | 15 July 2020, 11:11:45 UTC | More statistics for the different strategies | 15 July 2020, 11:11:45 UTC |
e19a5e1 | Romain Wallon | 02 July 2020, 20:27:01 UTC | Merge branch 'weakening-investigations' into cdcl-strategies | 02 July 2020, 20:27:01 UTC |
0f34a5c | Romain Wallon | 02 July 2020, 20:26:09 UTC | Another fix for Java 8 | 02 July 2020, 20:26:09 UTC |
713a084 | Romain Wallon | 02 July 2020, 19:45:39 UTC | Merge branch 'cdcl-strategies' of https://gitlab.ow2.org/sat4j/sat4j into cdcl-strategies | 02 July 2020, 19:45:39 UTC |
e72e867 | Romain Wallon | 02 July 2020, 19:45:04 UTC | Merge branch 'weakening-investigations' into cdcl-strategies | 02 July 2020, 19:45:04 UTC |
d89b7c9 | Romain Wallon | 02 July 2020, 19:44:28 UTC | Fixes an issue with Java 8 | 02 July 2020, 19:44:28 UTC |
57ca63c | Romain Wallon | 22 June 2020, 16:54:55 UTC | Fixes a missing method and uses LBD-based restarts in resolution-based solvers | 22 June 2020, 16:54:55 UTC |
9f33062 | Romain Wallon | 20 June 2020, 13:17:34 UTC | Merge branch 'master' into cdcl-strategies | 20 June 2020, 13:17:34 UTC |
81fa78b | Romain Wallon | 20 June 2020, 13:16:52 UTC | Removes an unused import. | 20 June 2020, 13:16:52 UTC |
22374e5 | Daniel Le Berre | 10 June 2020, 12:48:03 UTC | Added annotation on the method, not the type for ManyCore. | 10 June 2020, 12:48:03 UTC |
22f5a2a | Daniel Le Berre | 10 June 2020, 09:29:07 UTC | Removed incorrect annotation. | 10 June 2020, 09:29:07 UTC |
e1e0122 | Daniel Le Berre | 09 June 2020, 21:06:29 UTC | Add solutionlistener feature. | 09 June 2020, 21:06:29 UTC |
b7ea93a | Daniel Le Berre | 09 June 2020, 21:01:46 UTC | completed SearchListener. Added solver feature. | 09 June 2020, 21:01:46 UTC |
34cbcb2 | Daniel Le Berre | 09 June 2020, 20:45:28 UTC | Added ne reader feature. | 09 June 2020, 20:45:28 UTC |
b00f768 | Daniel Le Berre | 09 June 2020, 20:41:00 UTC | Add missing annotation for new Order feature. | 09 June 2020, 20:41:00 UTC |
8e74b60 | Daniel Le Berre | 09 June 2020, 20:36:57 UTC | Improved output for Anthony. | 09 June 2020, 20:36:57 UTC |
7d9f74d | Daniel Le Berre | 09 June 2020, 20:34:20 UTC | Add constraint feature. | 09 June 2020, 20:35:04 UTC |
355a053 | Daniel Le Berre | 04 June 2020, 07:01:13 UTC | Allow to force the heuristics using an external file. | 04 June 2020, 07:01:13 UTC |
a5a5be9 | Romain Wallon | 23 May 2020, 13:11:19 UTC | Adds the bump strategies regarding partial assignments | 23 May 2020, 13:11:19 UTC |
6aacef0 | Romain Wallon | 04 May 2020, 14:59:13 UTC | Merge branch 'master' of https://gitlab.ow2.org/sat4j/sat4j into cdcl-strategies | 04 May 2020, 14:59:13 UTC |
29fdce5 | Romain Wallon | 04 May 2020, 14:57:51 UTC | Merges master into cdcl-strategies. | 04 May 2020, 14:57:51 UTC |
42a72c2 | Daniel Le Berre | 01 May 2020, 17:58:58 UTC | Fix for #161 | 01 May 2020, 17:58:58 UTC |