github.com/QuiltMC/quilt-loader-sat4j commits

IN PROGRESS - issue SAT-38: Investigate usage of plain CNF rather than custom cardinality of PB constraints

http://jira.ow2.org/browse/SAT-38
First implementation of SAT-38

git-svn-id: svn+ssh://svn.forge...

1f39109a408cf40ed3f27e31bf3a6b62706f4824 authored about 13 years ago by sroussel <sroussel@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

IN PROGRESS - issue SAT-38: Investigate usage of plain CNF rather than custom cardinality of PB constraints

http://jira.ow2.org/browse/SAT-38
First implementation of SAT-38

git-svn-id: svn+ssh://svn.forge...

7d38034519f85e8f6631fddf372fe70e145f043a authored about 13 years ago by sroussel <sroussel@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

REally fixed the issue with ToString().

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1076 ba638df5-4473-46d1-82f8-c...

4f9097c418f746307840ba7ef41395b8befad52f authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

TosTring() method calls toString("") to allow an easier management of the toString() method in the subclasses.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1075 ba638df5-4473-46d1-82f8-c...

aeedff45d96a8c9fb24de45f90d2d858b90fbe40 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Updated dependency to rhino 1.7R2.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1074 ba638df5-4473-46d1-82f8-...

c3f27ff7597f4b2d0dc95b30270d5d0e28b8d818 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Updated test case to show new behavior.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1073 ba638df5-4473-46d1-82f8-c...

656edb31fbe25f733e225a5edddad5a8bc8ed04f authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

return only models with variables appearing in the formula.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1072 ba638df5-4473-46d1-82f8-c...

3828e99c14f031b8d038df55688766f784c30a77 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Take into account new model()/modelWithInternalVariables() methods.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1071 ba638df5-4473-46d1-82f8-c...

34ee64dfc7149b406c71b3ab854fe34740e2a478 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Fix testcase with implicit call to newVar().

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1070 ba638df5-4473-46d1-82f8-c...

cb8d2d01f50cf730c42108d468c840d27fee886c authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Updated test case to the expected behavior, not implemented one :)

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1069 ba638df5-4473-46d1-82f8-c...

610038e499902925c7db18d6fe10a0709e085b06 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Fix solver to return a model with only the variables used when new variables are added using nextFreeVarId().

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1068 ba638df5-4473-46d1-82f8-c...

1b6247c7212f062bcb9f546f28a403c0d6a4c88f authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Display declared vs internal number of variables on the console.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1067 ba638df5-4473-46d1-82f8-c...

d9031b0daeb7dedd099aa28f09178b2a261addd5 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Implement SAT43 for MAXSAT.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1066 ba638df5-4473-46d1-82f8-c...

4066cb3cbf5dae1a1383baec71542b937476a94b authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Tests for SAT43.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1065 ba638df5-4473-46d1-82f8-c...

b5457498facf68a55174ab03c072d3e395ade081 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Code to implement SAT43.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1064 ba638df5-4473-46d1-82f8-c...

3af032a08f110b7fde587aa77ecdc11865cabd29 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Remove notion of wall in glucose.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1063 ba638df5-4473-46d1-82f8-c...

dd36b2b7135730447f27d658f5019e1704e5c90a authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Code to implement for SAT-42.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1062 ba638df5-4473-46d1-82f8-c...

725b46e8352ee79d81147c8982ac9465c2e084b0 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Prevent UnitClause removal during simplifyDB (was throwing an exception).

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1061 ba638df5-4473-46d1-82f8-c...

e08bb4525a91eb7aa3d04a6d28ee7132c14237cd authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

LitsToCoefs structure added to remaining MaxWatchXXXPB constraints

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1060 ba638df5-4473-46d1-82f8-c...

7de07511eae1962ba5198bb649ee315708fd6fb2 authored about 13 years ago by parrain <parrain@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

LongWatchPBCP constructors created

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1059 ba638df5-4473-46d1-82f8-c...

4b431d6b9084269162c4549d69cfc65efc252f8e authored about 13 years ago by parrain <parrain@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Pull up mapping to the MaxWatchPbLong class.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1058 ba638df5-4473-46d1-82f8-c...

560eaae3812348aec57b5055c0c5534f1370ea26 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

First implementation of SAT-41.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1057 ba638df5-4473-46d1-82f8-c...

e18b958f9a14b80c52d850dd952d4192394be1de authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

from MaxWatchLongCP to MaxWatchLong

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1056 ba638df5-4473-46d1-82f8-c...

5d056a5bd18e89c9502c7a769ad306198bb10455 authored about 13 years ago by parrain <parrain@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Fix for bug SAT40.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1055 ba638df5-4473-46d1-82f8-c...

74d7bd0a13b2bf432f4740b852e4883cb01ea826 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Made the class non final, to be able to create a subclass taking account the objective function.

RandomWalks counters is not reset at each init call (call to isSatisfiable()) but when the order ...

933d3284c0d463b2fb7452728d608b42c4ef342d authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

equals fixed

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1053 ba638df5-4473-46d1-82f8-c...

93b2ca28f6f9f8fc008ab6dc73c4aff78dd79eb4 authored about 13 years ago by parrain <parrain@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Moved ConstrGroup to org.sat4j.core to avoid cycles (thanks sonar).

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1052 ba638df5-4473-46d1-82f8-c...

8935c05829a5e8ae7322f9f4ccd13c39890c38a8 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Moved ConstrGroup to org.sat4j.core to avoid cycles (thanks sonar).

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1051 ba638df5-4473-46d1-82f8-c...

4274127a8ddda5f7bd2db0d574bd8ed12dd71d71 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Moved ConstrGroup to org.sat4j.core to avoid cycles (thanks sonar).

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1050 ba638df5-4473-46d1-82f8-c...

680d29011b71480ad79078609e6f4be46fa2cd16 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

ClausesCardConstr data structures factories cleaned. All dsf now inherit from AbstractPBClauseCardConstrDataStructure.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1049 ba638df5-4473-46d1-82f8-c...

e2cc38434acf92824bdf06e9102f5c195efd93e1 authored about 13 years ago by parrain <parrain@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Implementation of exactly card constr.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1048 ba638df5-4473-46d1-82f8-c...

87dbf3a5502baee69b9168a26c2ed30f3c807258 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Temporary implementation of int based API.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1047 ba638df5-4473-46d1-82f8-c...

23d30f2f1b034d0ffd729eb6bd0fc4ce051611aa authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Added test cases for explanation support with exactly.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1046 ba638df5-4473-46d1-82f8-c...

79e47509698f89eb21746944cd698f514f577680 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Made the Xplain tests reusable for PB case.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1045 ba638df5-4473-46d1-82f8-c...

d08dc7997600fe81e8462597f3aee68276738204 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Added a message in the exception to point out the developer toward the XplainPB class.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1044 ba638df5-4473-46d1-82f8-c...

038fe05947def397e619b11c2255d7ce9f768a3c authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

throws an exception when trying to explain an exactly constraint.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1043 ba638df5-4473-46d1-82f8-c...

abeaac0f01bfa99f06647cbc722f51c15481d83a authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Added a toString() method.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1042 ba638df5-4473-46d1-82f8-c...

b1ba06270e8020db9d83f20703e42d4edfd5dd7f authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Added new methods addAtLeast/addAtMost/addExactly in the PB solver. It should be must clearer now for the end user which method to call for creating a constraint.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1041 ba638df5-4473-46d1-82f8-c...

4bd3f79213d5b06c9bc2a3a8d7941f46d68b021c authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Change due to the move of ConstrGroup in org.sat4j.specs

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1040 ba638df5-4473-46d1-82f8-c...

18bd14949e8dd203f08f8071b2564b56d982000d authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Fix for bug SAT-39: there is now a method addExactly(IVecInt,int) that creates a constraint that should satisfy exactly n literals.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1039 ba638df5-4473-46d1-82f8-c...

2f069322058b4e6337f06d62f5f77dcb761871b7 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Support at most constraints with one literal only.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1038 ba638df5-4473-46d1-82f8-c...

2f2cce2fac967bd96911804bce1ead05fb6a824c authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Added support for clauses in AtLeast card constraints.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1037 ba638df5-4473-46d1-82f8-c...

54cb049c5b2fade39dd7943525699d11093fe248 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

New potential fix for SAT37: the wrong code ran on functional tests.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1036 ba638df5-4473-46d1-82f8-c...

07e7e5c67ccc7a7b845c8182aa8c9aafd20b5b57 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Reverted back code added to solve BugSAT37.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1035 ba638df5-4473-46d1-82f8-c...

8a33a6b713316414a605c6aaaffb89806ca1f010 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Another try in solving bug SAT37.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1034 ba638df5-4473-46d1-82f8-c...

f0b3713b732e2dbc7c05a3e59837c7a43f0a814a authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Reverted change: makes the solver incorrect :(

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1033 ba638df5-4473-46d1-82f8-c...

e1c10cd99bfed3e91131dfc14d770b170a9d1126 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Reset qhead to zero before starting search.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1032 ba638df5-4473-46d1-82f8-c...

f22e3a61ec0ee31dd2ecde7c3896075c4d451581 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

The MUS engine does no longer skip duplicated contiguous entries (results in wrong answers during MUS competition).

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1031 ba638df5-4473-46d1-82f8-c...

6fdb4cc20079feb2a10786e0632f3d04d0cca4f8 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Allow Xplain engine to skip removal of duplicated entries. During the MUS competition, some benchmarks had duplicated continuous clauses.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1030 ba638df5-4473-46d1-82f8-c...

f02eceb6bc6647a5722c7c1f19acad80cffa0cd0 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Fix for bug SAT37.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1029 ba638df5-4473-46d1-82f8-c...

15681d8237e273dab8749b303b06b057c30fbc23 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Test case provided by Axel on the forum describing bug SAT37.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1028 ba638df5-4473-46d1-82f8-c...

7bec6dc227e80af9fead6de5564401d629e085fb authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Fixed the computation for the speed of the solver.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1027 ba638df5-4473-46d1-82f8-c...

3eef6a3a9deb9a9888a636d00ea706100eadda40 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Added PB solver decorator with clausal cardinalities representation.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1026 ba638df5-4473-46d1-82f8-c...

207bd7ee3ee8300c26a96f1e56e219df70e79542 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

First implementation of a full clausal representation of cardinality constraints using sequential counters.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1025 ba638df5-4473-46d1-82f8-c...

d32ac09435729b2e85c77d9b92f6dd53220c0499 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Test case for clausal cardinalities representation.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1024 ba638df5-4473-46d1-82f8-c...

0d5a7e82435947b5aa25a3ee90336ada45a5b45a authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Added comment to clarify that card constraints are expected to be of "At Least" form.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1023 ba638df5-4473-46d1-82f8-c...

158587f8eeb8e59e3171123995f3c676ba4cca33 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Added a new constructor to allow the user to provide a nice string output of the solvers.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1022 ba638df5-4473-46d1-82f8-c...

0627214b3b1d2bb4144ae73aea6bcbcf31031115 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Changed visibility of utility methods.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1021 ba638df5-4473-46d1-82f8-c...

2c0c33b002f64dbdf4242e88b4dabd4ad8caa643 authored about 13 years ago by lonca <lonca@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Allow ConstrGroup to contain null.

Added a new getSolvers() method.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/tru...

0a2bc7f06909ee8518d630d716af40a22ae0ef81 authored about 13 years ago by lonca <lonca@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Removed flushing. Does not have any effect regarding OOM exception.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1019 ba638df5-4473-46d1-82f8-c...

030a819c18d2b5d290e69aba7ffdc8e7a2210a94 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Added missing static in NO_NEGATION.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1018 ba638df5-4473-46d1-82f8-c...

843c94a5607ed8506ab42589286213b803bacd4c authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Flush the output to avoid buffering too much content when the solution is large.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1017 ba638df5-4473-46d1-82f8-c...

219210abba6002f73c6c94eebc7185d80be493d6 authored about 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Replaced back MinWatch by MaxWatch.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1016 ba638df5-4473-46d1-82f8-c...

27659ddb330b85228a1741062078acd1347cc439 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

enabled back expensive simplification in the solver.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1015 ba638df5-4473-46d1-82f8-c...

6bb4c53401501b3e07b0abca805984ff315e73b3 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Enabled back shortcut for conflict analysis and card and PB constraints.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1014 ba638df5-4473-46d1-82f8-c...

2f52820f198f07db0be8e141a7873e9a54eed164 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Default solver no longer uses reason simplification.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1013 ba638df5-4473-46d1-82f8-c...

b45f28ad9a2a7a94d3f3521c5e5989369972a83a authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

We now use MinWatch for all PB constraints.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1012 ba638df5-4473-46d1-82f8-c...

4cea7d6ba64eb4a08b809bac037590c9b21d7c05 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Removed simplifications during conflict analysis, that are probably not correct (the solver becomes incorrect).

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1011 ba638df5-4473-46d1-82f8-c...

0a0ebf399e32a662ae82c356b0e9baf94712528a authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

allow to pick any element from the heap (for random walk).

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1010 ba638df5-4473-46d1-82f8-c...

2533b2c71728424d0d9d60636d8bff5458765009 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Improved version that will eventually make a random move. Based on a new version of the heap algorithm.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1009 ba638df5-4473-46d1-82f8-c...

c5fda96b598c504de1d86d9fa1b51505f3dca2a6 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

should have fixed incorrectness bug in the solver.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1008 ba638df5-4473-46d1-82f8-c...

0fd07e8ca66ae716d286d36d4c2594820e399f0f authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Made MinWatch the default.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1007 ba638df5-4473-46d1-82f8-c...

5967b3037bb796d3017b063511251ba3d17add0d authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Improve expensiveSimplification with card and pb case.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1006 ba638df5-4473-46d1-82f8-c...

fcb77fbedb4109e0ad29e20716e70faa684f9f08 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Implement new canBePropagatedMultipleTimes.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1005 ba638df5-4473-46d1-82f8-c...

625f2841222357e24cf4b6eb3352bef0e91ae1c5 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Implement new canBePropagatedMultipleTimes.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1004 ba638df5-4473-46d1-82f8-c...

4d2fadc0a801bfbda29537a036e233653c91314e authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Implement new canBePropagatedMultipleTimes.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1003 ba638df5-4473-46d1-82f8-c...

2b3f3c9fad74b081d00afd2939061032c0eb8eba authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1002 ba638df5-4473-46d1-82f8-c3ae2a17a6e1

fb0b38ed1cd88b3158d947ffba4c5ced05252fec authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Should have improved the efficiency of PB solvers. Need testing to check the pure SAT solvers did not slow down too much.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1001 ba638df5-4473-46d1-82f8-c...

ca9f42a386a001bc17eae5ab5f63a296dc0f3cf0 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

The file is reset after finding each solution.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1000 ba638df5-4473-46d1-82f8-c...

1d5a87db58a3cebdcfe4635d4eaa999593277ac4 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Fixed newline issues in OPBStringSolver.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@999 ba638df5-4473-46d1-82f8-c3...

dc6d25670ef2a47ae42cb79ed838450badddbb3c authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

New testcase to show the small problems with OPBStringSolver.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@998 ba638df5-4473-46d1-82f8-c3...

6a8be7ff39683d7eee438f14232679e1c45b80ce authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Fixed javadoc to precise the meaning of moreThan boolean value.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@997 ba638df5-4473-46d1-82f8-c3...

b84dc11bac81b9f85bacdf02c14eb96e862809a9 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Small code changes that might improve speed.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@996 ba638df5-4473-46d1-82f8-c3...

bd6040d3ad40bf8a9a4ac24b0f7c20db19d38518 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Removed unnecessary solver factory.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@995 ba638df5-4473-46d1-82f8-c3...

695a24d6785d078cb681064e46933c6d3dd99d14 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Removed unnecessary solver factory.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@994 ba638df5-4473-46d1-82f8-c3...

2d3fa586c61909675f28b5afd3236904240e9b92 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Improved parsing error message.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@993 ba638df5-4473-46d1-82f8-c3...

6a24234f09f88d6fb8fc31d5caec8dc79329c3d0 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Fixed missing UnitClause management in the creation of a clause.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@992 ba638df5-4473-46d1-82f8-c3...

6817f07d2200afa64c492c6e8416b11cfba237b2 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Improved parsing error message.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@991 ba638df5-4473-46d1-82f8-c3...

a4f77a4cf22e065f9dbc4b2051a56b7b03f8a999 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Removed IllegalStateException when the helper produces null constrs (if a variable satisfies the constraint, it can happen).

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@990 ba638df5-4473-46d1-82f8-c3...

332fca4204dcdb3dc5f1d79850f6b55ec3ee4d00 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Fix for bug SAT35.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@989 ba638df5-4473-46d1-82f8-c3...

1a476ccb746a852378737c77afa2df6b111830d1 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Test case for bug SAT35.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@988 ba638df5-4473-46d1-82f8-c3...

bfe2461a3f1b9730d4057df3453d04f32bc5d8c5 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Fixed more issues due to unit clause management.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@987 ba638df5-4473-46d1-82f8-c3...

5cf28eb1be42cba7c8f09ccff6f7a2dd28bd99e9 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

ManyCore now has support for findModel() methods.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@986 ba638df5-4473-46d1-82f8-c3...

dca700fb4e5400e0484163407ffc73b2d89e175a authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Test case showing the problems described in bug SAT34 on OPB solvers.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@985 ba638df5-4473-46d1-82f8-c3...

a023916e39cb6984648c757b42f820df0d66fd2c authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Changed all DSF to make sure that the solvers are always returning non null unit clause objects.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@984 ba638df5-4473-46d1-82f8-c3...

866ad172a4cb3191948953831b21dbb3717e2d6b authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Made sure that the pure clausal DSF was also returning unit clauses.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@983 ba638df5-4473-46d1-82f8-c3...

7ac014788df551b8979b1a1ebfcf055ebf290392 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Fixed the tests now that unit clauses are supported everywhere in sat4j.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@982 ba638df5-4473-46d1-82f8-c3...

ddf386289178c095e945aaf7861fc59387332623 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Fixed the tricks related to unit clauses.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@981 ba638df5-4473-46d1-82f8-c3...

2154149d92cb454b0e91ccb2ac7d97d5969ae031 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Should better handle the cases of unit clauses.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@980 ba638df5-4473-46d1-82f8-c3...

cb9ab0707def49edc54201226d8913c51e388407 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

No longer returns null in case of unit clauses.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@979 ba638df5-4473-46d1-82f8-c3...

a44cfc7cfad4ed83a1944efa440ca403bf958d43 authored over 13 years ago by leberre <leberre@ba638df5-4473-46d1-82f8-c3ae2a17a6e1>

Ecosyste.ms: OpenCollective

github.com/QuiltMC/quilt-loader-sat4j