Skip to content
GitLab
Menu
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
SAT4J
sat4j
Commits
46291e4d
Commit
46291e4d
authored
Feb 08, 2018
by
Daniel Le Berre
Browse files
Added new test case to prevent solvers without learning to pass.
parent
afab137a
Pipeline
#754
passed with stages
in 27 minutes and 8 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
org.sat4j.core/src/test/java/org/sat4j/StampPerformanceTest.java
0 → 100644
View file @
46291e4d
/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004, 2012 Artois University and CNRS
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
*
* Based on the original MiniSat specification from:
*
* An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
* Sixth International Conference on Theory and Applications of Satisfiability
* Testing, LNCS 2919, pp 502-518, 2003.
*
* See www.minisat.se for the original solver in C++.
*
* Contributors:
* CRIL - initial API and implementation
*******************************************************************************/
package
org.sat4j
;
import
static
org
.
junit
.
Assert
.
assertTrue
;
import
java.io.IOException
;
import
org.junit.Test
;
import
org.sat4j.minisat.SolverFactory
;
import
org.sat4j.reader.DimacsReader
;
import
org.sat4j.reader.ParseFormatException
;
import
org.sat4j.reader.Reader
;
import
org.sat4j.specs.ContradictionException
;
import
org.sat4j.specs.ISolver
;
import
org.sat4j.specs.TimeoutException
;
/**
* This is a performance test that requires real conflict driven clause learning
* to be solved.
*
* Stamp project noticed that main functional tests could be solved without
* learning.
*
* @author leberre
*
*/
public
class
StampPerformanceTest
{
@Test
(
timeout
=
60000
)
public
void
testOnlyCDCLSolversCanSolveEfficientlyThis
()
throws
ContradictionException
,
TimeoutException
,
ParseFormatException
,
IOException
{
ISolver
solver
=
SolverFactory
.
newDefault
();
Reader
reader
=
new
DimacsReader
(
solver
);
reader
.
parseInstance
(
"src/test/testfiles/bmc-ibm-3.cnf.gz"
);
assertTrue
(
solver
.
isSatisfiable
());
}
}
org.sat4j.core/src/test/testfiles/bmc-ibm-3.cnf.gz
0 → 100644
View file @
46291e4d
File added
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment