sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2018-05-11T12:15:13Zhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/4Provide a representation of pseudo boolean constraints with primitive type lo...2018-05-11T12:15:13ZDaniel Le BerreProvide a representation of pseudo boolean constraints with primitive type long instead of BigIntegerPseudo boolean constraints are currently using BigInteger for representing coefficients and degrees.
If this is the only option for cutting planes based inference, it would be cheaper to use when possible primitive types for those const...Pseudo boolean constraints are currently using BigInteger for representing coefficients and degrees.
If this is the only option for cutting planes based inference, it would be cheaper to use when possible primitive types for those constraints, to efficiently propagate truth values.
One could choose either int or long for that.
long is probably a good tradeoff between the space required to store the information and the number of cases in which it will apply. Since we are going to 64 bits arch, long should be handled natively by the JVMs at some point.2.3.0https://gitlab.ow2.org/sat4j/sat4j/-/issues/11Allow creation of ManyCore solver from a list/array of existing solvers inste...2018-05-11T12:15:13ZDaniel Le BerreAllow creation of ManyCore solver from a list/array of existing solvers instead of their name in a factoryIt is currently impossible to create a new multi solver using existing solvers. One need to use a solver factory and a list of name instead.
It would be simpler to also allow the multi solver to reuse existing solvers.It is currently impossible to create a new multi solver using existing solvers. One need to use a solver factory and a list of name instead.
It would be simpler to also allow the multi solver to reuse existing solvers.2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/12Use List instead of IVec in DependencyHelper.getSolution()2018-05-11T12:15:13ZDaniel Le BerreUse List instead of IVec in DependencyHelper.getSolution()Currently, the DependencyHelper class returns an IVec object, i.e. a Sat4j specific data structure.
Since the DependencyHelper is supposed to be embedded in Java software, it is probably wise to use only Java classical data structure to...Currently, the DependencyHelper class returns an IVec object, i.e. a Sat4j specific data structure.
Since the DependencyHelper is supposed to be embedded in Java software, it is probably wise to use only Java classical data structure to interact with that class.
We could use for instance a java.util.List object instead of an IVec.
The main issue here is that it would break the API: the DependencyHelper class exists since Sat4j 2.1.
2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/15Allow to reset the DependencyHelper2018-05-11T12:15:13ZDaniel Le BerreAllow to reset the DependencyHelperThere is currently no way to reset a DependencyHelper. In some cases, it might be useful to reset it, i.e. to clear its mapping, objective function and solver.There is currently no way to reset a DependencyHelper. In some cases, it might be useful to reset it, i.e. to clear its mapping, objective function and solver.2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/33Improve project documentation (including web site)2018-07-07T05:11:52ZDaniel Le BerreImprove project documentation (including web site)Sat4j is mainly a research project, used to try our ideas around SAT. We start to receive more and more calls for help in the forums, which is nice because it shows that Sat4j is used, but it is also a sign that the documentation is not ...Sat4j is mainly a research project, used to try our ideas around SAT. We start to receive more and more calls for help in the forums, which is nice because it shows that Sat4j is used, but it is also a sign that the documentation is not good enough.
The tools we are using have evolved recently. Jira for instance should appear prominently on the web site while it does not, so we need to redirect users there.
We are going to design a new web site for next year (2012). Please use this bug report to tell us what you would like to see there.2.3.3https://gitlab.ow2.org/sat4j/sat4j/-/issues/34Make sure that all solvers return a unit clause in addClause2018-07-07T05:11:52ZDaniel Le BerreMake sure that all solvers return a unit clause in addClauseIn many cases, to allow the end user to easily remove unit clauses or constraints that propagate literals, we retour UnitClause or UnitClauses objects in the addXxxx() methods.
However, especially in the simple SAT case, that behavior i...In many cases, to allow the end user to easily remove unit clauses or constraints that propagate literals, we retour UnitClause or UnitClauses objects in the addXxxx() methods.
However, especially in the simple SAT case, that behavior is not enforced for all DataStructureFactory.
We thus need to make sure that all DSF do return a UnitClause object instead of null when a unit clause is detected.
2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/36Allow pretty printing of solutions2018-07-07T05:11:53ZDaniel Le BerreAllow pretty printing of solutionsWe currently generate very long lines with the solution of the problem (SAT, PB or MAXSAT).
We have OutOfMemory problems when displaying a solution after a OOM exception has ben launched.
It would probably not happen is the output stre...We currently generate very long lines with the solution of the problem (SAT, PB or MAXSAT).
We have OutOfMemory problems when displaying a solution after a OOM exception has ben launched.
It would probably not happen is the output stream is flushed regularly, i.e. after a limited amount of literals in the solution line.
It would therefore be nice to have a way to pretty print the solution line.
The only issue is that it may break scripts that simply do a grep to retrieve the solution.https://gitlab.ow2.org/sat4j/sat4j/-/issues/38Investigate usage of plain CNF rather than custom cardinality of PB constraints2018-07-07T05:11:53ZDaniel Le BerreInvestigate usage of plain CNF rather than custom cardinality of PB constraintsSat4j uses by default a custom constraint for cardinality and PB constraints.
The main advantage is to reduce the memory needed to represent the constraints. However, it requires ad hoc propagation and analysis procedure.
Many solvers fo...Sat4j uses by default a custom constraint for cardinality and PB constraints.
The main advantage is to reduce the memory needed to represent the constraints. However, it requires ad hoc propagation and analysis procedure.
Many solvers for solving MaxSat problems rely on cardinality of PB translation into SAT.
It would be nice to be able to easily try in sat4j the effect of pure clausal encodings against current solution.2.3.2https://gitlab.ow2.org/sat4j/sat4j/-/issues/39Add the possibility to create a constraint k among n in IProblem2018-07-07T05:11:53ZDaniel Le BerreAdd the possibility to create a constraint k among n in IProblemIn the pseudo boolean competition, and in many situations, it is important to be able to create a constraint that satisfies exactly k variables among n.
The current way to proceed in Sat4j is to create both a <= and a >= constraints.
T...In the pseudo boolean competition, and in many situations, it is important to be able to create a constraint that satisfies exactly k variables among n.
The current way to proceed in Sat4j is to create both a <= and a >= constraints.
That's fine. However, there are possibilities to encode directly such kind of constraints in the solver.
As such, it would be great to provide a new method for that in the API, even if the current implementation remains unchanged.2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/41Use a specific data structure to locate efficiently the weight associated to ...2018-07-07T05:11:53ZDaniel Le BerreUse a specific data structure to locate efficiently the weight associated to a literal in a counter based constraintAfter checking the reason for inefficiency of Sat4j on specific benchmarks, it turns out that large counter based constraints have a bottleneck:
// finding the index for p in the array of literals
int indiceP = 0;
while ((lits[ind...After checking the reason for inefficiency of Sat4j on specific benchmarks, it turns out that large counter based constraints have a bottleneck:
// finding the index for p in the array of literals
int indiceP = 0;
while ((lits[indiceP] ^ 1) != p)
indiceP++;
Using an auxiliary array or map to store the location of the literals instead of going through that loop will probably make the propagation and undo much faster.
(hint: use an array when the size of the constraint contains at least half of the variables, else use a map).2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/42Allow Sat4j to use bunzip2 to uncompress on the fly bz2 (and possibly others)...2018-07-07T05:11:53ZDaniel Le BerreAllow Sat4j to use bunzip2 to uncompress on the fly bz2 (and possibly others) compressed filesBenchmarks take more and more space, so they are usually stored in a compressed form.
Java has a built in support for zip file, but not for bz2 files.
One pragmatic way to add support for bz2 (and maybe 7z compressed files), is to use p...Benchmarks take more and more space, so they are usually stored in a compressed form.
Java has a built in support for zip file, but not for bz2 files.
One pragmatic way to add support for bz2 (and maybe 7z compressed files), is to use platform specific decoders, e.g. bunzip2 on unix platform.
This is how abscon is managing bz2 files, and it works fine for both Linux and Mac Os X.2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/43Allow the solver to be aware of the user defined max var id2018-07-07T05:11:53ZDaniel Le BerreAllow the solver to be aware of the user defined max var idWhen using SAT encodings, it is often necessary to create new variables on the fly.
This is true for instance in the translation from MaxSAT to PBO, from Card to SAT, etc.
In that context, it is important to make a difference between th...When using SAT encodings, it is often necessary to create new variables on the fly.
This is true for instance in the translation from MaxSAT to PBO, from Card to SAT, etc.
In that context, it is important to make a difference between the original max var id
and the maxvarid after adding the new variables.
It is assumed in most cases in Sat4j that the user defined maxvarid is defined using the method
ISolver.newVar(int maxvarid)
Then new variables can be retrieved using nextFreeVarId().
We could for instance fix the value set using newVar() and add a method to retrieve it.
That way, the model iterator for instance could use that value instead of the current nVar().2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/45Separate MS and PWMS decorator from the optimization method2018-07-07T05:11:53ZDaniel Le BerreSeparate MS and PWMS decorator from the optimization methodSince we now have two methods for optimizing, lower bounding and upper bounding, we need to have the decorators used in MaxSat independent of the optimization method.
This basically means that the decorator should not optimize the probl...Since we now have two methods for optimizing, lower bounding and upper bounding, we need to have the decorators used in MaxSat independent of the optimization method.
This basically means that the decorator should not optimize the problem, it should delegate that to a PseudoOptDecorator or a ConstraintRelaxingPseudoOptDecorator.
Since we use here new variables, it means updating the current pseudo-opt decorators to deal with additional variables.2.3.1https://gitlab.ow2.org/sat4j/sat4j/-/issues/59Use package-info.java instead of package.html for package JavaDoc2019-01-03T09:55:37ZDaniel Le BerreUse package-info.java instead of package.html for package JavaDocThere are some package documentation missing.
The preferred way to document packages since Java 5 is to use a package-info.java file instead of a package.html file in the package.
When working on improving the Javadoc, we should move t...There are some package documentation missing.
The preferred way to document packages since Java 5 is to use a package-info.java file instead of a package.html file in the package.
When working on improving the Javadoc, we should move the current package documentation inside package-info.java files.
See http://docs.oracle.com/javase/6/docs/technotes/tools/solaris/javadoc.html#packagecomment for details.
2.3.2https://gitlab.ow2.org/sat4j/sat4j/-/issues/67Concurrent calls to isSatisfiable2019-01-03T09:55:38ZAlexey VoronovConcurrent calls to isSatisfiableIt would be great to have Sat4j thread-safe.
The use-case I have is that I share one solver, and ask many questions with different assumptions. Even though my code is sequential, the test framework starts all tests in parallel under th...It would be great to have Sat4j thread-safe.
The use-case I have is that I share one solver, and ask many questions with different assumptions. Even though my code is sequential, the test framework starts all tests in parallel under the hood, which resulted in very misleading exceptions until I realised that there was a concurrency problem.
An easy solution would be to simply add Synchronized to isSatisfiable() functions. The drawback of this will be that the call to model() after isSatisfiable() might give the model for the assumptions of another thread.
Another solution is to add ConcurrentModificationException if isSatisfiable is called while another call to isSatisfiable is in progress. This will not solve problems with model() after isSatisfiable(), but at least might hint early on that there is a concurrency problem.
A great solution would be to allow multiple calls to isSatisfiable (with different sets of assumptions) to be executed in parallel. I’m not sure that this is achievable by any simple code modification, but my thoughts are as following. Whatever is kept in the solver between consecutive calls can be readily shared between two parallel calls. And whatever is removed between consecutive calls should be private to each call of isSatisfiable. API would change, since models would be different for each call to isSatisfiable, but isSatisfiable itself could return the model if there exist one (using some java variant of Haskell’s Maybe or Scala’s Option class).
Parallel calls would create all sorts of problems, for example, what happens if a clause is added to the solver while a call to isSatisfiable() is in progress in another thread. But maybe such issues can be separated somehow.
I don’t yet know what would be the simplest---yet user-friendly--- solution. All ideas welcome :)2.3.2https://gitlab.ow2.org/sat4j/sat4j/-/issues/120Remove call to System.gc in solver2018-04-13T11:56:12ZGhost UserRemove call to System.gc in solverI did some performance tests with the partial weighted maxsat solver called in many (up to 150) threads. After a while, tens of threads stuck in the call to "System.gc" in the class "org.sat4j.minisat.core.Solver", method "reduceDB()". T...I did some performance tests with the partial weighted maxsat solver called in many (up to 150) threads. After a while, tens of threads stuck in the call to "System.gc" in the class "org.sat4j.minisat.core.Solver", method "reduceDB()". This was a major performance bottleneck.
I downloaded the source, removed the call to "System.gc", compiled the sat4j-core and started the performance test again. The bottleneck was gone.
I think this call to System.gc should be removed. If there is really a need for this call, it could be made configurable (via an API call), so that it can be switched off if sat4j is used in multithreaded applications.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/121Initialization of org.sat4j.minisat.core.Solver calls Runtime.getRuntime().fr...2018-04-13T11:56:14ZGhost UserInitialization of org.sat4j.minisat.core.Solver calls Runtime.getRuntime().freeMemory()The class Solver in the sat4j core package initializes a variable called "memoryTimer" with an anonymous inner class of type ConflictTimerAdapter.
This inner class statically initializes a variable called "memorybound":
final long memor...The class Solver in the sat4j core package initializes a variable called "memoryTimer" with an anonymous inner class of type ConflictTimerAdapter.
This inner class statically initializes a variable called "memorybound":
final long memorybound = Runtime.getRuntime().freeMemory() / 10;
This is an expensive operation which seems to slow down the entire system for counting the available memory. In a multi-threaded scenary with many small partial weighted maxsat instances, it can lead to the machine being occupied with calculating the free memory again and again.
And: The initial class is not necessarily needed at all, e.g. when running a WeightedMaxSatDecorator with the default solver:
maxSatSolver = new WeightedMaxSatDecorator(SolverFactory.newDefault());
I propose to implement another kind of initialization that is only computing the amount of available memory when it is really needed. There are some usages of the variable "solver.memory_based" insat4j-core and sat4j-pb, and I think this could be replaced by a getter method that does the initialization when it is needed.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/90Better management of forgotten variables for undo-based constraints2018-04-13T11:56:17ZDaniel Le BerreBetter management of forgotten variables for undo-based constraintsSat4j allows to forget some variables during prime implicant computation.
It performs that operation by falsifying both the positive and negative literal associated with a variable.
It works fine for clauses and cardinality constraints.
...Sat4j allows to forget some variables during prime implicant computation.
It performs that operation by falsifying both the positive and negative literal associated with a variable.
It works fine for clauses and cardinality constraints.
However, there is an issue for constraints requiring a call to undo when backtracking.
The constraints to be considered when undoing an assignment is stored for a variable, not a literal. As such, when forgetting a variable, both the constraints where the positive and negative literal appears are part of that constraint. So a call to undo() on a constraint that does contains the literal will occur.
Worst, it is necessary to perform the undo both on the literal and its oppositve in that case, to properly undo all constraints.
In our testcases, the PB constraints are encoding the objective function and are deleted after each PI computation, so the current fix is simply to avoid a NPE that occurs when the undo() method is applied on a constraint not associated by such literal.
We are currently working on a new PI computation scheme, so that code with forget will eventually be removed. The current fix allows the solver to be correct, and prevents NPE to occur.https://gitlab.ow2.org/sat4j/sat4j/-/issues/104Improve error report when xsd missing2018-04-13T11:56:15ZBenoît HoessenImprove error report when xsd missingWhen using the csp solver within sat4J, a null pointer exception is launched if instance_2_0.xsd is missing from org.sat4j.csp.xml.CspXmlParser:50
A possible fix would be to make sure that url is not null:
if(url == null){
throw new ...When using the csp solver within sat4J, a null pointer exception is launched if instance_2_0.xsd is missing from org.sat4j.csp.xml.CspXmlParser:50
A possible fix would be to make sure that url is not null:
if(url == null){
throw new IOException("Unable to locate instance_2_0.xsd");
}2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/86Add Glucose 21 dynamic restart strategy and enable it by default2018-04-13T11:56:13ZDaniel Le BerreAdd Glucose 21 dynamic restart strategy and enable it by defaultThe new Dynamic restart strategy of Glucose 2.1 has been presented in "Refining restarts strategies for SAT and UNSAT formulae. Gilles Audemard and Laurent Simon, in proceedings of CP'2012".
That dynamic restart strategy is going to be ...The new Dynamic restart strategy of Glucose 2.1 has been presented in "Refining restarts strategies for SAT and UNSAT formulae. Gilles Audemard and Laurent Simon, in proceedings of CP'2012".
That dynamic restart strategy is going to be Sat4j default instead of Armin Biere's In/Out rapid Restart strategy.2.3.3https://gitlab.ow2.org/sat4j/sat4j/-/issues/85Allow easy access to a pseudo boolean optimizer2018-04-13T11:56:14ZDaniel Le BerreAllow easy access to a pseudo boolean optimizerWhen a newcomer to Sat4j wants to solve a pseudo boolean optimization problems, it usually takes the PB solver available in SolverFactory.newDefault(), which looks ok from a user point of view.
However, by default, a PB solver does not ...When a newcomer to Sat4j wants to solve a pseudo boolean optimization problems, it usually takes the PB solver available in SolverFactory.newDefault(), which looks ok from a user point of view.
However, by default, a PB solver does not perform any optimization. The optimization is performed by a generic procedure on IOptimizationProblem.
The PseudoOptDecorator provides the IOptimizationProblem capability to IPBSolver.
The optimization can then be performed using an OptToPBSATAdapter object.
That process allows the power user to build custom PB optimizers but makes difficult the usage of the library for most users that really just pick the default settings.
The idea is to add a new method in the SolverFactory, newDefaultOptimizer, to provide a ready to use optimizer.
2.3.3https://gitlab.ow2.org/sat4j/sat4j/-/issues/119Iterators can be created at each conflict2018-04-13T11:56:15ZBenoît HoessenIterators can be created at each conflictWhenever the ConflictTimerContainer is used, an iterator on Vec is created.
```
public void newConflict() {
Iterator<ConflictTimer> it = this.timers.iterator();
while (it.hasNext()) {
it.next().newConfli...Whenever the ConflictTimerContainer is used, an iterator on Vec is created.
```
public void newConflict() {
Iterator<ConflictTimer> it = this.timers.iterator();
while (it.hasNext()) {
it.next().newConflict();
}
}
{code}
This could be easily changed to a version using no iterator to avoid object creation/destruction
{code:title=ConflictTimerContainer.java|borderStyle=solid}
public void newConflict() {
for(int i =0; i<this.timers.size(); i++){
this.timers.get(i).newConflict();
}
}
```
This, applied to a small instance like velev-engi-uns-1.0-4nd.cnf can reduce the number of created object by 92594 (= 311936 B)2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/98Allow hybrid lexico optimization2018-04-13T11:56:12ZDaniel Le BerreAllow hybrid lexico optimizationIn some cases, it would be nice to be able to perform a lexico optimization without waiting to prove the optimality of each criteria.
It means that the first criteria is optimized during a given timeout, then the first and second are op...In some cases, it would be nice to be able to perform a lexico optimization without waiting to prove the optimality of each criteria.
It means that the first criteria is optimized during a given timeout, then the first and second are optimized during a given timeout, and so on until all the criteria are considered.
We would use a classical transformation of lexico into a linear objective function for all but the first optimization.2.3.4https://gitlab.ow2.org/sat4j/sat4j/-/issues/88Avoid calling visualization code when no visualization is needed2018-04-13T11:56:17ZDaniel Le BerreAvoid calling visualization code when no visualization is neededWhen using the sat4j-sat.jar package without option (to discover them) on a machine without X server (a cluster), the app throws an exception because it tries to access X related features.
Exception in thread "main" java.lang.ExceptionI...When using the sat4j-sat.jar package without option (to discover them) on a machine without X server (a cluster), the app throws an exception because it tries to access X related features.
Exception in thread "main" java.lang.ExceptionInInitializerError
at java.lang.Class.forName0(Native Method)
at java.lang.Class.forName(Class.java:169)
at org.sat4j.sat.RTSI.findnames(Unknown Source)
at org.sat4j.sat.RTSI.find(Unknown Source)
at org.sat4j.sat.RTSI.find(Unknown Source)
at org.sat4j.sat.RTSI.find(Unknown Source)
at org.sat4j.sat.Solvers.showAvailableRestarts(Unknown Source)
at org.sat4j.sat.Solvers.usage(Unknown Source)
at org.sat4j.sat.Launcher.usage(Unknown Source)
at org.sat4j.sat.Launcher.run(Unknown Source)
at org.sat4j.sat.Launcher.main(Unknown Source)
Caused by: java.awt.HeadlessException:
No X11 DISPLAY variable was set, but this program performed an operation which requires it.
at sun.awt.HeadlessToolkit.getScreenSize(HeadlessToolkit.java:261)
at org.sat4j.sat.RemoteControlFrame.<clinit>(Unknown Source)
... 11 more
Such code should only be launched when the visualization option is set.2.3.3https://gitlab.ow2.org/sat4j/sat4j/-/issues/109Allow iterating on a part of a model (subset of its variables)2018-04-13T11:56:13ZDaniel Le BerreAllow iterating on a part of a model (subset of its variables)In some cases, it may be useful to iterate over a subset of the variables
(over decisions variables for instance).
The idea is to simply restrict the use of the model iterator (using blocking clauses) to a subset of the variables only.
...In some cases, it may be useful to iterate over a subset of the variables
(over decisions variables for instance).
The idea is to simply restrict the use of the model iterator (using blocking clauses) to a subset of the variables only.
We require for this a new class, for efficiency reason, instead of generalizing the code of the actual ModelIterator class.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/112Integrate faster prime implicant computation2018-04-13T11:56:11ZDaniel Le BerreIntegrate faster prime implicant computationWe propose in a paper to be presented in FMCAD 2013 a new algorithm for computing prime implicants in a CDCL solver. The code of that paper is available on a specific branch (BRESIL). We need to move that code to the main branch now, and...We propose in a paper to be presented in FMCAD 2013 a new algorithm for computing prime implicants in a CDCL solver. The code of that paper is available on a specific branch (BRESIL). We need to move that code to the main branch now, and to make a release of Sat4j including that new feature before presenting that work at FMCAD.2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/72Print the statistics of all solvers in manycore2018-04-13T11:56:15ZDaniel Le BerrePrint the statistics of all solvers in manycoreCurrently, only the statistics of the winner are displayed. We should display the statistics of all solvers.Currently, only the statistics of the winner are displayed. We should display the statistics of all solvers.https://gitlab.ow2.org/sat4j/sat4j/-/issues/94if-then constraint2018-04-13T11:56:15ZMihai Barbuceanuif-then constraintWhat would be the best way to have if-then constraints (without the else part, which the ite forces on the user) in the GateTranslator? The GateTranslator does not have a default constructor hence can't be simply extended.
Thanks
MihaiWhat would be the best way to have if-then constraints (without the else part, which the ite forces on the user) in the GateTranslator? The GateTranslator does not have a default constructor hence can't be simply extended.
Thanks
Mihai2.3.6https://gitlab.ow2.org/sat4j/sat4j/-/issues/96Allow Sat4j to provide unsat proofs in RUP format2018-04-13T11:56:17ZDaniel Le BerreAllow Sat4j to provide unsat proofs in RUP formatThere is a new track for certifying unsat proofs. It should not be difficult to allow sat4j to participate by implementing an unsat proof search listener.There is a new track for certifying unsat proofs. It should not be difficult to allow sat4j to participate by implementing an unsat proof search listener.2.3.4https://gitlab.ow2.org/sat4j/sat4j/-/issues/100Create a specific event when learning unit clauses2018-04-13T11:56:14ZDaniel Le BerreCreate a specific event when learning unit clausesWhen the solver learns unit clauses (a literal), it needs to got back to decision level zero, and such clause is managed specifically in the solver.
In the context of parallel SAT solving, a solver like plingeling is sharing unit clauses...When the solver learns unit clauses (a literal), it needs to got back to decision level zero, and such clause is managed specifically in the solver.
In the context of parallel SAT solving, a solver like plingeling is sharing unit clauses among parallel solvers. Having a specific unit clause event would allow to implement more easily such feature in Sat4j.2.3.4