Comments (11)
@myreen What's your operating system? I can't reproduce your steps on Intel macOS:
> minisatProve.SAT_PROVE ``b ==> T``;
val it = |- b ==> T: thm
from hol.
I can confirm the bug with SAT_ORACLE
on my machine
uname -a
Linux yongkiam-ThinkPad-X1C 6.2.0-36-generic #37~22.04.1-Ubuntu SMP PREEMPT_DYNAMIC Mon Oct 9 15:34:04 UTC 2 x86_64 x86_64 x86_64 GNU/Linux
from hol.
@binghe I'm on MacOS running on Mac. But note that you need to call SAT_ORACLE rather than SAT_PROVE.
from hol.
@binghe I'm on MacOS running on Mac. But note that you need to call SAT_ORACLE rather than SAT_PROVE.
Sorry, I didn't notice that! Now I can reproduce too. (Then this seems not an issue of MiniSAT but the SML code behind SAT_ORACLE
).
from hol.
I think the issue is (at least) in the function invoke_solver" (src/HolSat/minisatProve.sml
, line 57-78)
fun invoke_solver solver lfn ntm clauseth cnfv vc is_proved svm sva in_name =
let val nr = Array.length clauseth
in
if access(getSolverExe solver,[A_EXEC]) then
let
val answer = invokeSat solver T (SOME vc) (SOME nr) svm sva in_name
in case answer of
SOME model => (* returns |- model ==> ~t *)
let val model' = transform_model cnfv lfn model
in if is_proved then satCheck model' ntm
else mk_sat_oracle_thm([],mk_imp(list_mk_conj model',ntm)) end
| NONE => (* returns ~t |- F *)
replay_proof is_proved sva nr in_name solver vc clauseth
lfn ntm NONE
end
else (* do not have execute access to solver binary, or it doesn't exist*)
(if nr > !sat_limit then
warn "SAT solver not found. Using slow internal prover."
else ();
DPLL_TAUT (dest_neg ntm))
end
end
In the above function, is_proved
is false when SAT_ORACLE
is used, and true when SAT_PROVE
is used.
from hol.
Hmm... I think just replace mk_sat_oracle_thm([],mk_imp(list_mk_conj model',ntm))
with mk_sat_oracle_thm([ntm],F)
will fix the bug. The above mentioned satCheck()
actually should always return [.] |- F, which after DISCH_ALL
becomes [] |- ~t ==> F
(t is the original problem). If we fully trust the SAT solver and do not do this further verification, mk_sat_oracle_thm([ntm],F)
will give exactly the same output, only this is a theorem without proof.
from hol.
No... if the input term is a /\ ~a
(clearly UNSAT), the value of model'
in the code is [``a``]
and satCheck model' ntm
gives [] |- a ==> ~(a /\ ~a)
, which is indeed in the form model ==> ~t
. I was wrong in saying that satCheck
always returns something like [.] |- F
.
Now I think perhaps the whole idea of SAT_ORACLE
is wrong, without calling satCheck
the intended oracle theorem cannot be determined, because at that moment the code doesn't even know the input term is SAT or UNSAT... @mn200
from hol.
I think... it's possible that MiniSAT's behavior has changed, say, under new C++ compilers. Previously on Linux ARM64, MiniSAT every wrongly reported SAT for an UNSAT problem, and such a mistake was later captured by HOL when trying to construct the fake SAT result as a theorem (whose concl is the input term). Now, perhaps MiniSAT is doing the opposite thing: reporting UNSAT for an SAT problem (e.g. b ==> T
) but this time the further verification (when constructing the output theorem) has automatically fixed the answer, thus the issue was hidden. Using SAT_ORACLE
merely exposed this bug.
from hol.
Now I think it's MiniSAT's problem on certain inputs (~(b ==> T)
is just one of them). Picking another tautology term like b \/ ~b
the SAT_ORACLE
returns correct answer:
> SAT_ORACLE ``b \/ ~b``;
val it = [oracles: DISK_THM, HolSatLib] [axioms: ] [] ⊢ b ∨ ¬b: thm
> SAT_ORACLE ``b ==> T``;
Exception- SAT_cex [oracles: HolSatLib] [axioms: ] [] ⊢ b ⇒ ¬(b ⇒ T) raised
I tried HOL builds back to k6, and also tried latest HOL built with very old C++ compilers (on Mac OS X 10.6, GCC 4.2), the reported issue with b ==> T
is always there. Thus now I think it should be MiniSAT 1.x's original bug.
from hol.
We're using such an old version of MiniSAT that no-one other than us will ever fix it. Is there an obvious test-case we can feed into minisat to demonstrate the problem as a first step?
from hol.
We're using such an old version of MiniSAT that no-one other than us will ever fix it. Is there an obvious test-case we can feed into minisat to demonstrate the problem as a first step?
Yes, I should first confirm if MiniSAT behaves correct on raw inputs (of DIMACS). But then I found MiniSAT is innocent this time!
In minisatProve.sml
, if I manually evaluate the ML code (first, the open
s, then all code inside the local
block). In function GEN_SAT
, I got the following values of its local variables:
val cnfv = SOME "SP": string option
val in_name = "/var/tmp//MLTEMPECqLFC.cnf": string
val lfn = <Redblackmap(1)>: (term, term) RBM.dict
val ntm = ``~(b ==> T)``: term
val sva = fromList[``T``, ``SP0``]: term array
val svm = (2, <Redblackmap(1)>): int * (term, term * int) SVM.dict
val tmpname = "/var/tmp//MLTEMPECqLFC": string
val vc = 1: int
Then, the file contents of in_name
("/var/tmp//MLTEMPECqLFC.cnf") is the following:
c File /var/tmp//MLTEMPECqLFC.cnf generated by HolSatLib
c
p cnf 1 1
1
0
But the above DIMACS is wrong. Here the input term of SAT_ORACLE
is b ==> T
, which is equivalent to ^b \/ T
. Recall that the goal was to check if this term is a tautology (!b. b ==> T
) and the method is to let SAT solver to check the negation of the input term, i.e. ~(b ==> T)
, which is b /\ F
, a CNF.
In DIMACS format, the line p cnf n m
indicates there are totally n Boolean variables and m clauses, and the rest lines each represent one clause, each is a disjunction of involved variables (zero or more), ended with zero. Thus b
is 1 0
, and F
should be just 0
. The above DIMACS file generated by HOL has two issues:
- The line
p cnf ...
has wrong numbers. It should bep cnf 1 2
instead ofp cnf 1 1
(line 3). - Somehow the line for the first clause (
1
) misses the ending zero, i.e., it should be1 0
(line 4).
There's a MiniSat web interface [1] taking DIMACS inputs. If I put the above DIMACS contents as is, the solving result is SAT. But after manual fixes according to the above two issues (only the 2nd is fatal), the result is UNSAT, the correct one.
[1] http://logicrunch.it.uu.se:4096/~wv/minisat/
from hol.
Related Issues (20)
- Building HOL4 will crash with latest Apple update of Xcode HOT 3
- Remove/Name Anonymous Rewrite for NUM_CEILING HOT 1
- Allow "reduced" info printing in emacs HOT 1
- Use rule-names instead of conjunctions in Inductive definitions HOT 1
- `Holmake: Exception: Subscript` when building HOL with -j12 or greater (but not -j11 or lower) HOT 5
- Limits on the number of jobs for Holmake? HOT 2
- "intLib.ARITH_PROVE ``0n = x * Num 0i``" fails unexpectedly HOT 1
- intLib.{ARITH,COOPER}_PROVE can't prove certain goals HOT 5
- intLib.ARITH_PROVE raises exception `NotFound` HOT 1
- Ignore assumption directive for simplifier
- Add spec form to cover both `INST` and `SPEC` of theorems
- Add a q.subpat_{x_,}assum
- A broken generated HTML theory in non-Unicode mode HOT 2
- Moscow ML builds broken after `cv_translator` HOT 1
- General modern "quotation" syntax support
- Q.PAT_X_ASSUM returns bad errors
- C++ compilation failure of `src/HolSat/sat_solvers/zc2hs` on macOS HOT 4
- Fix intLib to avoid noisy output HOT 1
- Unexpected error with `DefnBase.one_line_ify`
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.
from hol.