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 |
a2030a5 | Daniel Le Berre | 01 May 2020, 14:37:57 UTC | Fix implementations of LCDS breaking encapsulation. | 01 May 2020, 14:37:57 UTC |
87aed1d | Daniel Le Berre | 30 April 2020, 19:10:24 UTC | Add DECIDED_CYCLE category | 30 April 2020, 19:10:24 UTC |
21e9739 | Daniel Le Berre | 30 April 2020, 19:09:26 UTC | Added test file for #161 | 30 April 2020, 19:09:26 UTC |
d6dafed | Daniel Le Berre | 29 April 2020, 17:44:54 UTC | :bug: test case showing bug #161 | 29 April 2020, 17:44:54 UTC |
c30a037 | Daniel Le Berre | 23 April 2020, 14:17:58 UTC | renamed field. | 23 April 2020, 14:17:58 UTC |
a901a1e | Daniel Le Berre | 23 April 2020, 14:15:32 UTC | decided_propagated_learned + refactoring origin. | 23 April 2020, 14:15:50 UTC |
94b8f65 | Daniel Le Berre | 22 April 2020, 11:19:35 UTC | Add missing class. | 22 April 2020, 11:19:35 UTC |
f3ecade | Daniel Le Berre | 22 April 2020, 11:19:19 UTC | More features identified in the code. | 22 April 2020, 11:19:19 UTC |
c2a6a1c | Daniel Le Berre | 22 April 2020, 10:29:46 UTC | Made UnitClauseConsumer the only interface to implement for ManyCore (instead of SearchListener). | 22 April 2020, 10:29:46 UTC |
93739f8 | Daniel Le Berre | 22 April 2020, 08:59:41 UTC | Compute only decided propagated when color parameter is given (else it breaks the state of the solver when reused afterwards). | 22 April 2020, 08:59:41 UTC |
96192bb | Daniel Le Berre | 22 April 2020, 07:36:13 UTC | Fix code to maintain invariants. | 22 April 2020, 07:36:13 UTC |
bdd1bd3 | Daniel Le Berre | 21 April 2020, 19:02:32 UTC | Add a few feature annotations. | 21 April 2020, 19:02:32 UTC |
4c49fb2 | Daniel Le Berre | 21 April 2020, 19:01:02 UTC | Rename name() into value() to simplify use with default parent. | 21 April 2020, 19:01:02 UTC |
c67f55e | Daniel Le Berre | 21 April 2020, 15:55:52 UTC | Annotation to explain the design of Sat4j | 21 April 2020, 15:55:52 UTC |
08ec8f5 | Daniel Le Berre | 18 April 2020, 09:10:47 UTC | Move colors as a property of the enumeration. | 18 April 2020, 09:10:47 UTC |
f6d084d | Daniel Le Berre | 18 April 2020, 08:57:15 UTC | Fix decided_propagated computation (mixup p and q) | 18 April 2020, 08:57:15 UTC |
4265eae | Daniel Le Berre | 17 April 2020, 13:58:43 UTC | Fixing decided_propagated computation. | 17 April 2020, 13:58:43 UTC |
ad98282 | Daniel Le Berre | 17 April 2020, 12:56:54 UTC | Added missing class | 17 April 2020, 12:56:54 UTC |
2ca18bb | Daniel Le Berre | 17 April 2020, 12:49:25 UTC | Added decided/propagated. | 17 April 2020, 12:49:25 UTC |
a4bc472 | Romain Wallon | 15 April 2020, 12:48:33 UTC | Merges master into cdcl-strategies | 15 April 2020, 12:48:33 UTC |
8784f11 | Daniel Le Berre | 10 April 2020, 08:15:52 UTC | Blue instead of purple + stats. | 10 April 2020, 08:15:52 UTC |
03a4b84 | Daniel Le Berre | 07 April 2020, 07:43:55 UTC | Updated outdated PB files. | 07 April 2020, 07:43:55 UTC |
e836ecb | Daniel Le Berre | 07 April 2020, 07:01:33 UTC | Better support for literal assignment origin. | 07 April 2020, 07:01:33 UTC |
2cd4cbe | Daniel Le Berre | 06 April 2020, 17:17:32 UTC | Fix LBD computation with unassigned literals (when used with PB constraints). | 06 April 2020, 17:17:32 UTC |
f39e392 | Daniel Le Berre | 06 April 2020, 15:35:04 UTC | Allow displaying colored models using -Dcolor system parameter. | 06 April 2020, 15:35:04 UTC |
71c7ab4 | Daniel Le Berre | 30 March 2020, 12:36:56 UTC | Default LCDS is ActivityBased for PB constraints. | 30 March 2020, 12:36:56 UTC |
f8232e6 | Daniel Le Berre | 30 March 2020, 12:27:50 UTC | Javadoc regarding LBD computation in LCDS. | 30 March 2020, 12:27:50 UTC |
88cb4b1 | Daniel Le Berre | 30 March 2020, 12:19:35 UTC | Merge branch 'master' of https://gitlab.ow2.org/sat4j/sat4j.git | 30 March 2020, 12:19:35 UTC |
4d85c81 | Daniel Le Berre | 30 March 2020, 12:19:13 UTC | call onClauseLearning() in SolverCP conflict analysis. | 30 March 2020, 12:19:13 UTC |
f6f7d3c | Romain Wallon | 26 March 2020, 14:30:35 UTC | Allows to check whether a PB constraint is currently satisfied. | 26 March 2020, 14:30:35 UTC |
3dc429a | Romain Wallon | 20 March 2020, 11:30:49 UTC | Improves OPB parsing: number of constraints and Exception handling. | 20 March 2020, 11:30:49 UTC |
f47469f | Romain WALLON | 13 March 2020, 09:43:38 UTC | Adds some new strategies for the CDCL algorithm. | 13 March 2020, 09:43:38 UTC |
10f70aa | Daniel Le Berre | 11 March 2020, 14:20:25 UTC | Add a getter to LCDS | 11 March 2020, 14:20:25 UTC |
2a009b3 | Daniel Le Berre | 10 March 2020, 12:33:03 UTC | No more solver duplicated field. | 10 March 2020, 12:33:03 UTC |
1d6996c | Daniel Le Berre | 09 March 2020, 12:48:27 UTC | Use setActivity instead of incActivity (even if it is the same behavior in that particular case). | 09 March 2020, 12:48:27 UTC |
d988264 | Romain WALLON | 06 March 2020, 16:10:47 UTC | Merge branch 'master' into weakening-investigations | 06 March 2020, 16:10:47 UTC |
866a97e | Romain WALLON | 06 March 2020, 16:10:18 UTC | Adds the RoundingSat approaches to the solver factory | 06 March 2020, 16:10:18 UTC |
40960df | Daniel Le Berre | 04 March 2020, 15:31:22 UTC | Now provide access to the winner id. | 04 March 2020, 15:31:22 UTC |
998908f | Romain WALLON | 04 March 2020, 09:00:10 UTC | Merge branch 'master' into weakening-investigations | 04 March 2020, 09:00:10 UTC |
faeea89 | Daniel Le Berre | 03 March 2020, 17:31:53 UTC | Merge branch 'master' of https://gitlab.ow2.org/sat4j/sat4j | 03 March 2020, 17:31:53 UTC |
fc6db1f | Daniel Le Berre | 03 March 2020, 17:31:29 UTC | Add missing use of assumptions | 03 March 2020, 17:31:29 UTC |
ed3ca96 | Romain WALLON | 02 March 2020, 13:00:56 UTC | Considers assumptions when invoking `preventTheSameDecisionsToBeMade' | 02 March 2020, 13:00:56 UTC |
f1b4696 | Romain WALLON | 28 February 2020, 15:54:12 UTC | Encapsulates the starting of the mapping. | 28 February 2020, 15:54:12 UTC |
6dc0731 | Romain WALLON | 28 February 2020, 15:51:23 UTC | Still more freedom for subclassing readers. | 28 February 2020, 15:51:23 UTC |
8d54a5f | Romain WALLON | 28 February 2020, 14:04:22 UTC | Gives more freedom to subclass readers in third-party softwares. | 28 February 2020, 14:04:22 UTC |
234f5de | Romain WALLON | 28 February 2020, 08:54:32 UTC | Adds the possibility to apply RS approach on the conflict only | 28 February 2020, 08:54:32 UTC |
ea2aa23 | Romain WALLON | 21 February 2020, 16:52:42 UTC | Fixes some bugs in the implementation of RoundingSat approach. | 21 February 2020, 16:52:42 UTC |
9e80879 | Romain Wallon | 16 February 2020, 12:12:11 UTC | Adds the division on both sides of the resolution. | 16 February 2020, 12:12:11 UTC |
3951cad | Romain WALLON | 14 February 2020, 14:10:58 UTC | Clarifies that propagating on PB constraints does not guarantee to detect all conflicts | 14 February 2020, 14:10:58 UTC |
4f9abd5 | Romain WALLON | 14 February 2020, 14:07:31 UTC | Some improvements for weaken-to-clash | 14 February 2020, 14:07:31 UTC |
d4e5c7b | Romain WALLON | 14 February 2020, 10:09:14 UTC | Fixes some bugs in the new approaches. | 14 February 2020, 10:09:14 UTC |