anjlab / sat3 Goto Github PK
View Code? Open in Web Editor NEWReference Implementation of Romanov's Polynomial Algorithm for Boolean 3-SAT Problem
Home Page: http://romvf.wordpress.com/
License: GNU Lesser General Public License v3.0
sat3's People
Contributors
Stargazers
Watchers
sat3's Issues
Read basic and compact ASCII encoding format
Encoding description:
http://www.is.titech.ac.jp/~watanabe/gensat/index.html#encoding
Samples:
http://www.is.titech.ac.jp/~watanabe/gensat/a2/index.html#sample
Error in finding HSS route for uf125-01.cnf
Hyperstructure created but route was not found for instance uf125-01.cnf from Uniform Random-3-SAT set uf125-538
Support cnf files with sparse variable names
False negative results
Running both 1.0.3 and 2.0.0-SNAPSHOT showed false negative results with the following log output:
04:20:17,337|6946 INFO [Program] - CTF count: 117
04:20:17,337|6946 INFO [Helper] - **********************************************************************
04:20:17,337|6946 INFO [StopWatch] - Create CTS...
04:21:20,025|69634 INFO [StopWatch] - Create CTS: 62688ms; overall: 69491ms
04:21:20,025|69634 INFO [Program] - One of the structures was built empty
com.anjlab.sat3.EmptyStructureException
at com.anjlab.sat3.SimpleFormula.complete(SimpleFormula.java:226)
at com.anjlab.sat3.Helper.completeToCTS(Helper.java:762)
at com.anjlab.sat3.Program.main(Program.java:184)
04:21:20,025|69634 INFO [Helper] - **********************************************************************
04:21:20,025|69634 INFO [StopWatch] - Saving current statictics of calculations to c:\Users\dmitrygusev\Downloads\11f5d019850183f02432a41a4551317c\cnf.cnf-results.txt...
04:21:20,053|69662 INFO [StopWatch] - Saving current statictics of calculations to c:\Users\dmitrygusev\Downloads\11f5d019850183f02432a41a4551317c\cnf.cnf-results.txt: 13ms; overall: 69504ms
Formula not satisfiable
Program completed
Links to CNF instances:
Non-empty HSS for UNSAT instance has been built
We have found several examples where non-empty HSS for UNSAT instances was built. This shouldn't happen according to Theorem 1 (assuming its correct). Here are the instances:
- (sat-2002-beta\submitted\zhang-lintao\xor-chain\x1_16.shuffled.cnf) from SAT Competition 2002 Benchmark
- http://logic.pdmi.ras.ru/~hirsch/benchmarks/hgen8-n260-01-S1597732451.shuffled-as.sat03-885.cnf
Until someone find an error in Theorem 1 we consider this is a bug in implementation.
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.