Skip to content

Commit

Permalink
Merge branch 'release_1.1'
Browse files Browse the repository at this point in the history
  • Loading branch information
czengler committed Aug 29, 2016
2 parents 8b62ddd + b00c639 commit ca506d1
Show file tree
Hide file tree
Showing 169 changed files with 10,535 additions and 3,730 deletions.
2 changes: 1 addition & 1 deletion .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
# vim swap files
*.swp

# build files
# encode files
target/
.sonar/

Expand Down
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
[![wercker status](https://app.wercker.com/status/24c4765f3a0d79520ad80a1e4c20cfa2/s/master "wercker status")](https://app.wercker.com/project/bykey/24c4765f3a0d79520ad80a1e4c20cfa2) [![Coverage Status](https://coveralls.io/repos/logic-ng/LogicNG/badge.svg?branch=master&service=github)](https://coveralls.io/github/logic-ng/LogicNG?branch=master) ![License](https://img.shields.io/badge/license-Apache%202-blue.svg) ![Version](https://img.shields.io/badge/version-1.0.3-ff69b4.svg)
[![wercker status](https://app.wercker.com/status/24c4765f3a0d79520ad80a1e4c20cfa2/s/master "wercker status")](https://app.wercker.com/project/bykey/24c4765f3a0d79520ad80a1e4c20cfa2) [![Coverage Status](https://coveralls.io/repos/logic-ng/LogicNG/badge.svg?branch=master&service=github)](https://coveralls.io/github/logic-ng/LogicNG?branch=master) ![License](https://img.shields.io/badge/license-Apache%202-blue.svg) ![Version](https://img.shields.io/badge/version-1.1-ff69b4.svg)

<img src="https://github.com/logic-ng/LogicNG/blob/master/doc/logo/logo_big.png" alt="logo" width="300">

## Introduction
LogicNG is a Java Library for creating, manipulating and solving Boolean and Pseudo-Boolean formulas. It includes 100% Java implementations of popular tools like [MiniSAT](http://minisat.se), [CleaneLing](http://fmv.jku.at/cleaneling/), [Glucose](http://www.labri.fr/perso/lsimon/glucose/), or [OpenWBO](http://sat.inesc-id.pt/open-wbo/).
LogicNG is a Java Library for creating, manipulating and solving Boolean and Pseudo-Boolean formulas. It includes 100% Java implementations of popular tools like [MiniSAT](http://minisat.se), [CleaneLing](http://fmv.jku.at/cleaneling/), [Glucose](http://www.labri.fr/perso/lsimon/glucose/), [PBLib](http://tools.computational-logic.org/content/pblib.php), or [OpenWBO](http://sat.inesc-id.pt/open-wbo/).

Its main focus lies on memory-efficient data-structures for Boolean formulas and efficient algorithms for manipulating and solving them.
The library is designed to be used in industrial systems which have to manipulate and solve millions of formulas per day.
Expand Down
8 changes: 4 additions & 4 deletions pom.xml
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@
<modelVersion>4.0.0</modelVersion>
<groupId>org.logicng</groupId>
<artifactId>logicng</artifactId>
<version>1.0.3</version>
<version>1.1</version>
<name>LogicNG</name>
<packaging>jar</packaging>

Expand All @@ -42,7 +42,7 @@
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-compiler-plugin</artifactId>
<version>3.3</version>
<version>3.5.1</version>
<configuration>
<source>1.7</source>
<target>1.7</target>
Expand Down Expand Up @@ -71,7 +71,7 @@
<plugin>
<groupId>org.jacoco</groupId>
<artifactId>jacoco-maven-plugin</artifactId>
<version>0.7.5.201505241946</version>
<version>0.7.7.201606060606</version>
<configuration>
<excludes>
<exclude>**/LogicNGPropositional*</exclude>
Expand Down Expand Up @@ -119,7 +119,7 @@
<plugin>
<groupId>org.eluder.coveralls</groupId>
<artifactId>coveralls-maven-plugin</artifactId>
<version>4.1.0</version>
<version>4.2.0</version>
<configuration>
<sourceDirectories>
<sourceDirectory>target/generated-sources/antlr</sourceDirectory>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -28,47 +28,44 @@

package org.logicng.cardinalityconstraints;

import org.logicng.collections.ImmutableFormulaList;
import org.logicng.formulas.FType;
import org.logicng.formulas.Formula;
import org.logicng.formulas.FormulaFactory;
import org.logicng.datastructures.EncodingResult;
import org.logicng.formulas.Variable;

import java.util.LinkedList;
import java.util.List;

/**
* Encodes that exactly one variable is assigned value true. Uses the 'naive' encoding with no introduction
* of new variables but quadratic size.
* @version 1.0
* @since 1.0
* Encodes that at least 'rhs' variables are assigned value true. Uses the cardinality network
* encoding due to Asín, Nieuwenhuis, Oliveras, and Rodríguez-Carbonell .
* @version 1.1
* @since 1.1
*/
public final class CCEXOPure extends CCExactlyOne {
final class CCALKCardinalityNetwork implements CCAtLeastK {

private final FormulaFactory f;
private final CCCardinalityNetworks cardinalityNetwork;

/**
* Constructs the naive EXO encoder.
* @param f the formula factory
* Constructs a new cardinality encoder.
*/
public CCEXOPure(final FormulaFactory f) {
this.f = f;
CCALKCardinalityNetwork() {
this.cardinalityNetwork = new CCCardinalityNetworks();
}

@Override
public void build(final EncodingResult result, final Variable[] vars, int rhs) {
cardinalityNetwork.buildALK(result, vars, rhs);
}

@Override
public ImmutableFormulaList build(final Variable... vars) {
final List<Formula> result = new LinkedList<>();
if (vars.length == 0)
return new ImmutableFormulaList(FType.AND);
if (vars.length == 1) {
result.add(vars[0]);
return new ImmutableFormulaList(FType.AND, result);
}
result.add(this.f.clause(vars));
for (int i = 0; i < vars.length; i++)
for (int j = i + 1; j < vars.length; j++)
result.add(this.f.clause(vars[i].negate(), vars[j].negate()));
return new ImmutableFormulaList(FType.AND, result);
public CCIncrementalData incrementalData() {
return cardinalityNetwork.incrementalData();
}

/**
* Builds the constraint for incremental usage.
* @param result the result
* @param vars the variables
* @param rhs the right-hand side
*/
void buildForIncremental(final EncodingResult result, final Variable[] vars, int rhs) {
cardinalityNetwork.buildALKForIncremental(result, vars, rhs);
}

@Override
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -28,45 +28,36 @@

package org.logicng.cardinalityconstraints;

import org.logicng.collections.ImmutableFormulaList;
import org.logicng.formulas.FType;
import org.logicng.formulas.Formula;
import org.logicng.datastructures.EncodingResult;
import org.logicng.formulas.FormulaFactory;
import org.logicng.formulas.Variable;

import java.util.LinkedList;
import java.util.List;

/**
* Encodes that exactly one variable is assigned value true. Uses the 2-product method due to Chen.
* @version 1.0
* Encodes that at least 'rhs' variables can be assigned value true. Uses the modular totalizer encoding for
* translating the cardinality constraint into CNF.
* @version 1.1
* @since 1.0
*/
public final class CCEXOProduct extends CCExactlyOne {
private final FormulaFactory f;
private final CCAMOProduct amo;
final class CCALKModularTotalizer implements CCAtLeastK {

private final CCModularTotalizer totalizer;

/**
* Constructs the naive AMO encoder.
* Constructs a new modular totalizer.
* @param f the formula factory
*/
public CCEXOProduct(final FormulaFactory f) {
this.f = f;
this.amo = new CCAMOProduct(f);
CCALKModularTotalizer(final FormulaFactory f) {
this.totalizer = new CCModularTotalizer(f);
}

@Override
public void build(final EncodingResult result, final Variable[] vars, int rhs) {
this.totalizer.buildALK(result, vars, rhs);
}

@Override
public ImmutableFormulaList build(final Variable... vars) {
final List<Formula> result = new LinkedList<>();
if (vars.length == 0)
return new ImmutableFormulaList(FType.AND);
if (vars.length == 1) {
result.add(vars[0]);
return new ImmutableFormulaList(FType.AND, result);
}
result.add(this.f.or(vars));
result.addAll(this.amo.build(vars).toList());
return new ImmutableFormulaList(FType.AND, result);
public CCIncrementalData incrementalData() {
return this.totalizer.incrementalData();
}

@Override
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -26,56 +26,36 @@
// //
///////////////////////////////////////////////////////////////////////////

/*****************************************************************************************
* Open-WBO -- Copyright (c) 2013-2015, Ruben Martins, Vasco Manquinho, Ines Lynce
* <p>
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
* <p>
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
* <p>
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*****************************************************************************************/

package org.logicng.cardinalityconstraints;

import org.logicng.collections.ImmutableFormulaList;
import org.logicng.formulas.FormulaFactory;
import org.logicng.datastructures.EncodingResult;
import org.logicng.formulas.Variable;

import java.util.Collection;

/**
* Encodes that at least 'rhs' variables are assigned value true. Uses the totalizer encoding for
* translating the cardinality constraint into CNF.
* @version 1.0
* @version 1.1
* @since 1.0
*/
public final class CCALKTotalizer extends CCAtLeastK {
final class CCALKTotalizer implements CCAtLeastK {

private final CCTotalizer totalizer;

/**
* Constructs a new totalizer.
* @param f the formula factory
*/
public CCALKTotalizer(final FormulaFactory f) {
this.totalizer = new CCTotalizer(f);
CCALKTotalizer() {
this.totalizer = new CCTotalizer();
}

@Override
public void build(final EncodingResult result, final Variable[] vars, int rhs) {
this.totalizer.buildALK(result, vars, rhs);
}

@Override
public ImmutableFormulaList build(final Collection<Variable> vars, int rhs) {
return this.totalizer.buildALK(vars, rhs);
public CCIncrementalData incrementalData() {
return this.totalizer.incrementalData();
}

@Override
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,75 @@
///////////////////////////////////////////////////////////////////////////
// __ _ _ ________ //
// / / ____ ____ _(_)____/ | / / ____/ //
// / / / __ \/ __ `/ / ___/ |/ / / __ //
// / /___/ /_/ / /_/ / / /__/ /| / /_/ / //
// /_____/\____/\__, /_/\___/_/ |_/\____/ //
// /____/ //
// //
// The Next Generation Logic Library //
// //
///////////////////////////////////////////////////////////////////////////
// //
// Copyright 2015-2016 Christoph Zengler //
// //
// Licensed under the Apache License, Version 2.0 (the "License"); //
// you may not use this file except in compliance with the License. //
// You may obtain a copy of the License at //
// //
// http://www.apache.org/licenses/LICENSE-2.0 //
// //
// Unless required by applicable law or agreed to in writing, software //
// distributed under the License is distributed on an "AS IS" BASIS, //
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or //
// implied. See the License for the specific language governing //
// permissions and limitations under the License. //
// //
///////////////////////////////////////////////////////////////////////////

package org.logicng.cardinalityconstraints;

import org.logicng.datastructures.EncodingResult;
import org.logicng.formulas.Variable;

/**
* Encodes that at most 'rhs' variables are assigned value true. Uses the cardinality network
* encoding due to Asín, Nieuwenhuis, Oliveras, and Rodríguez-Carbonell .
* @version 1.1
* @since 1.1
*/
final class CCAMKCardinalityNetwork implements CCAtMostK {

private final CCCardinalityNetworks cardinalityNetwork;

/**
* Constructs a new cardinality encoder.
*/
CCAMKCardinalityNetwork() {
this.cardinalityNetwork = new CCCardinalityNetworks();
}

@Override
public void build(final EncodingResult result, final Variable[] vars, int rhs) {
cardinalityNetwork.buildAMK(result, vars, rhs);
}

@Override
public CCIncrementalData incrementalData() {
return cardinalityNetwork.incrementalData();
}

/**
* Builds the constraint for incremental usage.
* @param result the result
* @param vars the variables
* @param rhs the right-hand side
*/
void buildForIncremental(final EncodingResult result, final Variable[] vars, int rhs) {
cardinalityNetwork.buildAMKForIncremental(result, vars, rhs);
}

@Override
public String toString() {
return this.getClass().getSimpleName();
}
}
Loading

0 comments on commit ca506d1

Please sign in to comment.