logic-ng/logicng

The Next Generation Logic Library

logicng's Issues

Upgrade antlr dependencies version 4.13.1

Hi everyone,

i was wondering if there is a chance to upgrade the antlr dependencies to a more recent version (like 4.13.1).

Since i also use ANTLR within a project with LogicNG, I face errors due to incompatible code generations.

LogicNG used 4.9.3 within the latest published version of 2.4.1.

ANTLR Tool version 4.9.3 used for code generation does not match the current runtime version 4.13.1
ANTLR Runtime version 4.9.3 used for parser compilation does not match the current runtime version 4.13.1

Thanks in advance. Br, Franz

[Question] enumerateAllModels() method - Is there an Option for order of output?

In the enumerateAllModels() methods, is there an option for the preferred "solution output order"?
I.e. if I would like to get the results with the most "True" values for the variables first or the results with the most "False" values for the variables?
Something like an "ascending" or "descending" sort order?

Improve discoverability of features

Currently the only documentation apart from JavaDoc is the "Getting Started" section in the README. As JavaDoc is great when you know something exists but terrible if you don't it would be great to have a way to learn about features.
So for example I just learned about the Anonymizer and the BackboneSimplifier by looking through closed issues. This is not the best experience.
Even a list with features and classnames would be good.

Performance of QMC

Hi,
should calling QMC on this really crash it ? I understand there are many variables, but still.

(a0 | a1) & (a2 | a3) & (a4 | a5) | (a6 | a7) & (a8 | a9) | a10 | a11 | a12

Would there be a way to detect and throw/exit when the algorithm is going haywire ? e.g. a timeout or max rewritten size or such added to the QMC API. That would be nicer than wrapping invocations with a thread + external timeout, which is what I'm currently considering.

Lazy evaluation for PseudoBooleanParser in FormulaFactory

Because FormulaFactory isn't thread-safe can we have same form of lazy evaluation in FormulaFactory?

For example set the PseudoBooleanParser to null by default:

And if the parser is really used create it:

			if (parser == null) {
				parser = new PseudoBooleanParser(this);
			}
			// now use the parser

Maybe the same for CNFEncoder, PBEncoder ?

CNFFactorisation throws null pointer exception.

Try to run this code:

PropositionalParser parser = new PropositionalParser(f);
Formula f1 = parser.parse("((((var4711&var0815&Multiversum&var494|var4711&var0815&var007|var0815&var007&var494)&~(var4712&Multiversum)&~(var4712&var007&var494)&~Variablenname&~Zorro)&Hura)|(((var4711&var0815&Multiversum&var494|var4711&var0815&var007|var0815&var007&var494)&~(var4712&Multiversum)&~(var4712&var007)&~Variablenname&~Zorro)&Feuerwerk)|((Multiversum&Pistole&~Variablenname&~Zorro)&Hura)|((Multiversum&Pistole&~Variablenname&~Zorro)&Feuerwerk)|((Ix&Wonderwoman&~Variablenname&~Zorro)&Feuerwerk))");

Formula f2 = parser.parse("(Hura&Multiversum&Pistole|Feuerwerk&(Ix&Wonderwoman|Multiversum&Pistole)|var0815&(Hura&var4711&var007&~var494&Multiversum|(Hura|Feuerwerk)&(var494&(var4711&Multiversum|var007)|var4711&var007)&~var4712))&~Variablenname&~Zorro");

Formula equiv = f.equivalence(f1,f2);
System.out.println("Equivalent? "+equiv.holds(new TautologyPredicate(f)));

it produces a NullPointerException.

Exception in thread "main" java.lang.NullPointerException at org.logicng.formulas.FormulaFactory.condenseOperandsAnd(FormulaFactory.java:885) at org.logicng.formulas.FormulaFactory.constructAnd(FormulaFactory.java:423) at org.logicng.formulas.FormulaFactory.and(FormulaFactory.java:392) at org.logicng.transformations.cnf.CNFFactorization.apply(CNFFactorization.java:109) at org.logicng.transformations.cnf.CNFFactorization.apply(CNFFactorization.java:83) at org.logicng.formulas.Formula.transform(Formula.java:222) at org.logicng.transformations.cnf.CNFEncoder.singleAdvancedEncoding(CNFEncoder.java:130) at org.logicng.transformations.cnf.CNFEncoder.advancedEncoding(CNFEncoder.java:126) at org.logicng.transformations.cnf.CNFEncoder.encode(CNFEncoder.java:107) at org.logicng.formulas.Formula.cnf(Formula.java:213) at org.logicng.solvers.MiniSat.add(MiniSat.java:204) at org.logicng.predicates.satisfiability.SATPredicate.test(SATPredicate.java:82) at org.logicng.formulas.Formula.holds(Formula.java:242) at org.logicng.predicates.satisfiability.TautologyPredicate.test(TautologyPredicate.java:77) at org.logicng.formulas.Formula.holds(Formula.java:242)

We were able to fix this instance of the bug by changing line 100ff of class CNFFactorization from

case AND:
nops = new LinkedHashSet<>();
for (final Formula op : formula) {
if (!this.proceed) {
return null;
}
nops.add(this.apply(op, cache);
}
cached = formula.factory().and(nops);
break;

to

case AND:
nops = new LinkedHashSet<>();
for (final Formula op : formula) {
final Formula apply = this.apply(op, cache);
if (!this.proceed) {
return null;
}
nops.add(apply);
}
cached = formula.factory().and(nops);
break;

We believe this is not the whole fix needed for this type of bug. It solves this instance, but CNFFactorization looks like it has multiple places where the proceed check is done too early or should at least be done again.

Bump to ANTLR runtime version 4.10.1

Can you please bump to ANTLR runtime version 4.10.1?

The latest JGraphT SNAPSHOT uses 4.10.1 and conflicts in my project with LogicNG using 4.9.3

• jgrapht/jgrapht#1143

Example how to get all true/false combinations of variables which fulfill a boolean formula?

Is there an example available how to get all true/false combinations of variables which fulfill a boolean formula?

Caused by: java.lang.ClassCastException: java.util.HashMap$Node cannot be cast to java.util.HashMap$TreeNode

When building complex combinations of AND based Formula's using the BDDKernel the following ClassCastException occurs due to the mixture of Maps being used. What is the reasoning why the BDDKernal uses TreeMaps for it's var2idx and idx2var variables? Why not HashMap?

Caused by: java.lang.ClassCastException: java.util.HashMap$Node cannot be cast to java.util.HashMap$TreeNode

• Some portions of the stacktrace have been deleted to protect intellectual property.

java.lang.ClassCastException
	at sun.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
	at sun.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:62)
	at sun.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:45)
	at java.lang.reflect.Constructor.newInstance(Constructor.java:422)
	at java.util.concurrent.ForkJoinTask.getThrowableException(ForkJoinTask.java:598)
	at java.util.concurrent.ForkJoinTask.reportException(ForkJoinTask.java:677)
	at java.util.concurrent.ForkJoinTask.invoke(ForkJoinTask.java:735)
	at java.util.stream.Nodes.collect(Nodes.java:328)
	at java.util.stream.ReferencePipeline.evaluateToNode(ReferencePipeline.java:109)
	at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:540)
	at java.util.stream.AbstractPipeline.evaluateToArrayNode(AbstractPipeline.java:260)
	at java.util.stream.ReferencePipeline.toArray(ReferencePipeline.java:438)
	at one.util.streamex.AbstractStreamEx.toArray(AbstractStreamEx.java:344)
	at one.util.streamex.AbstractStreamEx.toList(AbstractStreamEx.java:1186)
	at one.util.streamex.AbstractStreamEx.toListAndThen(AbstractStreamEx.java:1234)
...
	at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
	at java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:175)
	at java.util.Spliterators$ArraySpliterator.forEachRemaining(Spliterators.java:948)
	at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:481)
	at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:471)
	at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:545)
	at java.util.stream.AbstractPipeline.evaluateToArrayNode(AbstractPipeline.java:260)
	at java.util.stream.ReferencePipeline.toArray(ReferencePipeline.java:438)
	at one.util.streamex.AbstractStreamEx.toArray(AbstractStreamEx.java:344)
	at one.util.streamex.AbstractStreamEx.toImmutableList(AbstractStreamEx.java:1204)
...
	at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
	at java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:175)
	at java.util.Collections$2.tryAdvance(Collections.java:4717)
	at java.util.Collections$2.forEachRemaining(Collections.java:4725)
	at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:481)
	at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:471)
	at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:545)
	at java.util.stream.AbstractPipeline.evaluateToArrayNode(AbstractPipeline.java:260)
	at java.util.stream.ReferencePipeline.toArray(ReferencePipeline.java:438)
	at one.util.streamex.AbstractStreamEx.toArray(AbstractStreamEx.java:344)
	at one.util.streamex.AbstractStreamEx.toImmutableList(AbstractStreamEx.java:1204)
...
	at org.eclipse.core.internal.jobs.Worker.run(Worker.java:56)
Caused by: java.lang.ClassCastException: java.util.HashMap$Node cannot be cast to java.util.HashMap$TreeNode
	at java.util.HashMap$TreeNode.moveRootToFront(HashMap.java:1819)
	at java.util.HashMap$TreeNode.putTreeVal(HashMap.java:1999)
	at java.util.HashMap.putVal(HashMap.java:637)
	at java.util.HashMap.put(HashMap.java:611)
	at org.logicng.formulas.FormulaFactory.constructAnd(FormulaFactory.java:580)
	at org.logicng.formulas.FormulaFactory.and(FormulaFactory.java:424)
	at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
	at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
	at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
	at one.util.streamex.UnknownSizeSpliterator$USOfRef.forEachRemaining(UnknownSizeSpliterator.java:145)
	at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:481)
	at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:471)
	at java.util.stream.Nodes$CollectorTask.doLeaf(Nodes.java:2183)
	at java.util.stream.Nodes$CollectorTask.doLeaf(Nodes.java:2149)
	at java.util.stream.AbstractTask.compute(AbstractTask.java:316)
	at java.util.concurrent.CountedCompleter.exec(CountedCompleter.java:731)
	at java.util.concurrent.ForkJoinTask.doExec(ForkJoinTask.java:289)
	at java.util.concurrent.ForkJoinPool$WorkQueue.runTask(ForkJoinPool.java:1056)
	at java.util.concurrent.ForkJoinPool.runWorker(ForkJoinPool.java:1692)
	at java.util.concurrent.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:157)

Out of memory issue

The program will throw an Out Of Memory error if the formula has many variables(e.g. more than 200 variables).
java.lang.OutOfMemoryError: Java heap space
at java.util.LinkedHashMap.createEntry(Unknown Source)
at java.util.HashMap.addEntry(Unknown Source)
at java.util.LinkedHashMap.addEntry(Unknown Source)
at java.util.HashMap.put(Unknown Source)
at java.util.HashSet.add(Unknown Source)
at org.logicng.formulas.FormulaFactory.addFormulaOr(FormulaFactory.java:900)
at org.logicng.formulas.FormulaFactory.condenseOperandsOr(FormulaFactory.java:812)
at org.logicng.formulas.FormulaFactory.constructOr(FormulaFactory.java:520)
at org.logicng.formulas.FormulaFactory.or(FormulaFactory.java:477)
at org.logicng.transformations.cnf.CNFFactorization.distribute(CNFFactorization.java:109)
at org.logicng.transformations.cnf.CNFFactorization.distribute(CNFFactorization.java:106)
at org.logicng.transformations.cnf.CNFFactorization.distribute(CNFFactorization.java:106)
at org.logicng.transformations.cnf.CNFFactorization.apply(CNFFactorization.java:66)
at org.logicng.transformations.cnf.CNFFactorization.apply(CNFFactorization.java:52)
at org.logicng.formulas.Formula.transform(Formula.java:191)
at org.logicng.formulas.Formula.cnf(Formula.java:182)
at org.logicng.solvers.MiniGSat.add(MiniGat.java:154)
at org.logicng.solvers.sat.Test.parseRules(Test.java:94)
at org.logicng.solvers.sat.Test.testAssume(Test.java:66)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
at java.lang.reflect.Method.invoke(Unknown Source)
at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:50)
at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12)
at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:47)
at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17)
at org.junit.runners.ParentRunner.runLeaf(ParentRunner.java:325)
at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:78)
at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:57)
at org.junit.runners.ParentRunner$3.run(ParentRunner.java:290)
at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:71)

Formula immutable?

Schönen guten Tag zusammen,

ich hatte es Steffen neulich mal per Skype angekündigt und jetzt hier das passende Issue. Im Commit 1e7e001 haben wir eine Klasse eingecheckt die aus unserer Sicht einen Bug produziert.

Wir haben versucht das ganze möglicht minimal zu machen, soll heißen, der Code tut eigentlich nichts sinnvolles mehr und wir haben möglichst viel weggelassen. Was jetzt übrig ist sollte schon fast minimal sein.

Was passiert im Grunde?:
Wir basteln Formeln hin und her zusammen und bauen neue, Formula ist ja meines Wissens nach zunächst mal immutable. Dann wollen wir aus einer Formel eine neue berechnen indem wir Teile aus der bisherigen Formel rausstreichen. Dabei gelingt es uns (sollte es das?) die ursprüngliche Formel zu verändern indem wir ihre f.literals() verändern. Das allein ist ja schon unschön.

Dann verlassen wir die ganze Methode und machen einen Äquivalenzcheck auf zwei anderen Formeln. LogicNG sagt dann am Ende das Z = Z & ~X eine Tautologie sei.

Guckt euch das Beispiel mal an, wir haben echt lange nach dem Problem gesucht und haben für unseren Fall jetzt auch einen Fix, aber so wahnsinnig intuitiv ist das alles für uns nicht was da abläuft.

Wenn man auf Java8 umstellt lässt sich der Bug auch mit Streams und Lambdas erzeugen, könnte man auch gleich mal angucken was da passiert.

Liebe Grüße,
Daniel und Ivo

[Feature request] implement QuineMcClusky algortihm

Could you please provide an implementation of the Wikipedia - Quine–McCluskey algorithm

For example the python-boolean project (QM.py) code can be ported to Java. There's also a related blog entry available.

See also: Wikipedia - Petrick's method

When converting string formula, getting formula containing ~@RESERVED_CNF_0

When trying to parse the following string, the resulting CNF comes back with lots of @RESERVED_CNF_0 in it ?

(A & ~B | ~A & B) & (C & B & ~A & ~D & ~E | C & ~B & A & ~D & ~E | C & ~B & ~A & D & ~E | C & ~B & ~A & ~D & E | ~C & B & A & ~D & ~E | ~C & B & ~A & D & ~E | ~C & B & ~A & ~D & E | ~C & ~B & A & D & ~E | ~C & ~B & A & ~D & E | ~C & ~B & ~A & D & E) & (A & ~F | ~A & F) & (E & ~C | ~E & C)

Minimization algorithm available?

Is there a minimization algorithm like Quine McCluskey available?

Changing variable value after parsing formula

Hello, I was wondering if there's a way to change a variable's value after parsing a formula, for example:
After parsing ("A & ~(B | ~C)"), is there a way to give "A" the value "true", and then solve it?

In other words, to only get the assignments where A is true, without using enumerateAllModels().

enumerateAllModels with additionalVariables

Judging from the documentation, i expected this test case to suceed. It doesn't,

@Test
public void testModelEnumerationWithDontCares() {
    FormulaFactory factory = new FormulaFactory();
    SATSolver solver = MiniSat.miniSat(factory);
    Variable a = factory.variable("A");
    Variable b = factory.variable("B");
    solver.add(a);
    List<Variable> allVars = new LinkedList<>();
    allVars.add(a);
    allVars.add(b);
    List<Assignment> models = solver.enumerateAllModels(null,allVars);
    //The models should be A,B as well as A, -B
    assertEquals(2, models.size());
  }

Memory requirements

I am trying to convert my logic representation of SHA1 hash algorithm into LogicNG and run CNF. But I am getting Java heap space error, even when allocating 24GB to heap space.

Is there a way to debug memory usage? I basically have a boolean graph with (and, xor and not) with 100 thousand nodes, building LogicNG formula works without any problems, but CNF algorithm fails on memory usage.

My goal is to feed the results to SAT solver.

BDD Kernel & Factory usage

Hi,

Just wanted to start off by saying this is a great library to work with Boolean Formula's and solvers, keep up the good work. I've been developing an algorithm using the BDD implementation provided in the LogicNG library and encountered a couple of limiting factors for both appending to the BDD & finally converting the result of the "allSat" (byte[]) method back it's input Variables.

First of all, the major issue I encountered during my use of the BDD implementation was that in order to use all the BDD functionality I am forced to use a BDDKernel class for the rest of the BDD implementation to function and therefore when some methods that I require for my algorithm to work are restricted due to being private I was forced to duplicate the entire BDDKernel source and have it extend the BDDKernel too. This resulted in duplication of all the variables found in the BDDKernel class which are all mostly private. This is not ideal and the major reason why I'm trying to reach out and request a simple fix that would help me use the BDDKernel without having to duplicate the code into my own source (including the BDDCache, BDDFactory, BDDPrime).

If the method "makeNode" was changed from a private to protected modifier, this would correct my problem and opens up the possibility for basic extensions of the Kernel allowing developers to add to the node list and construct there own methods and custom functionality.

Secondly, I identified that the BDDFactory already contains a mapping by Variable Ordering to index which matches exactly to the byte[] output you receive from calling the allSat (1) method from the BDD, obviously because we are actually talking about the "level" the variable is on. If a simple method was providing in the factory to retrieve the Variable based on the index it would make everything much easier for developers to construct a result from the byte array.

/**
 * Returns a Variable object matching to the index according to the Variable Ordering.
 *
 * @param index - The expected index of the Variable
 * @return Variable - the Variable to which the specified index is mapped, otherwise null if the index contains no mapping
 */
public Variable getVariableByIndex(int index) {
    return this.idx2var.get(index);
}

Here is an example of how I converted a byte array into it a list of Variables:

return cutSet -> IntStreamEx.range(cutSet.length)
                    .filter(index -> cutSet[index] == 1)
                    .mapToObj(factory::getVariableByIndex)
                    .toImmutableList();

Thanks

Parallel computing

Hello,
I have an array of DNF strings I have to parse and minimize. I'd like to do that in parallel, since I need the EXACT minimization and also conversion to CNF, without addition of new variables, that is a pretty intense task. For that, I'd use a Java Parallel Stream, but unfortunately there are issues when trying to use a parser in parallel. Is there a way, without making the code too complicated (read: using parallel streams, not thread objects) to make it work in parallel?

cnf() reorders the variables

In this JUnit test case the cnf() method reorders the variables and the JUnit test fails:

	public void testLogicNGCNF() {
		final FormulaFactory f = new FormulaFactory();
		final Variable x = f.variable("x");
		final Variable y = f.variable("y");
		final Literal notX = f.literal("x", false);
		final Literal notY = f.literal("y", false);
		// x & ~y | ~x & y
		final Formula formula = f.or(f.and(x, notY), f.and(notX, y)).cnf();
		assertEquals("(x | y) & (~x | ~y)", formula.toString());
	}

See: Symja JUnit tests

Add JavaDoc to "phase"

I am reading https://github.com/logic-ng/LogicNG#first-steps:

final Literal notC = f.literal("C", false);

The documentation states that phase is a Boolean parameter. There is no documentation on the phase in README.md and not at the JavaDoc of literal.

I wonder why

a) phase is not en enum? An enum makes the possibilities clear. Currently with false I don't know whether there is no phase processing, if its a phase, where all variables are false, an initialization phase, ... - Reading the code I would have set it to true, but I am not sure.

b) There is no literal creator without any phase parameter (and then setting a default phase)

Would is be, additionally, possible to describe the phase in the README.md file?

(Issue created in my the context of my free-time project JabRef)

[bug] Error when exporting single-clause cnf formula to dimacs file

FormulaDimacsFileWriter.write() produces a wrong .cnf file when exporting a formula that consists of a single clause with multiple literals. The formula is wrongfully split into multiple clauses that each contain one literal, effectively turning the disjunction into a conjunction.

Faulty testcase:
The expected .cnf file (src/test/resources/writers/formulas-dimacs/f4_f.cnf) for the testcase formula f4 (~(a & b) | b & ~c or as cnf: ~a | ~b | ~c) in FormulaDimacsFileWriterTest.testFormulas() is wrong, which hides this bug when executing the test suite.

Steps to reproduce:

• execute test method FormulaDimacsFileWriterTest.testFormulas()
• the testcase formula f4 has cnf ~a | ~b | ~c
• resulting dimacs .cnf file (src/test/resources/writers/temp/f4_f.cnf) is:

p cnf 3 3
-3  0
-1  0
-2  0

when it should be

p cnf 3 1
-1 -2 -3  0

What are valid variable names (for parsing)?

I encountered a ParserException due to an invalid character (.) when parsing a formula, which triggered this question. I could not find an answer in the documentation. Through tests I found out that underscores are supported.
Are other special characters supported?

How to create BDD ?

Is this the correct way to create the BDD for index 11 and 2 variables?

            int k = 11;
            int n = 2;
            FormulaFactory factory = new FormulaFactory();
            final BDDKernel bddKernel = new BDDKernel(factory, n, n * 30, n * 20);
            SortedMap<Integer, Variable> idx2var = bddKernel.idx2var();
            SortedMap<Variable, Integer> var2idx = bddKernel.var2idx();
            for (int i = 0; i < n; i++) {
              final Variable variable = factory.variable("x" + i);
              idx2var.put(i, variable);
              var2idx.put(variable, i);
            }
            BDD bdd = new BDD(k, bddKernel);

How can I evaluate the BDD for x0=false and x1=true?

miniSat.enumerateAllModels() returns assignments with additional variables

assignments returned from miniSat.enumerateAllModels() contain variables with name pattern @RESERVED_CC_*

What is the best way to represent a `BooleanFunction` in LogicNG?

What is the best way to represent a BooleanFunction in LogicNG:

• https://reference.wolfram.com/language/ref/BooleanFunction.html

Example:

This creates a boolean function:

f = BooleanFunction[30, 3] 

FullForm[f]

returns

BooleanFunction["BDD" -> {-3, 0, 2, -2, 1, 1, 3, 2, 1, -1}]

Pseudo-Boolean Constraint toString into Parser Roundtrip does not work.

If i parse a pseudo boolean constraint like

1 * A + 1 * B = 1

it works. If I then print this with toString() it becomes

A + B = 1

which can not be parsed anymore.

I believe that output should be parseable again. And it is in all other cases.

Is there xor?

Hello, is there a xor operation? I am unable to find it.

Is it possible to have saveState() and loadState() in MaxSATSolver?

There is saveState() and loadState() functions in MiniSat, it is very useful for not restart the solver from draft.

Is it safe to use a formula multiple times?

To use a formula as a subformula in multiple formulae?

Formula a = ...
Formula b = ... a ...
Formula c = ... a ...

Quine-McCluskey Solver Inefficient for Formulas with Many Input Variables

Hello, I have been running into some issues with the Quine-McCluskey solver when there are many input variables. Unfortunately, the solver seems to be very inefficient in these cases. Do you have any suggestions to speed up the computation when analyzing formulas such as f1 or f2 below?

f1 = "(0 & ~1 & ~3 & 2) | (0 & 1 & 2 & 4) | (0 & ~1 & 5 & 6 & 7 & ~1 & ~8 & ~9 & ~10 & ~11 & ~12 & 13 & ~3 & ~2) | (0 & 1 & 2)"
f2 = "(0 & 1 & 2) | (0 & ~1 & 5 & 6 & 7 & ~1 & ~8 & ~9 & ~10 & ~11 & ~12 & ~3 & ~2) | (0 & 1 & 2 & 4) | (0 & ~1 & 5 & 6 & 7 & ~1 & ~8 & ~9 & ~3 & ~2) | (0 & ~1 & ~3 & 2) | (0 & ~1 & 5 & 6 & 7 & ~1 & ~8 & ~9 & ~10 & ~11 & ~12 & 13 & ~3 & ~2) | (0 & ~1 & ~3 & ~2) | (0 & 1 & ~2)"

final FormulaFactory f = new FormulaFactory();
final PropositionalParser p = new PropositionalParser(f);
final Formula formula = p.parse(f1);
final Formula dnf = QuineMcCluskeyAlgorithm.compute(formula);

[Question] How to reduce syntactic size of a formula

Hi,

Thanks for making your package available, it's a nice piece of software.
I'm trying to minimize some boolean formulas, with the metric that resulting syntactic tree should have as few nodes as possible.
Part of the goal on my test set is the fact some atoms in formulas disappear, as they are asserted in both forms (a OR !a => true, a AND !a =>false). This is not immediately obvious, the formulas are pretty large, so I'm trying to use your package for this.

I've tried running MCQ, but the conversion to what looks like CNF makes some of my formulas blow up in size; this is not ideal.
I'm thinking of trying MCQ (which should always be better than CNF, right ?) then DNF and choosing the smallest, iff. it is syntactically smaller than my original formula.

And wrapping the whole thing so if some step/transformation blows up, just skip it and choose from remaining candidates.

But maybe there are better ways to do this ?

Thank you

Set support, Forall / Exists / Element of

Could there be support for the set based operators: ∀,∃, ∈, ∪? Great library!